用自动验证器让大模型辅助数学定理证明，效果显著提升。
MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
- 将数学基准miniF2F移植到Dafny自动验证器，实现高阶推理指导与底层自动化结合。
- 最佳模型Claude Opus 4.6在完整测试集上达62.7% pass@4，比空证明基线高23.8个百分点。
- 适合研究AI辅助数学推理、形式化验证或想用大模型做定理证明的学者。
大语言模型（LLMs）擅长推理，但其步骤验证仍具挑战性。形式化验证通过可机械检查的证明提供解决方案。交互式定理证明器（ITPs）主导数学推理，但需详尽低层证明步骤；自动-主动验证器虽具自动化优势，但多用于软件验证。近期工作已尝试在ITPs中评估LLMs用于软件验证，但将LLMs用于自动-主动验证器中的数学定理证明仍属空白。本文提出MINIF2F-DAFNY，首次将广泛使用的数学基准miniF2F迁移至自动-主动验证器Dafny。结果显示，仅靠Dafny自动化即可解决39%-44%的问题（空证明），而许多问题在ITPs中需大量证明引导。我们在8个现成的LLMs上评估了证明生成能力，最佳模型（Claude Opus 4.6）在完整测试集上达到62.7%的cumulative pass@4，较38.9%的空证明基线提升23.8个百分点。结果表明，自动-主动验证为人工智能辅助数学推理提供了互补的实证场景：大模型提供高层指导，SMT自动化处理底层细节。我们的基准与评估基础设施已开源：https://github.com/dafny-lang/miniF2F。
原文摘要 · Abstract (English)
LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (ITPs) dominate mathematical reasoning but require detailed low-level proof steps, while auto-active verifiers offer automation but focus on software verification. Recent work has begun bridging this divide by evaluating LLMs for software verification in ITPs, but the complementary direction, LLMs for mathematical theorem proving in auto-active verifiers, remains unexplored. We present MINIF2F-DAFNY, the first translation of the widely-used mathematical benchmark miniF2F to an auto-active verifier: Dafny. We find that Dafny's automation alone solves 39-44% of problems with empty proofs, whereas many require substantial proof guidance in ITPs. We evaluate 8 off-the-shelf LLMs on proof generation, with the best model (Claude Opus 4.6) achieving 62.7% cumulative pass@4 on the full test set, improving over the 38.9% empty-proof baseline by 23.8 percentage points. These results show that auto-active verification offers a complementary empirical setting for AI-assisted mathematical reasoning, where LLMs provide high-level guidance while SMT automation handles low-level details. Our benchmark and evaluation infrastructure are publicly available on https://github.com/dafny-lang/miniF2F.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。