用批评模型引导搜索，提升大模型自动证明定理能力。
InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
- 引入批评模型捕捉证明轨迹偏好信息，动态指导搜索路径。
- 在20,000多CPU天的专家迭代后，证明成功率从59.4%提升至65.9%。
- 适合关注形式化证明与大模型推理优化的研究者和开发者。
大语言模型（LLM）在数学定理证明中展现出强大潜力，尤其在使用形式语言如LEAN时。现有方法通常采用最佳优先搜索策略，逐条构建证明策略，但忽略了已有策略轨迹中的关键偏好信息，限制了深层证明的探索。本文提出一种直观而有效的方法：利用批评模型捕捉偏好信息，并在运行时指导证明模型的搜索。基于该证明-批评框架，我们进行了超过20,000 CPU天的大规模专家迭代，进一步微调证明模型与批评模型。训练后的InternLM2.5-StepProver显著提升了证明模型性能，成功率由59.4%提高至65.9%。我们还分析了批评模型在专家迭代过程中对定理证明各环节的影响，揭示其有效性。模型与搜索到的证明已开源，详见https://github.com/InternLM/InternLM-Math 和 https://huggingface.co/datasets/internlm/Lean-Workbook。
原文摘要 · Abstract (English)
Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。