Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

📄 arXiv: 2507.02726v1 📥 PDF

作者: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, Haitham Bou Ammar

分类: cs.AI, cs.LG

发布日期: 2025-07-03

💡 一句话要点

提出基于自生成目标条件MDP的Bourbaki框架，用于提升定理证明能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动定理证明 大型语言模型 马尔可夫决策过程 蒙特卡洛树搜索 目标条件学习 推理 PutnamBench

📋 核心要点

  1. 自动定理证明面临奖励稀疏和搜索空间巨大的挑战，尤其是在复杂问题如PutnamBench上，现有方法难以有效推理。
  2. 论文提出自生成目标条件MDP（sG-MDPs）框架，通过智能体自主生成并追求子目标，将复杂问题分解为更易管理的子问题。
  3. Bourbaki (7B)系统集成了多个7B LLM，利用MCTS算法求解sG-MDP，在PutnamBench上取得了显著的性能提升，解决了26个问题。

📝 摘要（中文）

由于稀疏奖励和证明规模庞大，推理对于大型语言模型（LLMs）来说仍然是一项具有挑战性的任务，尤其是在自动定理证明（ATP）的逻辑约束环境中。在PutnamBench等基准测试中，这种挑战更加明显，因为它包含需要复杂的多步骤推理的大学水平问题。为了解决这个问题，我们引入了自生成目标条件MDP（sG-MDPs），这是一个新的框架，其中智能体基于不断演变的证明状态生成和追求其子目标。鉴于这种更结构化的目标生成，由此产生的问题更易于搜索。然后，我们应用类似于蒙特卡洛树搜索（MCTS）的算法来解决sG-MDP，并在Bourbaki (7B) 中实例化我们的方法，Bourbaki (7B) 是一个模块化系统，可以集成多个 7B LLM，用于子目标生成和策略综合。在 PutnamBench 上，Bourbaki (7B) 解决了 26 个问题，在使用这种规模的模型时实现了新的最先进的结果。

🔬 方法详解

问题定义：论文旨在解决大型语言模型在自动定理证明任务中面临的推理难题，特别是对于需要复杂多步推理的问题，例如 PutnamBench 中的大学水平问题。现有方法由于奖励稀疏和搜索空间巨大，难以有效地找到正确的证明路径。

核心思路：论文的核心思路是将定理证明问题转化为一个自生成目标条件马尔可夫决策过程（sG-MDP）。智能体不再直接尝试证明最终定理，而是自主生成一系列子目标，并逐步实现这些子目标，最终达到证明目标。这种分解策略将复杂的证明过程分解为更小、更易于管理的步骤，从而降低了搜索难度。

技术框架：Bourbaki 框架包含以下主要模块：1) 子目标生成器：利用大型语言模型生成可能的子目标，这些子目标是当前证明状态的逻辑推论。2) 策略合成器：使用另一个大型语言模型，根据当前证明状态和子目标，生成相应的策略（即证明步骤）。3) 环境：模拟定理证明环境，根据策略更新证明状态，并提供奖励信号。4) 搜索算法：采用类似于蒙特卡洛树搜索（MCTS）的算法，在 sG-MDP 中进行搜索，选择最优的子目标和策略序列。

关键创新：论文的关键创新在于提出了自生成目标条件 MDP (sG-MDP) 的概念。与传统的 MDP 相比，sG-MDP 中的目标不是预先设定的，而是由智能体根据当前状态动态生成的。这种自生成目标的方式使得智能体能够更好地适应复杂的证明环境，并有效地探索证明空间。与现有方法相比，Bourbaki 不需要人工设计的启发式规则或专家知识，而是通过自主学习的方式来解决定理证明问题。

关键设计：Bourbaki 系统集成了多个 7B LLM，分别用于子目标生成和策略合成。具体来说，一个 LLM 用于根据当前证明状态生成多个候选子目标，另一个 LLM 用于根据当前证明状态和选定的子目标生成相应的策略。MCTS 算法用于在 sG-MDP 中进行搜索，选择最优的子目标和策略序列。奖励函数的设计至关重要，它需要能够有效地引导智能体朝着正确的证明方向前进。具体的奖励函数设计细节在论文中可能有所描述（未知）。

🖼️ 关键图片

fig_0

📊 实验亮点

Bourbaki (7B) 在 PutnamBench 上解决了 26 个问题，在使用 7B 规模的模型时实现了新的 state-of-the-art 结果。这一结果表明，通过自生成目标条件 MDP 和 MCTS 算法，可以有效地提升大型语言模型在复杂推理任务中的性能。该方法在模型规模较小的情况下，也能取得显著的性能提升，具有一定的实际应用价值。

🎯 应用场景

该研究成果可应用于自动定理证明、数学推理、代码验证等领域。通过将复杂问题分解为子目标，并利用大型语言模型进行策略搜索，可以显著提高问题求解的效率和准确性。未来，该方法有望应用于更广泛的逻辑推理和知识发现任务，例如智能合约验证、AI安全等。

📄 摘要（原文）

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.