Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
作者: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu
分类: cs.LO, cs.AI
发布日期: 2025-07-07
备注: Work in progress
💡 一句话要点
提出解耦推理与证明框架，显著提升LLM在IMO难题上的求解能力
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动定理证明 大型语言模型 解耦推理 形式化验证 国际数学奥林匹克 子目标生成 数学推理
📋 核心要点
- 现有自动定理证明器将推理和证明紧耦合，导致模型倾向于浅层策略，限制了深度推理能力。
- 论文提出解耦推理与证明的框架，利用专门的推理器生成子目标引理，再由证明器进行严格验证。
- 实验表明，该框架在极具挑战性的IMO问题集上取得了显著成功，解决了5个之前未被解决的问题。
📝 摘要（中文）
形式语言中的自动定理证明（ATP）是人工智能领域的一项基础性挑战。尽管大型语言模型（LLM）取得了显著进展，但其强大的非形式推理能力与薄弱的形式证明性能之间仍然存在巨大差距。现有研究表明，LLM在非形式化问题上的准确率超过80%，而在PutnamBench等基准测试中的形式化成功率仍低于8%。我们认为，这种差距的根本原因是当前最先进的证明器将推理和证明紧密耦合，导致训练范式无意中惩罚了深度推理，转而支持基于策略的浅层方法。为了弥合这一差距，我们提出了一种新颖的框架，将高层推理与低层证明生成解耦。我们的方法利用两个不同的、专门的模型：一个强大的、通用的推理器来生成多样化的、具有战略意义的子目标引理，以及一个高效的证明器来严格验证它们。这种模块化设计释放了模型的全部推理潜力，并绕过了端到端训练的陷阱。我们在具有挑战性的2000年后的IMO问题集上评估了我们的方法，这是一个之前没有开源证明器报告过成功的问题集。我们的解耦框架成功解决了其中的5个问题，这标志着在自动推理解决极具挑战性的数学问题方面迈出了重要一步。为了促进未来的研究，我们发布了我们生成的和验证的引理的完整数据集，这些引理适用于各种IMO问题，可在https://tencent-imo.github.io/ 上获取。
🔬 方法详解
问题定义：论文旨在解决大型语言模型在形式化数学问题，特别是国际数学奥林匹克（IMO）难题上的自动证明能力不足的问题。现有方法通常采用端到端训练，将推理和证明紧密耦合，导致模型难以进行深度推理，容易陷入浅层策略，无法有效解决复杂问题。
核心思路：论文的核心思路是将推理和证明过程解耦，分别由专门的模块负责。推理模块负责生成有价值的子目标引理，证明模块负责验证这些引理的正确性。这种解耦的设计旨在释放模型的推理潜力，避免端到端训练带来的限制。
技术框架：该框架包含两个主要模块：推理器（Reasoner）和证明器（Prover）。推理器是一个通用的、强大的语言模型，负责生成多样化的、具有战略意义的子目标引理。证明器是一个高效的定理证明器，负责严格验证推理器生成的引理。整个流程是：首先，推理器接收问题描述，生成多个可能的子目标引理；然后，证明器逐一验证这些引理；如果某个引理被证明是正确的，则将其添加到已知事实中，并重复上述过程，直到解决原始问题。
关键创新：该论文最重要的技术创新点在于解耦推理和证明过程。与以往的端到端方法相比，该方法能够更好地利用大型语言模型的推理能力，并避免了端到端训练带来的限制。通过将复杂的证明任务分解为更小的、更易于验证的子目标，该方法能够更有效地解决复杂问题。
关键设计：推理器采用大型语言模型，并使用适当的提示工程来引导其生成有价值的子目标引理。证明器可以使用现有的定理证明器，例如Metamath。论文中没有明确说明具体的参数设置、损失函数或网络结构，这些细节可能取决于所使用的具体模型和证明器。
🖼️ 关键图片
📊 实验亮点
该论文在极具挑战性的2000年后的IMO问题集上进行了评估，这是一个之前没有开源证明器报告过成功的问题集。实验结果表明，该解耦框架成功解决了其中的5个问题，证明了该方法在解决复杂数学问题方面的有效性。这一成果代表着在自动推理领域取得的显著进展。
🎯 应用场景
该研究成果可应用于自动定理证明、数学辅助教育、智能问答系统等领域。通过提升机器在复杂数学问题上的推理和证明能力，可以帮助数学家进行研究，辅助学生学习数学，并构建更智能的数学问题解答系统。此外，该方法还可以推广到其他需要复杂推理和验证的领域，例如软件验证、逻辑推理等。
📄 摘要（原文）
Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .