构建可验证的数学问题求解框架，提升AI解题过程透明度与人类对齐性。
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
- 将问题求解建模为确定性马尔可夫决策过程，实现过程可验证。
- 在三个新基准上测试，最高解题率仅27.47%，凸显挑战性。
- 适合关注AI可解释性、形式化验证的研究者与教育应用开发者。
问题求解虽看似直观，但缺乏通用而具体的定义。随着基于AI的问题求解代理兴起，过程可验证性需求日益迫切却研究不足。为此，本文提出将问题求解形式化为确定性马尔可夫决策过程；设计新框架FPS（Formal Problem-Solving），利用现有FTP（形式化定理证明）环境实现过程验证；提出D-FPS（Deductive FPS），解耦求解与答案验证以增强人机对齐。框架的表达性、保真性与完备性均被证明。构建三个新基准：FormalMath500（MATH500子集的形式化版本）、MiniF2F-Solving与PutnamBench-Solving，分别适配FTP基准。为实现可信赖、可解释且人类对齐的评估，提出RPE（Restricted Propositional Equivalence）——一种通过形式化验证判定答案正确性的符号方法。在四个主流FTP模型和两种提示方法的基线测试中，最高解题率分别为：FormalMath500的23.77%、MiniF2F-Solving的27.47%、PutnamBench-Solving的0.31%。
原文摘要 · Abstract (English)
As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent development of AI-based problem-solving agents, the demand for process-level verifiability is rapidly increasing yet underexplored. To fill these gaps, we present a principled formulation of problem-solving as a deterministic Markov decision process; a novel framework, FPS (Formal Problem-Solving), which utilizes existing FTP (formal theorem proving) environments to perform process-verified problem-solving; and D-FPS (Deductive FPS), decoupling solving and answer verification for better human-alignment. The expressiveness, soundness and completeness of the frameworks are proven. We construct three benchmarks on problem-solving: FormalMath500, a formalization of a subset of the MATH500 benchmark; MiniF2F-Solving and PutnamBench-Solving, adaptations of FTP benchmarks MiniF2F and PutnamBench. For faithful, interpretable, and human-aligned evaluation, we propose RPE (Restricted Propositional Equivalence), a symbolic approach to determine the correctness of answers by formal verification. We evaluate four prevalent FTP models and two prompting methods as baselines, solving at most 23.77% of FormalMath500, 27.47% of MiniF2F-Solving, and 0.31% of PutnamBench-Solving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。