Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models

• URL: http://arxiv.org/abs/2602.10538v2
• Date: Thu, 12 Feb 2026 19:27:06 GMT
• Title: Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
• Authors: Sho Sonoda, Shunta Akiyama, Yuya Uezato,
• Abstract summary: Agentic theorem provers are pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier.<n>We propose a distributional viewpoint and introduce provability, defined as the finite-horizon success probability of reaching a verified proof.<n>We provide a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions.
• Score: 8.948475969696075
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Agentic theorem provers -- pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier -- have recently achieved striking empirical success, yet it remains unclear which components drive performance and why such systems work at all despite classical hardness of proof search. We propose a distributional viewpoint and introduce \textbf{statistical provability}, defined as the finite-horizon success probability of reaching a verified proof, averaged over an instance distribution, and formalize modern theorem-proving pipelines as time-bounded MDPs. Exploiting Bellman structure, we prove existence of optimal policies under mild regularity, derive provability certificates via sub-/super-solution inequalities, and bound the performance gap of score-guided planning (greedy/top-\(k\)/beam/rollouts) in terms of approximation error, sequential statistical complexity, representation geometry (metric entropy/doubling structure), and action-gap margin tails. Together, our theory provides a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions, while clarifying limitations in worst-case or adversarial regimes.

Related papers

• On Multi-Step Theorem Prediction via Non-Parametric Structural Priors [50.16583672681106]
  In this work, we explore training-free theorem prediction through the lens of in-context learning (ICL)<n>We propose Theorem Precedence Graphs, which encode temporal dependencies from historical solution traces as directed graphs, and impose explicit topological constraints that effectively prune the search space during inference.<n>Experiments on the FormalGeo7k benchmark show that our method achieves 89.29% accuracy, substantially outperforming ICL baselines and matching state-of-the-art supervised models.
  arXiv  Detail & Related papers  (2026-03-05T06:08:50Z)
• Project Ariadne: A Structural Causal Framework for Auditing Faithfulness in LLM Agents [0.0]
  We introduce textbfProject Ariadne, a novel XAI framework to audit the causal integrity of agentic reasoning.<n>Unlike existing interpretability methods that rely on surface-level textual similarity, Project Ariadne performs textbfhard interventions ($do$-calculus) on intermediate reasoning nodes.<n>Our empirical evaluation of state-of-the-art models reveals a persistent textitFaithfulness Gap.
  arXiv  Detail & Related papers  (2026-01-05T18:05:29Z)
• Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
  We show that curriculum post-training avoids the exponential complexity bottleneck.<n>Under outcome-only reward signals, reinforcement learning finetuning achieves high accuracy with sample complexity.<n>We establish guarantees for test-time scaling, where curriculum-aware querying reduces both reward oracle calls and sampling cost from exponential to order.
  arXiv  Detail & Related papers  (2025-11-10T18:29:54Z)
• Non-asymptotic error bounds for probability flow ODEs under weak log-concavity [6.661419982187023]
  This work establishes non-asymptotic convergence bounds in the 2-Wasserstein distance for a general class of probability flow ODEs.<n>Our results extend convergence theory to more realistic data distributions and practical ODE solvers.
  arXiv  Detail & Related papers  (2025-10-20T14:54:38Z)
• SalaMAnder: Shapley-based Mathematical Expression Attribution and Metric for Chain-of-Thought Reasoning [45.78228118909098]
  Chain-of-Thought (CoT) prompting enhances the math reasoning capability of large language models (LLMs) to a large margin.<n>We present textbfSalaMAnder (textbfShtextbfaptextbfley-btextbfased textbfMathematical Expression textbfAttribution atextbfnd Mtextbfettextbfric), a theoretically grounded methodology.<n>We
  arXiv  Detail & Related papers  (2025-09-20T07:38:58Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  Chain-of-thought (CoT) reasoning enables large language models to break down complex problems into interpretable intermediate steps.<n>We introduce groundingS, a framework that formulates CoT reasoning as a Markov decision process (MDP) with latent state transitions.<n>We show improvements in reasoning accuracy, diversity, and exploration efficiency across benchmark reasoning tasks.
  arXiv  Detail & Related papers  (2025-07-10T21:32:18Z)
• From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
  We implement the classical axioms of preference-completeness, transitivity, continuity, and independence.<n>Our formalization captures the mathematical structure of preference relations over lotteries.<n>This formalization provides a rigorous foundation for applications in economic modeling, AI alignment, and management decision systems.
  arXiv  Detail & Related papers  (2025-06-08T10:09:54Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Identifiable Latent Neural Causal Models [82.14087963690561]
  Causal representation learning seeks to uncover latent, high-level causal representations from low-level observed data. We determine the types of distribution shifts that do contribute to the identifiability of causal representations. We translate our findings into a practical algorithm, allowing for the acquisition of reliable latent causal representations.
  arXiv  Detail & Related papers  (2024-03-23T04:13:55Z)
• Advancing Counterfactual Inference through Nonlinear Quantile Regression [77.28323341329461]
  We propose a framework for efficient and effective counterfactual inference implemented with neural networks. The proposed approach enhances the capacity to generalize estimated counterfactual outcomes to unseen data. Empirical results conducted on multiple datasets offer compelling support for our theoretical assertions.
  arXiv  Detail & Related papers  (2023-06-09T08:30:51Z)
• A Topological Perspective on Causal Inference [10.965065178451104]
  We show that substantive assumption-free causal inference is possible only in a meager set of structural causal models. Our results show that inductive assumptions sufficient to license valid causal inferences are statistically unverifiable in principle. An additional benefit of our topological approach is that it easily accommodates SCMs with infinitely many variables.
  arXiv  Detail & Related papers  (2021-07-18T23:09:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.