基於大規模 LEAN 問題集的專家迭代方法，推進自動定理證明：InternLM2.5-StepProver

核心概念

通過在大規模 LEAN 問題集上進行專家迭代訓練，InternLM2.5-StepProver 在自動定理證明方面取得了顯著進展，證明了專家迭代和評論模型在解決複雜數學問題方面的有效性。

要約

InternLM2.5-StepProver：基於大規模 LEAN 問題集的專家迭代方法，推進自動定理證明

研究背景

自動定理證明是人工智能領域中一個極具挑戰性的課題，需要複雜的推理能力和對數學的深入理解。近年來，大型語言模型（LLM）在數學定理證明方面展現出巨大潛力，特別是在使用 LEAN 等形式語言的情況下。

研究方法

本研究提出了 InternLM2.5-StepProver，這是一種基於專家迭代方法的自動定理證明模型。研究人員利用包含超過 20,000 個 CPU 天的 Lean-workbook 問題集進行專家迭代訓練。在迭代過程中，研究人員發現，解決問題的數量與證明長度和 CPU 使用量之間存在對數線性關係。此外，他們還訓練了一個評論模型，用於選擇相對簡單的問題供策略模型進行嘗試，並引導模型尋找更深層次的證明。

主要發現

• 成功率：只有 1.5% 的 CPU 使用量產生了成功的證明或反證，這凸顯了自動定理證明的巨大難度。
• 搜索策略：與樸素的最佳優先搜索方法相比，集成評論模型始終產生更深層次的證明。
• 比例關係：研究人員發現，已證明問題的數量與證明長度和計算資源之間存在對數線性關係，這為未來工作中的資源分配提供了寶貴的見解。

研究結論

InternLM2.5-StepProver 在 MiniF2F、Lean-Workbook-Plus、ProofNet 和 Putnam 等基準測試中均取得了最先進的表現。具體而言，它在 MiniF2F 測試中達到了 65.9% 的通過率，並在 Lean-Workbook-Plus 中證明（或反證）了 17.0% 的問題，與 Lean-Workbook-Plus 發布時僅證明了 9.5% 的問題相比有了顯著改進。

研究意義

本研究為提高證明搜索效率提供了實用的指導，並提出了擴展到與 AlphaProof 的 1 億個問題相當的更大訓練集的途徑。研究結果為自動數學推理的未來發展提供了具體指導。

研究局限性

本研究主要關注上下文級別的數學問題，較少關注其他自動定理證明場景。此外，目前還缺乏穩定的指標來衡量評論模型，這使得評論模型的迭代變得困難。

統計

研究人員使用超過 20,000 個 CPU 天來搜索 Lean-Workbook-Plus 上的證明。
InternLM2.5-StepProver 在 MiniF2F 測試中達到了 65.9% 的通過率。
InternLM2.5-StepProver 在 Lean-Workbook-Plus 中證明（或反證）了 17.0% 的問題。
只有 1.5% 的 CPU 使用量產生了成功的證明或反證。

引用

"Only 1.5% of CPU usage resulted in successful proofs or disproofs, highlighting the substantial difficulty of automated theorem proving."
"The integration of a critic model consistently produced deeper proofs compared to naive best-first-search approaches."
"We identified a log-linear relationship between the number of proved problems and both proof length and computational resources, providing valuable insights for resource allocation in future work."

抽出されたキーインサイト

InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems

by Zijian Wu, S... 場所 arxiv.org 10-22-2024

https://arxiv.org/pdf/2410.15700.pdf

深掘り質問

除了數學領域，這種專家迭代方法是否可以用於其他形式的自動推理，例如法律或醫學診斷？

是的，專家迭代方法不僅可以用於數學領域的自動推理，也可以應用於其他形式的自動推理，例如法律或醫學診斷。其核心思想是利用專家知識對模型進行迭代訓練，使其在特定領域的推理能力逐步提升。
以法律領域為例，可以構建一個包含法律條文、案例分析、法律意見書等數據的數據集。模型可以先學習如何理解法律條文和案例，然後嘗試根據給定的案件事實進行推理，給出初步的法律意見。法律專家可以對模型的推理結果進行評估和修正，并将修正后的結果反馈给模型进行学习。通过多轮迭代，模型可以逐步学习到法律专家的推理模式和判断标准，从而提高其在法律推理方面的准确性和可靠性。
同樣地，在醫學診斷領域，可以利用大量的病歷數據、醫學文獻、影像學資料等訓練模型。模型可以先學習如何识别医学影像、理解病历信息，然后尝试根据患者的症状和检查结果进行初步诊断。医学专家可以对模型的诊断结果进行评估和修正，并将修正后的结果反馈给模型进行学习。通过多轮迭代，模型可以逐步学习到医学专家的诊断思路和经验，从而提高其在医学诊断方面的准确性和可靠性。
然而，需要注意的是，将专家迭代方法应用于法律或医学診斷等领域也面临着一些挑战：

