用大模型指导专用证明器，效率提升25倍且准确率微增。
ProofCompass: Enhancing Specialized Provers with LLM Guidance
- 用大模型提供自然语言策略和失败分析，指导专用证明器。
- miniF2F上准确率从54.9%升至55.3%，尝试次数降至128次（原3200）。
- 无需训练新模型，适合资源受限的定理证明研究者。
语言模型在形式化数学推理中日益强大。然而，现有方法多依赖通用大模型或小型专用模型，各有局限；而训练专用大模型仍需大量计算资源。本文提出ProofCompass，一种新型混合方法：通过大型语言模型（LLM）指导现有专用证明器（如DeepSeek-Prover-v1.5-RL，简称DSP-v1.5），无需额外训练。LLM提供自然语言证明策略并分析失败尝试，选择中间引理实现有效问题分解。在miniF2F基准上，ProofCompass显著提升计算效率：准确率从54.9%提升至55.3%，尝试次数从3200次降至128次（减少25倍）。该协同方法为形式化定理证明中同时提升效率与精度开辟新路径。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。