🤖 machine learning

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

本文表明，选择公理在神经证明嵌入中留下了可测量的几何特征——其特征表现为随着证明在依赖图中远离该公理，异常得分和重构损失也随之下降——这与并预测了像 Lean 4 这样的系统中构造性定理证明与经典定理证明之间的性能差异。

原作者： Rodrigo Mendoza-Smith

发布于 2026-06-30✓ Author reviewed ⓘ

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Rodrigo Mendoza-Smith

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一个名为 Mathlib 的庞大且古老的图书馆。这个图书馆包含了近五十万条数学证明，它们全部是用一种严格的、计算机可读的语言——Lean 编写的。一个多世纪以来，数学家们一直在争论关于构建这些证明的两种不同方式：

构造性证明 (Constructive Proofs)： “乐高”法。如果你声称一座建筑存在，你必须展示如何一步步地用砖块将其搭建出来。
经典证明 (Classical Proofs)： “魔法”法。你可以仅仅通过说“它不可能不存在”来声称一座建筑存在，而无需展示如何建造它。这依赖于一条被称为选择公理 (Axiom of Choice) 的规则。

长期以来，人们认为这仅仅是哲学上的分歧。然而，本文指出，这些实际上是几何上的差异，你可以像测量地图上两个城市之间的距离一样去测量它们。

以下是作者如何发现这一点的，使用了简单的类比：

1. 魔法规则的“回声”

作者将这个图书馆视为一个巨大的回声室。他们训练了一个“计算机大脑”（AI），但这个大脑仅学习了“乐高”（构造性）证明。AI 学习了这些证明的节奏、风格和结构。它成为了识别什么是“正常”构造性证明的专家。

然后，他们向它输入了“魔法”（经典）证明。

结果： AI 不仅仅是说“这很不同”。它测量了有多不同。
类比： 想象你是一位只听过古典钢琴曲的音乐老师。如果你听到一首爵士乐，你可能会说：“这听起来很怪。”但如果你听到一首使用了非常特定、罕见乐器的现代爵士乐，它听起来可能比一首百年前创作的爵士乐显得没那么奇怪。

2. “深度”定律

作者意识到，并非所有的“魔法”证明都具有同等的魔力。

浅层深度 (距离 1-2)： 这些证明直接使用“魔法规则”（选择公理）。它们就像是在开头就使用了那种奇怪乐器的爵士乐。对于 AI 来说，它们听起来非常奇怪且“格格不入”。
深层深度 (距离 9+)： 这些证明在很久以前、深埋在其他引理链条之中时就使用了“魔法规则”。证明本身看起来非常像是一个“乐高”证明。对于 AI 来说，它们听起来几乎很正常。

发现： 存在一个平滑的梯度。当你远离“魔法规则”的直接使用时，证明会开始看起来并听起来更像标准的“乐高”证明。“陌生感”随之消退。作者称之为深度定律 (Depth Law)。

3. 三种测量“陌生感”的方法

论文使用了三种不同的“尺子”来测量这种距离，并且它们的结果是一致的：

异常评分 (The Anomaly Score)： 这个证明距离最近的“乐高”证明有多远？（就像测量一个爵士音符距离一个钢琴音符有多远）。
重构损失 (The Reconstruction Loss)： 如果 AI 尝试预测“魔法”证明的下一步，它出错的频率是否比处理“乐高”证明时更高？（就像老师预测句子中的下一个词；他们在处理“魔法”句子时会感到更加吃力）。
密度检查 (The Density Check)： 这个证明是生活在拥挤的“乐高”社区里，还是迷失在空旷的“魔法”荒野中？

这三把尺子都显示了相同的模式：“魔法”证明在靠近源头时非常独特，但随着远离源头，它们会逐渐融入其中。

4. “机器人求解器”测试

这篇论文最实用的部分涉及到一个名为 Aesop 的机器人，它试图自动解决这些数学问题。

