发表机构
Axiomatic AI; Institut de Ciències Fotòniques (ICFO); Massachusetts Institute of Technology (MIT); Institució Catalana de Recerca i Estudis Avançats (ICREA)（Axiomatic AI; 光子科学研究所; 麻省理工学院; 加泰罗尼亚研究与高级研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究发布了AxQM，这是物理学领域规模最大的教科书级证明综合基准，含1019个任务，用于评估自动形式化系统，所有任务保证有解且由Lean内核确定性评分。
AI 中文摘要
在证明助手（一种可检查所有定义、命题和证明的机器）中对数学进行形式化，已树立了严谨性的新标准。大型语言模型如今已能自主进行形式化，甚至达到整本书的规模。我们将这种严谨性标准引入物理学领域，物理学中的理论论证常带有未完全明确的理想化假设，任何逻辑漏洞都可能对相互关联的结果产生级联效应。鉴于需要评估物理学领域的自动形式化系统，我们发布了AxQM——一个基于尼尔森和庄的教科书《量子计算与量子信息》中479个条目生成的1019个可由内核检查的证明综合任务。这些任务用自定义的有限维量子力学Lean库表述。按任务数量计算，它是物理学领域最大的证明综合基准，规模是同类基准的四倍。AxQM源自该教科书形式化部分的近乎完整形式化，因此每个任务都保证有解决方案，而这些解决方案我们暂不公开。该基准的评分由Lean内核确定性地完成，内核会检查证明是否可编译、证明及其依赖的任何声明中是否无sorry（占位符），以及是否未引入新公理。
英文摘要
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.
Comments15 pages, 3 figures. Benchmark available at https://github.com/Axiomatic-AI/AxQM
