HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

📄 arXiv: 2505.15740v1 📥 PDF

作者: Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer

分类: cs.FL, cs.AI, cs.SE

发布日期: 2025-05-21

💡 一句话要点

HybridProver：结合LLM驱动的证明合成与细化的定理证明框架

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

关键词: 自动化定理证明 大型语言模型 形式化验证 证明合成 策略细化 Isabelle miniF2F

📋 核心要点

  1. 形式化验证依赖人工证明和专业工具，效率低且门槛高，阻碍了其广泛应用。
  2. HybridProver结合整体证明生成和策略细化，利用LLM自动生成并完善证明过程。
  3. 实验表明，HybridProver在miniF2F数据集上达到59.4%的成功率，超越了现有SOTA。

📝 摘要（中文）

形式化方法对于通过严格的数学证明来验证关键系统的可靠性至关重要。然而，其应用受到劳动密集型的手动证明以及使用定理证明器所需的专业知识的阻碍。大型语言模型（LLM）的最新进展为自动化定理证明提供了新的机会。两种有希望的方法是逐步生成策略和直接用LLM生成整个证明。然而，现有的工作没有尝试结合这两种方法。在这项工作中，我们介绍了HybridProver，一个双模型证明合成框架，它结合了基于策略的生成和整体证明合成，以利用这两种方法的优势。HybridProver直接生成用于评估的完整证明候选，然后从这些候选中提取证明草图。然后，它使用基于策略的生成模型，该模型集成了自动化工具，通过逐步细化来完成草图。我们为Isabelle定理证明器实现了HybridProver，并在我们优化的Isabelle数据集上微调了LLM。在miniF2F数据集上的评估证明了HybridProver的有效性。我们在miniF2F上实现了59.4%的成功率，而之前的SOTA是56.1%。我们的消融研究表明，这一SOTA结果归因于结合了整体证明和基于策略的生成。此外，我们展示了数据集质量、训练参数和抽样多样性如何影响LLM自动化定理证明的最终结果。我们所有的代码、数据集和LLM都是开源的。

🔬 方法详解

问题定义：论文旨在解决自动化定理证明中，现有方法要么依赖人工设计的策略，要么直接生成完整证明但缺乏细粒度控制的问题。现有方法的痛点在于，人工策略需要专家知识，而直接生成的方法难以保证正确性和可解释性。

核心思路：论文的核心思路是结合整体证明生成和策略细化两种方法。首先，利用LLM生成完整的证明候选，然后从中提取关键的证明草图。接着，使用基于策略的生成模型，结合自动化工具，逐步完善这些草图，从而实现更高效和可靠的自动化定理证明。

技术框架：HybridProver框架包含两个主要阶段：1) 整体证明生成阶段：使用LLM直接生成完整的证明候选。2) 策略细化阶段：从候选证明中提取证明草图，并使用基于策略的生成模型，结合自动化工具，逐步完善这些草图。框架还包括一个评估模块，用于评估生成的证明候选的质量。

关键创新：HybridProver的关键创新在于结合了整体证明生成和策略细化两种方法，充分利用了LLM的生成能力和自动化工具的推理能力。与现有方法相比，HybridProver能够更有效地生成高质量的证明，并提高自动化定理证明的成功率。

关键设计：论文使用了微调的LLM作为整体证明生成模型和策略生成模型。数据集的质量对最终结果有重要影响，因此论文对Isabelle数据集进行了优化。训练参数和抽样多样性也对结果有影响，论文进行了详细的实验分析。具体参数设置和网络结构在论文中有详细描述，此处未知。

🖼️ 关键图片

fig_0

📊 实验亮点

HybridProver在miniF2F数据集上取得了显著的成果，成功率达到59.4%，超越了之前的SOTA（56.1%）。消融实验证明，结合整体证明生成和策略细化是取得这一成果的关键。此外，论文还分析了数据集质量、训练参数和抽样多样性对结果的影响，为LLM在自动化定理证明中的应用提供了宝贵的经验。

🎯 应用场景

HybridProver具有广泛的应用前景，可用于验证软件和硬件系统的正确性，提高关键系统的可靠性。例如，可应用于操作系统内核、编译器、密码协议等关键领域的验证，减少漏洞和错误，提升系统安全性。未来，该技术有望进一步降低形式化验证的门槛，促进其在工业界的广泛应用。

📄 摘要（原文）

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent advancements in large language models (LLMs) offer new opportunities for automated theorem proving. Two promising approaches are generating tactics step by step and generating a whole proof directly with an LLM. However, existing work makes no attempt to combine the two approaches. In this work, we introduce HybridProver, a dual-model proof synthesis framework that combines tactic-based generation and whole-proof synthesis to harness the benefits of both approaches. HybridProver generates whole proof candidates for evaluation directly, then extracts proof sketches from those candidates. It then uses a tactic-based generation model that integrates automated tools to complete the sketches via stepwise refinement. We implement HybridProver for the Isabelle theorem prover and fine-tune LLMs on our optimized Isabelle datasets. Evaluation on the miniF2F dataset illustrates HybridProver's effectiveness. We achieve a 59.4% success rate on miniF2F, where the previous SOTA is 56.1%. Our ablation studies show that this SOTA result is attributable to combining whole-proof and tactic-based generation. Additionally, we show how the dataset quality, training parameters, and sampling diversity affect the final result during automated theorem proving with LLMs. All of our code, datasets, and LLMs are open source.