问题： 机器人擅长解决“乐高”证明（成功率为 20%），但处理“魔法”证明时表现糟糕（仅为 1.5%）。它就像一个能用积木盖房子，但在面对魔法咒语时会感到困惑的机器人。
转折： 作者尝试通过给机器人一个“神经引导”（一个建议第一步动作的智能助手）来帮助它。
结果： 这个引导起了一点作用，但它并没有解决问题。即使在“魔法”证明看起来非常像“乐高”证明时，机器人仍然在处理它们时感到极其困难。

核心结论： 尽管随着远离源头，“魔法”证明看起来越来越像“乐高”证明，但机器人求解器仍然认为它们非常困难。这表明，即使证明在表面上看起来再“正常”，“魔法”规则也会在证明中留下永久且隐形的伤痕，使得当前的计算机难以求解。

总结

本文证明了选择公理不仅仅是一个哲学概念；它在数学证明上留下了可测量的、几何上的指纹。

直接使用该规则会让证明在 AI 看来显得非常“异类”。
间接使用则会让证明看起来更“正常”。
然而，即使它们看起来很“正常”，自动化求解器在处理它们时仍然比处理纯构造性证明要困难得多。

这就像是发现，虽然一座用“魔法砖”建造的房子从外面看可能与用“普通砖”建造的房子完全一样，但如果你试图用标准的工具箱去维修它，那些魔法砖依然会带来麻烦。

技术摘要：神经证明嵌入中选择公理的几何度量

问题陈述

选择公理（AC）在历史上将数学基础划分为经典派和构造派，这种区别在很大程度上仍停留在哲学和方法论层面。虽然经典证明利用了 AC 允许的非构造性捷径，而构造证明则需要显式的见证者（witnesses），但目前尚不清楚这两类范式是否存在超出简单公理依赖关系之外、可在结构上被检测到的差异。本文研究了选择公理是否在形式化证明的空间内（特别是在 Lean 4 Mathlib 库中）留下了一个可测量的“几何签名”，以及该签名对于神经定理证明器是否具有操作层面的影响。

研究方法

数据划分与依赖追踪

作者利用 Lean 4 的内核级依赖追踪功能对 Mathlib 库进行划分，该库包含 471,260 个经过机器认证的声明。通过在依赖图上执行广度优先搜索，他们将声明分为两类：

经典证明： 传递依赖于 Classical.choice 的证明。
构造证明： 不依赖于上述内容的证明。

经典证明的“距离”被定义为该证明到 Classical.choice 的最短依赖链长度。这创建了一个分层数据集，其中证明根据其相对于公理的深度进行分组。本研究聚焦于一个经过筛选的群体，包含 42,355 个定理（31,144 个经典，11,211 个构造），其策略轨迹（tactic traces）步数在 2 到 200 步之间。

无标签表示学习

为了在不引入偏差的情况下测量这些证明的几何属性，作者专门在构造证明上训练了一个自监督去噪自动编码器。

输入： 证明被表示为策略头（tactic heads，例如 intro, rw, simp）的序列，丢弃了具体的参数，以专注于证明的组合结构。
架构： 一个 4 层 Transformer 编码器配对一个 2 层解码器。模型旨在从输入序列中重建被掩码处理的策略标记（20% 的损坏率）。
嵌入： 证明嵌入是编码器隐藏状态（排除填充部分）的均值，并归一化到单位球面上。
无标签约束： 编码器在训练、词表构建或超参数选择过程中从未见过经典证明。经典证明仅作为用于测量的留出群体（held-out population）。

几何度量

研究使用了三种互补的指标来衡量经典证明相对于构造训练分布的偏离程度，并将其作为函数考察其对依赖深度的响应：

异常得分（k-NN）： 与 $k$ 个最近的构造邻居之间的欧几里得距离。
重构损失： 当受构造训练的模型尝试预测经典证明中被掩码的标记时所产生的交叉熵损失。
密度超水平集包含度： 落在构造训练分布的高密度区域（超水平集）之外的经典证明比例。

操作性评估

研究通过两个系统评估了几何发现对定理证明性能的影响：

