Bourbaki：用于定理证明的自生成和目标条件化 MDP
人工智能
2025-07-04 v1 机器学习
摘要
推理是大型语言模型 (LLM) 面临的挑战之一，尤其是在自动定理证明 (ATP) 的逻辑受限环境中，因为稀疏奖励和证明规模的巨大。PutnamBench 等基准测试包含需要复杂、多步骤推理的大学水平问题，这放大了这些挑战。为此，我们提出自生成目标条件化 MDP (sG-MDP)，即一种代理人根据演化的证明状态生成并追求其子目标的框架。通过更结构化的目标生成，问题变得更适合搜索。我们然后应用类似蒙特卡洛树搜索 (MCTS) 的算法来解决 sG-MDP，在 Bourbaki (7B) 中实现我们的方案，该系统可以集成多个 7B LLM 用于子目标生成和战术综合。在 PutnamBench 上，Bourbaki (7B) 解决了 26 个问题，实现了该规模模型的新型态最佳结果。
引用
@article{arxiv.2507.02726,
title = {Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving},
author = {Matthieu Zimmer and Xiaotong Ji and Rasul Tutunov and Anthony Bordg and Jun Wang and Haitham Bou Ammar},
journal= {arXiv preprint arXiv:2507.02726},
year = {2025}
}