ProofCompass: Enhancing Specialized Provers with LLM Guidance

📄 arXiv: 2507.14335v1 📥 PDF

作者: Nicolas Wischermann, Claudio Mayrink Verdun, Gabriel Poesia, Francesco Noseda

分类: cs.AI

发布日期: 2025-07-18

备注: 19 pages, 7 figures. Accepted at the 2nd AI for MATH Workshop at the 42nd International Conference on Machine Learning (ICML 2025)

💡 一句话要点

ProofCompass：利用LLM指导，高效提升专业定理证明器性能

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

关键词: 形式化定理证明 大型语言模型 专业证明器 策略指导 计算效率

📋 核心要点

  1. 现有形式化数学推理方法依赖于大型通用模型或小型专用模型，前者计算成本高昂，后者能力有限。
  2. ProofCompass利用LLM提供证明策略和失败分析，指导专业证明器选择中间引理，实现问题分解。
  3. 实验表明，ProofCompass在计算资源消耗大幅降低的同时，性能超越了现有专业证明器。

📝 摘要（中文）

本文提出了一种名为ProofCompass的混合方法，旨在通过大型语言模型（LLM）策略性地指导现有的专业证明器方法（如DeepSeek-Prover-v1.5-RL (DSP-v1.5)），从而在无需额外模型训练的情况下实现显著的计算效率提升。LLM提供自然语言证明策略，并分析失败的尝试以选择中间引理，从而实现有效的难题分解。在miniF2F基准测试中，ProofCompass展示了卓越的资源效率：在尝试次数减少25倍（3200次降至128次）的情况下，性能超越了DSP-v1.5（54.9%提升至55.3%）。这种协同方法为同时提高形式化定理证明的计算效率和准确性铺平了道路。

🔬 方法详解

问题定义：论文旨在解决形式化定理证明中计算效率和模型能力之间的矛盾。现有方法要么依赖计算成本高昂的大型通用语言模型，要么使用能力受限的小型专用模型。训练大型专用模型需要大量的计算资源，而小型专用模型在复杂问题上表现不佳。因此，如何在有限的计算资源下，提升专业证明器在复杂定理证明任务上的性能是一个关键问题。

核心思路：ProofCompass的核心思路是利用大型语言模型（LLM）的推理能力来指导现有的专业证明器。LLM负责提供高层次的证明策略，并分析证明失败的原因，从而引导专业证明器选择合适的中间引理。这种方法结合了LLM的推理能力和专业证明器的计算效率，从而在计算资源有限的情况下，提升了证明性能。

技术框架：ProofCompass的整体框架包含以下几个主要模块：1) LLM策略生成器：利用LLM生成自然语言的证明策略。2) 失败分析器：分析专业证明器证明失败的原因，并提供改进建议。3) 中间引理选择器：根据LLM提供的策略和失败分析结果，选择合适的中间引理。4) 专业证明器：使用选择的中间引理进行定理证明。整个流程是迭代进行的，LLM不断根据专业证明器的反馈调整策略，直到证明成功或达到最大尝试次数。

关键创新：ProofCompass的关键创新在于将LLM的推理能力与专业证明器的计算效率相结合。与现有方法相比，ProofCompass不需要训练新的大型模型，而是利用现有的LLM和专业证明器，通过策略指导的方式提升证明性能。这种方法显著降低了计算成本，并提高了证明的效率。

关键设计：论文中没有明确给出关键的参数设置、损失函数、网络结构等技术细节。LLM的选择和prompt的设计是关键，但具体细节未知。中间引理的选择策略也至关重要，但论文中没有详细描述。专业证明器采用DeepSeek-Prover-v1.5-RL，其具体结构和参数设置也未在论文中详细说明。

🖼️ 关键图片

img_0

📊 实验亮点

ProofCompass在miniF2F基准测试中表现出色，在尝试次数减少25倍（3200次降至128次）的情况下，性能超越了DeepSeek-Prover-v1.5-RL（54.9%提升至55.3%）。这一结果表明，ProofCompass在计算资源效率方面具有显著优势，能够在有限的计算资源下，有效提升专业证明器的性能。

🎯 应用场景

ProofCompass方法具有广泛的应用前景，可应用于自动化定理证明、程序验证、智能合约安全审计等领域。通过结合LLM的推理能力和专业工具的计算效率，可以显著提升这些领域的自动化水平和效率。未来，该方法有望应用于更复杂的数学问题和软件系统，推动相关领域的发展。

📄 摘要（原文）

Language models have become increasingly powerful tools for formal mathematical reasoning. However, most existing approaches rely exclusively on either large general-purpose models or smaller specialized models, each with distinct limitations, while training specialized large models still requires significant computational resources. This paper introduces ProofCompass, a novel hybrid methodology that achieves remarkable computational efficiency by strategically guiding existing specialized prover methods, such as DeepSeek-Prover-v1.5-RL (DSP-v1.5) with a Large Language Model (LLM) without requiring additional model training. The LLM provides natural language proof strategies and analyzes failed attempts to select intermediate lemmas, enabling effective problem decomposition. On the miniF2F benchmark, ProofCompass demonstrates substantial resource efficiency: it outperforms DSP-v1.5 ($54.9\% \rightarrow 55.3\%$) while using 25x fewer attempts ($3200 \rightarrow 128$). Our synergistic approach paves the way for simultaneously improving computational efficiency and accuracy in formal theorem proving.