用智能分解法解决数学定理证明中反复失败的问题
MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
- 引入抱歉占位符，将未完成的证明目标拆解为独立模块
- 在IMO2025等竞赛题上证明成功率显著提升
- 适合需要复杂数学推理的自动化证明研究者
大型语言模型（LLM）及其代理系统在自动化定理证明方面取得显著进展。然而，对于需要复杂数学推理的问题，当前系统往往首次尝试即失败，需迭代调整证明策略。现有方法要么逐次修复证明中的错误，导致上下文过长、影响模型对未解决问题的关注；要么彻底放弃并从头重来，浪费大量已正确推导的内容。为解决这一困境，我们提出MechMath，一个基于抱歉占位符（Sorrifier）驱动的形式化分解框架。通过在Lean中使用sorry占位符精确隔离未解决的子目标，同时保留周围已验证的证明结构，MechMath将每个失败的子问题提取为独立且自包含的上下文，并单独求解。该方法既避免了完全重生成的低效，也防止因重复修补导致的上下文膨胀。在挑战性数学竞赛基准测试（包括IMO 2025、Putnam 2025、miniF2F以及ProverBench的一个子集）上的实验结果表明，该代理系统在证明效率上具有显著优势。
原文摘要 · Abstract (English)
Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require complex mathematical reasoning, current systems seldom succeed in their initial attempt, necessitating iterative adjustments to their proof strategies. Existing approaches for handling failed attempts typically either iteratively fix errors within the proof or discard the entire proof and regenerate it from scratch. The former leads to progressively longer contexts, which degrade the model's ability to attend to the remaining unresolved subproblems, while the latter is inefficient, as it may abandon mostly correct reasoning due to localized errors. To address this dilemma, we present MechMath, an agent system centered on a Sorrifier-driven formal decomposition paradigm. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, MechMath extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025, Putnam 2025, miniF2F, and a subset of ProverBench, demonstrate that our agent achieves significant advantages in proving efficiency.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。