解释智能定理证明器为何有效，揭示其成功背后的统计可证性机制。
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
- 将证明搜索建模为带确定验证器的马尔可夫决策过程，分析最优成功率与语法可证性的关系。
- 证明学习型证明器与最优证明器之间的可证性差距受平均截断证明长度和误差项影响。
- 揭示验证反馈、检索和证明缩短机制如何提升在偏置题集上的表现，适合形式化推理研究者。
智能定理证明器结合推理模型、检索、搜索与证明助手验证器，但其各组件对有限预算下证明成功率的实际贡献仍不清晰。本文通过统计可证性——即在特定定理实例流中，于预算内达到已验证证明的概率——来研究该问题。我们将形式化证明搜索建模为具有确定性验证器动态的有限时域可达性马尔可夫决策过程，并证明在忠实状态抽象下，最优成功概率等于普通语法可证性。随后分析一种简单但实际重要的流程：深度优先离线动作价值回归后接贪婪测试时证明。主要定理表明，学习型证明器与最优证明器间的可证性差距由占用加权的统一动作价值误差之和界定；在常见均匀误差假设下，主导复杂度乘子为学习型证明器的平均截断证明长度。误差分解为近似误差、训练分布几何覆盖度及蒙特卡洛标签噪声，在动作间隙边缘条件下可实现快速收敛。结果为验证反馈、检索、表示几何与证明缩短机制为何在偏置定理工作负载上有效提供了组件敏感的解释，且不违背经典最坏情况难解性。
原文摘要 · Abstract (English)
Agentic theorem provers combine a reasoning model, retrieval, search, and a proof assistant verifier, yet it remains unclear which components actually improve finite-budget proof success and why they help on real mathematical workloads. We study this question through statistical provability: the probability of reaching a verified proof within a budget on a specified stream of theorem instances. We model formal proof search as a finite-horizon reachability MDP with deterministic verifier dynamics, and show that under a faithful state abstraction the optimal success probability coincides with ordinary syntactic provability. We then analyze a simple but practically important pipeline: depth-wise offline action-value regression followed by greedy test-time proving. Our main theorem bounds the provability gap between the learned prover and the optimal prover by an occupancy-weighted sum of uniform action-value errors; in the common uniform-error reading, the leading complexity multiplier is the learned prover's average truncated proof length. The error decomposes into approximation error, geometric coverage of the training distribution, and Monte Carlo label noise, and improves to a fast rate under an action-gap margin condition. The result gives a component-sensitive account of why verifier feedback, retrieval, representation geometry, and proof-shortening mechanisms help on biased theorem workloads, without contradicting classical worst-case hardness.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。