用自生成目标增强推理，让大模型在数学定理证明中表现更优。
Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
- 模型动态生成子目标，将复杂证明分解为可搜索路径。
- 在PutnamBench上解决26道题，70亿参数模型达到新最好水平。
- 适合需要多步逻辑推理的数学证明任务，尤其适用于高阶竞赛题。
大语言模型在自动化定理证明（ATP）中仍面临挑战，尤其在奖励稀疏且证明空间庞大的场景下。以大学级别问题为主的PutnamBench更具挑战性，需复杂多步推理。为此，我们提出自生成目标条件化的马尔可夫决策过程（sG-MDP），让智能体基于不断演化的证明状态自主生成并追求子目标。这种结构化的目标生成使问题更适于搜索。我们采用类似蒙特卡洛树搜索（MCTS）的算法求解sG-MDP，构建了名为Bourbaki（7B）的模块化系统，可集成多个70亿参数的LLM进行子目标生成与策略合成。在PutnamBench上，Bourbaki（7B）成功解决26道题，成为该规模模型中的最新最佳结果。
原文摘要 · Abstract (English)
Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。