神经证明嵌入中选择公理的几何测量

一个多世纪以来，选择公理一直划分着数学的基础，但经典证明和构造性证明之间的区别仍然是哲学和方法论上的区别。我们使用 Lean 4 的公理依赖性的内核级跟踪来表明，选择的公理在证明空间中具有可测量的几何相关性，遵循单参数混合定律，并对神经定理证明者具有操作结果。为此，我们通过对选择公理的传递依赖性来划分 Mathlib 的 $471{,}260$ 声明，并通过策略调用序列表示经过过滤的 $42{,}355$ 追踪定理群体。我们使用该数据集中的构造性证明来训练自监督证明编码器，并表明，当使用它来测量经典证明时，三个互补测量（异常分数、重建损失和密度超级包含）随着证明与依赖图中公理的距离呈现出共同下降，从浅边界处的急剧分离（距离 $2$ 处的 AUC $0.847$）到距离〜$9{+}$ 处的不可区分性。鲁棒性控制表明，签名能够经受住长度、文件、作者和主题控制，并在经过标准化证明源训练的全源编码器下进行复制。在操作上，我们表明，在 $251$ Mathlib 定理的评估样本上，Lean 的 \texttt{aesop} 策略以经典定理的 $13\times$ 的速度求解构造性定理，并且使用 ReProver 策略生成器的神经引导混合将差距压缩到 $5\times$。几何异常分数预测超出证明长度的 \texttt{aesop} 失败，从而提供几何签名和证明者性能之间的操作联系。