aesop： 一个符号化的最佳优先搜索证明器。
混合系统（ReProver + aesop）： 一种神经引导的方法，由策略生成器提出第一步动作，随后由 aesop 接手。

核心结果

深度定律

主要发现是存在一个“深度定律”：经典证明与构造证明之间的几何差异随其与 Classical.choice 的距离而呈现可预测的衰减。

浅层深度下的显著分离： 在深度为 2（直接调用经典引理的证明）时，分离现象非常显著。k-NN 异常得分的 AUC 达到 0.847，重构损失比构造基准高出 34.5%，且有 43% 的经典证明落在构造 90% 密度区域之外。
向不可区分性衰减： 随着深度增加，各项指标向构造基准收敛。到深度 9 或更高时，所有三项指标都趋于随机水平（AUC $\approx$ 0.5，损失 $\approx$ 基准，包含度 $\approx$ 90%），使得深层经典证明在几何上与构造证明无法区分。
单参数混合定律： 作者将这种梯度建模为两个分布的混合：构造分布 $P$ 和直接相关的经典分布 $R$ 。深度为 $d$ 的分布 $Q_d$ 被建模为 $Q_d = (1 - \lambda_d)P + \lambda_d R$ ，其中 $\lambda_d$ 是随深度递减的混合权重。通过归一化处理后，三种不同的测量指标合并为一条曲线，支持了这一单参数定律。

鲁棒性控制

该特征对以下潜在混淆变量具有鲁棒性：

关键词： 移除显式的经典策略标记（如 classical, by contra）仅轻微降低了深度-2 的 AUC（从 0.847 降至 0.754），表明该信号是结构性的而非仅仅是词汇性的。
长度： 对嵌入进行长度残差化处理后，梯度依然存在。
作者/文件/主题： 控制作者、文件和数学子领域的混合效应模型证实，该信号在特定上下文中依然存在。
陈述 vs. 证明： 定理陈述显示的深度梯度远弱于证明（陈述的聚合 AUC 为 0.604，而证明的聚合 AUC 为 0.675），这证实了该信号主要是组合性的（证明结构）而非主题性的（定理内容）。
公理特异性： 虽然 propext 和 Quot.sound 也显示出深度梯度，但 Classical.choice 产生的梯度最为陡峭，表明其具有独特的运算耦合性。

操作性后果

几何签名与证明器性能相关：

aesop 失效： aesop 解决了 20.0% 的构造定理，但仅解决了 1.5% 的经典定理（存在 13 倍的差距）。与几何信号不同，这种操作差距并未随深度平滑，即无论距离公理多远，经典证明对 aesop 而言始终难以处理。
神经引导： 加入神经策略生成器（ReProver）将差距缩小至约 5 倍（22.0% vs 4.5%），但未能完全消除。
预测能力： 异常得分比单纯的证明长度能更好地预测 aesop 的失败情况（加入异常得分后，AUC 从 0.766 提升至 0.841）。

意义与主张

本文声称提供了第一个关于选择公理在证明空间中具有可测量几何相关性的经验证据。作者认为：

结构性区别： 经典/构造之争不仅是一种哲学立场，也是证明组合中的一种结构属性，这在神经嵌入中是可见的。
操作相关性： 这种几何签名并非抽象的奇谈，它能预测自动化定理证明器的性能。“深度定律”表明，随着证明远离公理，它们在结构上变得更接近构造证明，但对于像 aesop 这样的符号证明器而言，由于 Classical.choice 的存在，操作障碍依然存在。
方法论贡献： 本研究展示了在单一类别（构造证明）上进行的无标签、自监督学习，如何揭示由逻辑依赖定义的另一类持有类（经典证明）的结构边界，为元数学分析提供了一种新工具。

作者对因果机制保持审慎，指出虽然几何签名与操作差距之间存在强关联，但导致证明器困难的具体原因（是结构性障碍还是规则集配置问题）仍需进一步研究。这项工作旨在邀请社区去识别形式化库中类似的结构轴线。