为推理模型时代的高级定理证明复活 DSP
摘要
近期进展如 DeepSeek-Prover-V2-671B 和 Kimina-Prover-Preview-72B, 表明在自动定理证明中存在一种以强化学习(RL)为基础的大规模训练趋势。令人惊讶的是, 我们发现即使没有任何训练, 通过仔细协调现有即插即用推理模型和 tactic step provers 也能实现相当的性能。本文介绍了 \textbf{DSP+}，这是一种改进版的草案、草图和证明框架, 其特点是针对每个阶段的 \emph{细粒度且集成} 的神经符号增强: (1) 在草案阶段, 我们提示推理模型生成简洁的自然语言子目标以利于草图阶段, 删除思考标记和对人类编写证明的引用; (2) 在草图阶段, 子目标被自动形式化为带有假设的语句以利于证明阶段, 并根据预定义规则屏蔽包含语法错误的草图行; (3) 在证明阶段, 我们将符号搜索方法如 Aesop 与 step provers 紧密集成, 以为草图子目标建立证明。实验结果表明, 在无需任何额外模型训练或微调的情况下, DSP+ 解决了 miniF2F、ProofNet 和 PutnamBench 中分别为 644、644 和 24 个问题中的 80.7%、32.8% 和 24 个问题, 而且所需资源比最先进的方案更少。DSP+ 解决了 miniF2F 中的一个 IMO 题目 \texttt{imo\_2019\_p1}, 该题目是任何先前工作都未解决的。此外, DSP+ 生成的证明模式可以被人类专家理解, 以便识别形式化错误; 例如, 发现了 miniF2F 中的八个错误形式化的陈述。我们的结果凸显了除 RL-based 训练之外的经典推理模式的潜力。所有组件将开源。
引用
@article{arxiv.2506.11487,
title = {Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models},
author = {Chenrui Cao and Liangcheng Song and Zenan Li and Xinyi Le and Xian Zhang and Hui Xue and Fan Yang},
journal= {arXiv preprint arXiv:2506.11487},
year = {2025}
}
备注
31 pages. Associated code and results are available at https://github.com/microsoft/DSP-Plus