超越定理证明：形式化问题解决的表述、框架与基准

问题解决作为一个看似不言自明的任务，一直是科学和工程的重要组成部分。然而，对于问题解决本身，目前还缺乏一种通用而具体的形式化表述。随着近期基于人工智能的问题解决智能体的发展，对过程级可验证性的需求迅速增加，但这一领域尚未得到充分探索。为了填补这些空白，我们提出了一种将问题解决形式化为确定性马尔可夫决策过程的原则性方法；一个新的框架FPS（形式化问题解决），它利用现有的FTP（形式化定理证明）环境来进行过程验证的问题解决；以及D-FPS（演绎式FPS），它将求解和答案验证解耦，以更好地实现人机对齐。我们证明了这些框架的表达能力、合理性和完备性。我们构建了三个问题解决基准：FormalMath500，是MATH500基准的一个子集的正式形式化；MiniF2F-Solving和PutnamBench-Solving，是FTP基准MiniF2F和PutnamBench的改编版本。为了进行忠实、可解释和人机对齐的评估，我们提出了RPE（受限命题等价），这是一种通过形式化验证来确定答案正确性的符号方法。我们评估了四种流行的FTP模型和两种提示方法作为基线，它们在FormalMath500上最高解决了23.77%，在MiniF2F-Solving上解决了27.47%，在PutnamBench-Solving上解决了0.31%。