arXiv:2505.04528v1 宣告类型: 新 摘要: 作为一个看似自解释的任务，问题解决一直是科学和工程中的一个重要组成部分。然而，问题解决本身的通用且具体的表述仍然缺失。随着基于AI的问题解决代理的 recent 发展，过程级可验证的需求正在迅速增加但尚未得到充分开发。为填补这些空白，我们提出了一种问题解决的原理性表述，作为确定性马尔可夫决策过程；一种新型框架 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%。