Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
作者: Joshua Ong Jun Leang, Haonan Li, Zheng Zhao, Xinyi Shang, Wenda Li, Zhengzhong Liu, Erix Xing, Shay Cohen, Eleonora Giunchiglia
分类: cs.AI
发布日期: 2026-09-10
备注: 9 pages, preprint
💡 一句话要点
提出Magenta以解决数学推理与形式验证之间的鸿沟问题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 数学推理 形式验证 大型语言模型 机器检查 自动化定理证明 Lean 4 智能管道
📋 核心要点
- 现有的大型语言模型在非正式数学推理中表现出色，但无法利用机器的离散验证能力，导致推理的准确性不足。
- 论文提出Magenta，通过将Lean信号集成到非正式推理过程中，构建一个无训练的智能管道，能够自动生成机器检查的数学证明。
- Magenta在多个奥林匹克基准测试中实现了100%的准确率，并成功解决了IMO 2026的所有问题，显示出其强大的推理能力。
📝 摘要（中文）
大多数数学知识通过非正式的数学和自然语言进行传达。尽管大型语言模型在非正式数学推理中表现良好，但仍存在不足。本文提出Magenta，一个无训练的智能管道，能够将自然语言问题转化为Lean 4语句并构建机器检查的证明。Magenta在所有评估的奥林匹克基准中实现了100%的准确率，并在与K2-Horizon-7B推理器配对时解决了所有IMO 2026问题。分析表明，语句裁定对防止虚假证书至关重要，而反馈引导的修正优于独立重采样。
🔬 方法详解
问题定义：本文旨在解决大型语言模型在非正式数学推理中无法利用机器验证能力的问题，导致推理结果的准确性不足。
核心思路：Magenta通过将Lean信号集成到非正式推理过程中，创建一个无训练的智能管道，能够将自然语言问题转化为Lean 4语句并生成机器检查的证明。
技术框架：Magenta的整体架构包括三个主要模块：自然语言问题解析、Lean语句生成和机器检查证明构建。首先解析自然语言问题，然后生成相应的Lean语句，最后构建并验证机器检查的证明。
关键创新：Magenta的核心创新在于将非正式推理与形式验证结合，通过语句裁定和错误归因机制，确保生成的证明保持原问题的准确性，避免虚假证书的产生。
关键设计：在设计中，语句裁定者用于验证形式化是否保留了原问题，而错误归因者则将失败的尝试引导至数学重新推导或局部Lean修复，确保系统的高效性和准确性。
🖼️ 关键图片
📊 实验亮点
Magenta在所有评估的奥林匹克基准中实现了100%的准确率，特别是在与K2-Horizon-7B推理器配对时，成功解决了所有六个IMO 2026问题。这表明其在复杂数学推理中的强大能力和可靠性。
🎯 应用场景
该研究的潜在应用领域包括教育、自动化定理证明、数学研究等。Magenta可以帮助学生和研究人员更高效地进行数学推理和验证，提升数学问题解决的准确性和效率，未来可能在智能教育和自动化工具中发挥重要作用。
📄 摘要（原文）
Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.