数据质量问题: 法律和医学领域的数据往往存在噪声、偏差、不完整等问题，这会影响模型的训练效果。
专家知识的获取和表示: 法律和医学领域的专家知识往往非常复杂，难以用简单的规则或模型进行完全的表示。
伦理和法律风险: 在法律和医学领域，错误的推理结果可能会带来严重的伦理和法律风险。
因此，在将专家迭代方法应用于这些领域时，需要谨慎考虑上述挑战，并采取相应的措施来 mitigate 这些风险。

如果數據集中存在偏差或不完整性，專家迭代方法是否會放大這些問題，從而導致有偏見或不完整的證明？

是的，如果數據集中存在偏差或不完整性，專家迭代方法有可能會放大這些問題，導致模型產生有偏見或不完整的證明。
這是因為專家迭代方法本质上是一种数据驱动的学习方法，模型的推理能力很大程度上取决于训练数据的质量。如果训练数据本身存在偏差或不完整性，模型就很难学习到全面的知识和正确的推理模式。相反，模型可能会过度拟合训练数据中的偏差，从而放大这些偏差，导致其在面对新的、未见过的数据时，产生有偏见或不完整的推理结果。
以下是一些可能导致问题被放大的具体例子：

数据偏差: 如果训练数据集中包含的数学问题类型单一，例如主要集中在代数领域，而较少涉及几何或拓扑学，那么模型在经过专家迭代训练后，很可能在代数领域的推理能力较强，但在其他领域的推理能力较弱，从而导致其在面对新的数学问题时，产生有偏见的证明。
数据不完整: 如果训练数据集中缺少某些重要的定理或公理，那么模型在进行推理时，就可能无法获得必要的知识，从而导致其无法完成完整的证明。
为了避免专家迭代方法放大数据偏差或不完整性带来的问题，可以采取以下措施：

构建高质量的训练数据集: 尽可能确保训练数据集的全面性和代表性，涵盖不同类型、不同难度的数学问题，并尽量减少数据偏差。
引入多种评估指标: 除了准确率之外，还可以使用其他指标来评估模型的推理能力，例如泛化能力、鲁棒性、可解释性等。
结合其他方法: 可以将专家迭代方法与其他方法结合起来，例如符号推理、知识图谱等，以弥补数据驱动方法的不足。
总而言之，专家迭代方法虽然可以有效提高模型的推理能力，但在实际应用中，需要充分意识到数据偏差和不完整性带来的潜在风险，并采取相应的措施来避免这些问题被放大。

如何設計一個評估指標，更準確地衡量評論模型在引導策略模型尋找更深層次證明方面的有效性？

为了更准确地衡量评论模型在引导策略模型寻找更深层次证明方面的有效性，可以考虑以下几个方面的评估指标：
1. 基于搜索效率的指标:

平均证明长度 (Average Proof Length): 统计在评论模型的指导下，策略模型成功找到的证明的平均长度。平均证明长度越长，说明评论模型越能引导策略模型找到更深层次的证明。
证明深度 (Proof Depth): 类似于平均证明长度，但更关注证明的逻辑层次结构，可以统计证明树的深度。
搜索步数 (Search Steps): 统计策略模型在找到证明之前所需要的平均搜索步数。搜索步数越少，说明评论模型的引导效率越高。
成功率 vs. 搜索预算 (Success Rate vs. Search Budget): 分析在不同的搜索预算（例如允许搜索的步数或时间）下，策略模型在评论模型指导下找到证明的成功率。
2. 基于证明质量的指标:

证明简洁性 (Proof Conciseness): 评估找到的证明是否简洁易懂，例如可以使用代码行数或逻辑推理步骤的数量来衡量。
证明可读性 (Proof Readability): 可以采用人工评估的方式，评价证明的逻辑清晰度和易懂程度。
证明新颖性 (Proof Novelty): 评估找到的证明是否是新的、未曾出现过的证明路径，可以反映评论模型的引导能力是否跳出了训练数据的局限。
3. 基于模型泛化能力的指标:

跨领域迁移能力 (Cross-Domain Transferability): 测试评论模型在引导策略模型解决不同数学领域问题时的效果，例如从代数领域迁移到几何领域。
未见问题解决能力 (Zero-Shot Problem Solving): 测试评论模型在引导策略模型解决未曾见过的新问题时的效果。
在实际评估中，可以根据具体的研究目标和应用场景，选择合适的指标组合，并进行综合分析。
此外，还可以考虑以下几点：

与基线模型进行比较: 将评论模型引导的策略模型与其他基线模型（例如未使用评论模型的策略模型）进行比较，以更直观地体现评论模型的有效性。
进行消融实验: 通过逐步移除评论模型的某些功能模块，观察其对最终证明结果的影响，以分析评论模型各个模块的作用和贡献。
总而言之，设计一个全面、合理的评估指标体系对于准确衡量评论模型的有效性至关重要。