AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
作者: Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H. L. Koppens
分类: quant-ph, cs.AI, cs.LO
发布日期: 2026-09-04
备注: 15 pages, 3 figures. Benchmark available at https://github.com/Axiomatic-AI/AxQM
💡 一句话要点
提出AxQM基准以评估物理领域的形式证明合成
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式证明 量子计算 自动化形式化 物理学基准 Lean库 证明合成 数学形式化
📋 核心要点
- 现有方法在物理学中缺乏足够的形式化，导致理论论证中的理想化未被充分表述，可能造成逻辑漏洞。
- 论文提出AxQM基准，包含1,019个任务，旨在评估物理学中的自动形式化系统，确保每个任务都有解。
- AxQM是物理学中最大的证明合成基准，使用Lean内核进行评分，确保证明的正确性和严谨性。
📝 摘要（中文）
在证明助手中形式化数学，机器检查每个定义、陈述和证明，设立了新的严谨标准。大型语言模型现已能够自主进行形式化，甚至达到整本教科书的规模。我们将这一严谨标准引入物理学，发布AxQM，这是一个包含1,019个可核查的证明合成任务的基准，任务来源于Nielsen和Chuang的《量子计算与量子信息》教科书。AxQM是物理学中最大的证明合成基准，确保每个任务都有解决方案，并通过Lean内核进行确定性评分。
🔬 方法详解
问题定义：论文要解决的问题是物理学中形式化不足的问题，现有方法在理论论证中常常存在逻辑漏洞，影响结果的可靠性。
核心思路：论文的核心思路是通过发布AxQM基准，提供大量可核查的证明合成任务，以评估和推动物理学中的自动形式化系统的发展。
技术框架：AxQM基准包含1,019个任务，基于Nielsen和Chuang的教科书，使用Lean库进行形式化，评分由Lean内核进行，确保每个任务都有解且评分过程透明。
关键创新：最重要的技术创新点在于AxQM是物理学中最大的证明合成基准，任务数量是现有基准的四倍，且每个任务都经过严格的形式化处理。
关键设计：在设计中，任务的评分依赖于Lean内核，确保证明的编译正确性，没有错误声明，并且不引入新的公理。
🖼️ 关键图片
📊 实验亮点
AxQM基准包含1,019个任务，是物理学中最大的证明合成基准，任务数量是现有基准的四倍。评分由Lean内核进行，确保每个任务都有解，且评分过程严格、透明。
🎯 应用场景
该研究的潜在应用领域包括量子计算、量子信息理论及其他物理学领域，能够为自动化证明系统提供标准化的评估基准，推动相关领域的研究和应用发展。未来，AxQM可能成为物理学教育和研究中的重要工具，提升理论物理的严谨性和可靠性。
📄 摘要（原文）
Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.