智能代理定理证明器为何有效：基于统计可证性理论的数学推理模型分析

智能代理定理证明器结合了推理模型、检索、搜索与证明助理验证器，然而仍不清楚哪些组件实际改善了有限预算下的证明成功率，以及它们为何在真实数学工作负载中有效。我们通过统计可证性研究此问题：在给定的定理实例序列上，在预算限制内到达经验证的证明的概率。我们将形式证明搜索建模为有限时段可达 MDP，其确定性验证器动力学下，optimal success probability 与普通语法可证性一致。我们随后分析一条简单但在实际中重要的管线：深度层离线动作价值回归 followed by 贪心测试时证明。我们的主要定理通过占比加权的均匀动作价值误差之和，界定了学习的证明器与 optimal 证明器之间的可证性差距；在常见的均匀误差阅读下，主要复杂度乘子是学习证明器的平均截断证明长度。该误差分解为逼近误差、训练分布的几何覆盖率，以及蒙特卡洛标签噪声，在动作间隙条件下可改善为快速收敛率。该结果在不违反经典最坏情况硬度的前提下，提供了一种对组件敏感的解释，说明为何在偏置定理工作负载上，验证器反馈、检索、表示几何与证明缩短机制有效。