AxQM：一个面向有限维量子力学库中形式化证明合成的教科书规模基准

在证明助手中将数学形式化，由机器检查每个定义、命题和证明，已经树立了严谨性的新标准。大型语言模型如今也能够自主进行形式化，甚至达到整本教科书的规模。我们将这一严谨标准引入物理学，因为理论论证中包含的理想化假设往往没有被完整陈述，而任何逻辑缺口都可能对相互依赖的结果产生连锁影响。鉴于需要评估物理领域的自动形式化系统，我们发布 AxQM：这是一组由 479 个条目构成的 1,019 个可由 kernel 检查的证明合成任务，取材自 Nielsen 和 Chuang 的教材 Quantum Computation and Quantum Information。任务以一个自定义的 Lean 有限维量子力学库表述。按任务数量计算，它是物理领域规模最大的证明合成基准，大约是现有基准的四倍。AxQM 源自该教材形式部分的近乎完整形式化，因此每个任务都保证有解，而这些解我们保密。该基准的评分由 Lean kernel 确定性完成，它会检查证明是否能编译、其中或其依赖的任何声明中是否出现 sorry，以及是否引入了新的公理。