技术摘要：为何代理定理证明器有效

问题陈述

近期的代理定理证明器结合了大型语言模型（LLM）与检索、搜索及证明助手验证器，在生成已验证的数学证明方面展现了实证成功。然而，现有的理论框架难以解释这一成功。经典证明论关注证明的存在性，而复杂性理论关注最坏情况下的难度。两者均无法充分解释为何特定算法能在固定的计算预算下，针对实践中遇到的特定、有偏的定理分布（例如库定理、基准测试族），以高概率取得成功。

本文探讨的问题是：在指定的定理实例流上，特定代理证明器在固定预算内生成被验证器接受的证明的概率是多少？ 作者认为，理解这种“统计可证性”对于解释为何检索、验证器反馈和分解等组件能提升性能，同时又不与经典不可判定性或最坏情况下界相矛盾，至关重要。

方法论

1. 形式化为可达性马尔可夫决策过程（MDP）

作者将形式化证明搜索建模为具有确定性动态的有限视界可达性马尔可夫决策过程（MDP）：

• 状态（$X$）： 当前的证明义务（例如 Lean 中的开放目标列表）加上验证器反馈。
• 动作（$A$）： 证明器移动，如策略（tactics）、推理规则或检索命令。
• 转移（$F$）： 确定性验证器更新映射 $F: X \times A \to X$。无效动作映射到失败状态；有效动作转移到新的证明状态。
• 目标（$G$）： 已解决状态集合（空目标列表）。

该公式将验证器的操作语义视为转移核。作者证明，在忠实状态抽象下，最优 MDP 成功概率与相同预算内的普通语法可证性完全一致，在保持逻辑完整性的同时实现了统计分析。

2. 统计可证性定义

核心指标是统计可证性（$SP^\pi_B(q_0)$），定义为证明器策略 $\pi$ 在 $B$ 次验证器调用内到达已验证证明的概率，该概率在初始定理分布 $q_0$ 和证明器内部随机性上取平均。这与最优成功概率 $SP^*_B(q_0)$ 形成对比。

作者还追踪平均截断证明长度（$Len^\pi_B(q_0)$），定义为成功前或预算耗尽前的期望验证器调用次数。该指标在其界限中作为关键的可解释性抓手。

3. 学习流程分析

本文分析与当前实践相一致的流程：

1. 离线动作价值回归： 从训练分布上基于验证器支持的 rollout（模拟证明）中学习深度动作价值函数（$Q^*_t$）。
2. 贪婪测试时证明： 在测试时利用学习到的分数贪婪地选择最佳动作。

分析依赖于假设 3.1，该假设提出：

• 紧凑的集中集（$C_t$），训练和测试均在此发生。
• 最优价值函数和假设类的 Lipschitz 连续性。
• 探索分布对状态 - 动作空间具有充分覆盖。
• 每个查询可用多个独立的 rollout 标签以减少噪声。

主要贡献与结果

1. 主定理（统计可证性界限）

核心结果（定理 3.1）界定了学习到的证明器的成功概率与最优证明器的成功概率之间的差距。该界限是均匀动作价值误差的占用加权和：

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

其中：

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ 是学习到的证明器在第 $s$ 步尚未解决问题（未解决质量曲线）的概率。
• $\epsilon_t$ 是深度 $t$ 处学习到的动作价值估计器的均匀误差界。

误差项（$\epsilon_t$）的解释：
误差分解为三个组成部分：

1. 近似误差： 假设类无法表示真实价值函数的能力不足。
2. 覆盖/几何误差： 取决于训练分布的有效局部维度（$d_t$）和覆盖常数（$c_t$）。
3. Rollout 噪声： 用于回归的有限数量蒙特卡洛标签（$m_t$）带来的方差。

2. 平均证明长度的作用

一个关键见解是，界限中的主导复杂度乘数是学习到的证明器的平均截断证明长度（$Len^{\hat{\pi}}_B(q_0)$）。
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
这意味着缩短证明的机制（例如有效的分解、引理引入）能直接降低端到端损失，即使局部价值估计误差（$\bar{\epsilon}_B$）保持不变。

3. 边界条件与快速速率

在边界条件下（即最佳动作与次佳动作价值之间的差距以高概率足够大），界限改善为快速速率：
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
这表明改善动作间隙（使正确动作明显优于错误动作）能显著加速收敛。

4. 缩放定律

本文推导了样本复杂度启发式方法。忽略对数因子，误差按 $n^{-1/(d+2)}$ 缩放，其中 $n$ 是验证器标签预算，$d$ 是有效局部维度。这阐明了“测试时缩放”收益可能源于：

• 减少有效视界（更短的证明）。
• 减少有效几何维度（更好的检索/表示）。
• 增加动作间隙边界。

意义与主张

本文声称提供了关于代理定理证明器为何在有偏负载上有效的组件敏感解释。它通过展示以下内容弥合了经典逻辑与统计学习之间的鸿沟：

1. 验证器反馈： 通过减少近似误差、改善覆盖率和增加动作间隙来提升可证性。
2. 检索与表示： 通过平滑价值函数、将状态空间集中在低维区域以及修剪错误选择以增加边界来发挥作用。
3. 证明缩短： 分解等机制减少了“占用权重”（平均证明长度），这是界限中误差的主要乘数。

作者强调，该理论并不与最坏情况下的难度相矛盾。相反，它解释了为何代理系统能在实践中遇到的特定、结构化的定理分布（库定理、基准测试）上取得成功，因为在这些场景中证明较短、间隙较大且覆盖良好。该框架将验证器视为信息通道，将证明器视为在有限预算下提取有用信息的统计学习器，为现代代理系统中普遍存在的工程选择（检索、分解、验证器循环）提供了严格的理由。