Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
作者: Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao, Lihong Zhi, Ruyong Feng
分类: cs.CL
发布日期: 2026-03-25
💡 一句话要点
Mechanic：基于Sorry驱动的形式化分解工作流，提升自动定理证明效率
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动定理证明 形式化分解 大型语言模型 Lean证明环境 Sorry驱动 数学推理 Agent系统
📋 核心要点
- 现有自动定理证明系统在处理复杂数学问题时，常因推理失败而效率低下，要么完全重构，要么反复修复导致上下文过长。
- Mechanic 采用 sorry 驱动的形式化分解策略，利用 Lean 的 sorry 占位符隔离未解决子目标，独立解决。
- 在 IMO 2025 和 Putnam 2025 等数学竞赛基准测试中，Mechanic 显著提升了定理证明的效率。
📝 摘要（中文）
大型语言模型（LLMs）和基于LLM的Agent在自动定理证明方面取得了显著进展。然而，对于需要复杂数学推理的问题，现有系统通常难以一次成功，需要反复修改证明策略。现有的处理失败尝试的方法要么丢弃整个证明并从头开始重新生成，要么迭代地修复证明中的错误。前者效率低下，因为它可能因为局部错误而放弃大部分正确的推理；而后者虽然保留了先前的进展，但会导致上下文长度逐渐增加，从而降低模型关注剩余未解决子问题的能力。为了解决这个困境，我们提出了Mechanic，一种新颖的Agent系统，它采用了一种sorry驱动的形式化分解策略。通过利用Lean中的sorry占位符来精确地隔离未解决的子目标，同时保留周围已验证的证明结构，Mechanic将每个失败的子问题提取到一个干净的、自包含的上下文中，并独立地解决它。这避免了完全重新生成的浪费和重复修复引起的过度上下文长度。在具有挑战性的数学竞赛基准（包括IMO 2025和Putnam 2025）上的实验结果表明，我们的Agent在证明效率方面取得了显著优势。
🔬 方法详解
问题定义：现有基于LLM的自动定理证明方法在处理复杂数学问题时，面临效率和上下文管理的挑战。完全重构浪费计算资源，而迭代修复则导致上下文长度线性增长，降低模型对未解决子问题的关注能力。现有方法难以在保证推理正确性的同时，有效利用已有的推理成果。
核心思路：Mechanic的核心思路是“分而治之”，将复杂的定理证明问题分解为更小的、独立的子问题。通过 Lean 证明环境中的 sorry 占位符，系统能够精确地识别和隔离未解决的子目标，并将其提取出来，形成一个独立的、自包含的证明上下文。这种分解策略避免了对整个证明过程的重复计算，并有效控制了上下文长度。
技术框架：Mechanic 的整体框架包含以下几个主要阶段：1) 问题分解：利用 Lean 的 sorry 占位符识别未解决的子目标。2) 上下文提取：将每个未解决的子目标提取到一个独立的上下文中，保留相关的定义和假设。3) 独立求解：使用 LLM-based agent 独立地解决每个子问题。4) 结果集成：将解决后的子问题证明集成回原始证明中，替换相应的 sorry 占位符。
关键创新：Mechanic 的关键创新在于其 sorry 驱动的形式化分解策略。与传统的重构或迭代修复方法不同，Mechanic 能够精确地定位和隔离未解决的子问题，从而避免了不必要的计算和上下文膨胀。这种分解策略使得系统能够更有效地利用已有的推理成果，并专注于解决剩余的难题。
关键设计：Mechanic 的关键设计包括：1) 使用 Lean 作为形式化证明环境，利用其强大的类型系统和证明工具。2) 设计专门的 prompt 模板，用于将子问题及其上下文传递给 LLM-based agent。3) 实现自动化的证明集成机制，将解决后的子问题证明无缝地集成回原始证明中。具体的参数设置、损失函数和网络结构取决于所使用的 LLM-based agent。
🖼️ 关键图片
📊 实验亮点
Mechanic 在 IMO 2025 和 Putnam 2025 等具有挑战性的数学竞赛基准测试中表现出色，证明了其在提升自动定理证明效率方面的显著优势。具体性能数据和对比基线未在摘要中给出，但强调了其在证明效率上的“显著优势”。
🎯 应用场景
Mechanic 有潜力应用于自动化数学研究、形式化验证、软件工程等领域。它可以帮助数学家更高效地探索新的定理，并辅助工程师验证软件和硬件系统的正确性。未来，该技术有望扩展到其他需要复杂推理和证明的领域，例如人工智能安全和智能合约验证。
📄 摘要（原文）
Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems requiring complex mathematical reasoning, current systems rarely succeed on the first try and must repeatedly modify their proof strategies. Existing approaches for handling failed attempts typically either discard the entire proof and regenerate it from scratch or iteratively fix errors within the proof. The former is inefficient, as it may abandon mostly correct reasoning due to localized errors, while the latter, although preserving prior progress, leads to progressively longer contexts which progressively degrades the model's ability to attend to the remaining unresolved subproblems. To address this dilemma, we propose Mechanic, a novel agent system that employs a sorry-driven formal decomposition strategy. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, Mechanic 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 and Putnam 2025, demonstrate that our agent achieves significant advantages in proving efficiency.