Pith. sign in

REVIEW 3 major objections 4 minor 30 references

This paper claims that the gap between a learned agentic prover and an optimal prover is at most twice the accumulated per-step scoring error, so short proofs and accurate step scores make success typical on biased problem streams.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 01:03 UTC pith:QFSGZ4MV

load-bearing objection A clean MDP framework for theorem proving, but the bridge from theory to practice is broken: the Monte Carlo label unbiasedness assumption is unverified, and the stated ERM bound doesn't match the appendix proof. the 3 major comments →

arxiv 2602.10538 v3 pith:QFSGZ4MV submitted 2026-02-11 stat.ML cs.LG

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

Sho Sonoda , Shunta Akiyama , Yuya Uezato This is my paper
classification stat.ML cs.LG MSC 68V1590C4068Q32
keywords statistical provabilityagentic theorem provingfinite-horizon MDPBellman recursionaction-value approximationtest-time computemargin conditionproof search
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tries to establish a statistical provability theory: treat formal proof search as a finite-horizon reachability problem, and measure success as the probability of reaching a verified proof within a step budget on a distribution of mathematical statements. Its central result bounds the loss from using a learned greedy prover instead of the optimal prover by twice the sum of per-step action-value errors — in plain terms, provability gap is proportional to effective proof length times score error. From this, the paper derives that proof-shortening, informative verifier feedback, retrieval, and representation geometry all help through a small set of measurable parameters, and that this is compatible with classical hardness results because real theorem distributions are biased, not uniform. A sympathetic reader would care because it converts a mysterious empirical success into a quantitative, component-sensitive account.

Core claim

Formalizing agentic theorem proving as a time-bounded reachability MDP — states are goal measures, actions are proof steps, the verifier defines the transition — the paper proves that for any initial problem whose relevant trajectories stay in a domain where learned scores h_b approximate the optimal one-step value Q*_b within ε_b, the deterministic greedy policy's success probability satisfies 0 ≤ V*_B(x0) − V^{π_h}_B(x0) ≤ 2 Σ_{b=1}^{B} ε_b. The regret of score-guided proof search is additive in per-step score errors, so the dominant complexity multiplier is the learned prover's average truncated proof length. Under a margin condition on action-value gaps the bound improves to a fast rate

What carries the argument

The central objects are the one-step optimal action-value functions Q*_b(x,a) — the probability that taking action a in state x leads to a proof within b remaining steps — and the learned score functions h_b that approximate them. The Bellman recursion V*_{b+1}(x) = 1[x∈G] ∨ sup_a Q*_{b+1}(x,a) turns proof search into dynamic programming, and sub-/super-solution inequalities yield provability certificates whose gap is at most twice the score error. The measure-valued encoding of proof states (a goal set as a finite Borel measure over an embedding space) gives compactness via the bounded-Lipschitz metric, which guarantees existence of optimal Markov policies.

Load-bearing premise

Everything rests on having unbiased estimates of Q*_b, the optimal value of each step, but the proposed Monte Carlo rollout labels are unbiased only if the continuation procedure is itself optimal, which is not shown and is unlikely for ordinary traces or greedy rollouts.

What would settle it

Take a small, fully enumerable proof MDP (e.g., a toy tactic environment with a known optimal prover). Train the score function h_b on labels produced by a deliberately suboptimal continuation policy. If an optimal prover beats the learned greedy prover by more than 2Σε_b on the same states — or if an exhaustive calculation shows E[Y|x,a] ≠ Q*_b for those labels — then the unbiased-label condition supporting Theorem 6 fails and Theorem 4's bound is not the operative explanation.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • If scores are accurate and proofs short, learned greedy provers nearly match optimal provers: the success gap grows only as proof length times per-step error, not exponentially in statement size.
  • Reducing proof length (via lemmas, cuts, or decomposition) and reducing score error (via better representations or more data) are interchangeable levers on the same bound — halving either halves the worst-case gap.
  • When correct actions are well separated from incorrect ones (a margin condition), the gap shrinks at the faster rate ε^{β+1}, improving sample complexity for a target success gap from (B/η)^{d+2} to (B/η)^{(d+2)/(β+1)}.
  • The framework identifies which components matter and how: verifier feedback localizes the relevant domain D, retrieval reduces effective proof length, and representation geometry controls statistical error via doubling dimension — all while classical worst-case hardness remains untouched as a lower bound on adversarial regimes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The load-bearing assumption that training labels satisfy E[Y|x,a] = Q*_b(x,a) is hard to meet in practice: labels from expert-trace or greedy-rollout continuation policies estimate that policy's value, not the optimal one. A testable consequence is that training scores on traces from a deliberately weak continuation policy should produce a greedy prover whose shortfall tracks the weak policy's val
  • The additive structure suggests a practical diagnostic: if one measured per-depth score errors ε_b on a held-out proof library, the bound could predict when extra test-time search (beam, rollouts) will pay off — when ε_b is large, search widens the candidate set instead of being wasted.
  • The certificate-gap minimization objective the paper sketches points to a theory-grounded representation-learning target: learn embeddings that make Bellman sub-/super-solutions tight, which is an operationalizable objective for proof-state encoders.
  • The margin-condition analysis implies that curriculum design that intentionally separates near-tie states (rather than merely increasing proof length) should improve fast-rate behavior — a consequence the paper does not spell out.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes a statistical treatment of agentic theorem proving: formal proof search is modeled as a finite-horizon reachability MDP over measure-valued proof states, with success probability as the objective. The main formal results are: existence of optimal Markov policies under compactness/Feller assumptions, provability certificates via Bellman sub-/super-solutions, a worst-case regret bound (Theorem 4) controlling the gap between a learned greedy prover and the optimal prover by the sum of uniform action-value errors, and a fast-rate margin version (Theorem 5). Section 7 claims sufficient statistical conditions under which the uniform approximation assumption holds with high probability, with Monte Carlo rollout labels as the practical construction.

Significance. If the advertised results were fully supported, this would provide a useful conceptual framework: the Bellman/certificate machinery is clean, and the decomposition of the provability gap into approximation error, geometric complexity, and margin properties is potentially informative. Theorem 4 is a correct conditional statement under Assumption 2, and I credit the paper for making that conditional structure explicit. However, the practical bridge—the part that claims to explain why agentic provers work—is not established. The unbiasedness of the proposed rollout labels is the main gap, and the proof of Theorem 6 analyzes a different estimator from the one stated. The explanatory narrative is also close to tautological in places: success is high when a learned function approximates optimal success and the horizon is short, which is an unpacking of the definition rather than an independent explanation. The paper's value lies in the formal scaffolding; its advertised claim about real training pipelines requires substantial revision.

major comments (3)
  1. The unbiasedness condition E[Y|x,a]=Q*_b(x,a) in Theorem 6 is load-bearing: it is what converts a statistical estimation statement into control of the epsilon_b in Assumption 2, and hence into the regret bound of Theorem 4. Remark 1 proposes Monte Carlo rollout labeling: apply action a, then follow "some continuation procedure" for b-1 steps. For any fixed continuation policy pi_c, E[Y|x,a]=Q^{pi_c}_{b-1}(x,a)=E[V^{pi_c}_{b-1}(x')|x,a], which is generally <= Q*_b(x,a)=E[V*_{b-1}(x')|x,a], with equality only if pi_c is optimal. No optimality or unbiasedness of the continuation procedure is shown, and expert-trace or learned rollout policies will not satisfy it. Consequently the labels estimate a behavior value, not the optimal value; Theorem 6 does not control epsilon_b in Assumption 2, and Theorem 4's bound against V*_B is unsupported for the described training pipelines. This is a load-
  2. The main text states that h_b is fit by empirical risk minimization and invokes Lemma 4. The proof in Appendix F proves a different statement: Theorem 7 analyzes a Lipschitz extension of sample means at a fixed eta-net of D, with independent samples at each net point, and it introduces an L_Q-Lipschitz assumption on Q* that is absent from the main theorem. No argument is given that ERM attains this bound, nor that an adaptively collected trajectory from a real interaction can be converted into independent net-point samples without an unstated coverage or distributional assumption. Appendix F itself concedes that the theorem "implicitly mixes two issues". Thus Theorem 6, as stated in Section 7, is unproved. The theorem should be either proved directly using Lemma 4 or replaced by the net-estimator statement with all additional assumptions stated in the main text.
  3. Theorem 5's fast-rate claim is not justified by the argument given. The proof in Section 6.4 asserts that errors occur only on the event Delta<=2epsilon, whose probability is bounded by the margin tail, and that the loss there is O(epsilon); Appendix D then says the sum gives O(B epsilon^{beta+1}) "up to constants and technical details about termination". The occupancy distribution nu_b is not tied to a specific policy, and the step converting expected per-depth regret under nu_b into E[V*_B(X_0)-V^{pi_{h,k}}_B(X_0)] is not supplied. Since the margin-induced fast rate is a headline contribution, this propagation step needs a rigorous, self-contained proof.
minor comments (4)
  1. The phrases "relevant domain D" and "relevant a" are informal. The invariant should be stated precisely, e.g., all state-action pairs reachable under both the optimal policy and the learned policy for the initial distribution of interest.
  2. Notation and numbering: Appendix F refers to "Theorem 7" as a refined version of Theorem 6, but the main text only labels Theorem 6. Also, the target is written Q in the appendix rather than Q*_b, which can confuse the reading.
  3. The scaling-law discussion (exponential improvements from reducing L_eff or d_D) is framed as a consequence of the bounds, but the mechanisms (cut-introduction, manifold localization) are illustrative rather than formal. This should be labeled as interpretation/conjecture rather than a derived result.
  4. The short proof of Theorem 4 would benefit from a two-line induction on b, since the additivity of per-step losses is the core structural point of the paper and appears only as a sentence.

Circularity Check

1 steps flagged

Practical label construction is circular: rollout labels estimate Q* only if the continuation policy is already optimal, so the statistical bridge to Theorem 4 is not established.

specific steps
  1. fitted input called prediction [Section 7, Remark 1; Theorem 6; Definition 3]
    "Theorem 6: 'Suppose ... E[Y|x,a] = Q*_b(x,a)' ... Remark 1: '(4) Then follow some continuation procedure for at most b−1 further steps. (5) Output Y = 1 if the proof is solved within the remaining steps, else Y = 0.' Definition 3: 'Q*_b(x,a) := ∫ V*_{b−1}(x′) P(dx′|x,a).'"

    For any fixed continuation policy π_c, the Remark 1 rollout has E[Y|x,a] = V^{π_c}_{b−1}(x′), where x′ is the state after action a. By Definition 3, Q*_b(x,a) = E[V*_{b−1}(x′)]. These coincide only if the continuation policy is optimal. The paper neither asserts nor proves optimality; it merely says 'some continuation procedure.' Thus the unbiasedness premise of Theorem 6 is not supplied by the proposed construction: h_b fitted to such labels estimates the behavior policy's value, not Q*. Substituting that ε_b into Theorem 4 compares the learned prover to the behavior value, not to V*_B. The 'prediction' of near-optimal provability therefore assumes, inside the label-generation procedure, the very optimality the score is supposed to learn.

full rationale

The formal core of the paper is internally valid and not circular in the strict sense: Definitions 1–3 set up a reachability MDP, Assumption 2 is a uniform approximation condition, Lemma 3 and Theorem 4 give a valid regret bound conditional on that assumption, and Theorem 6 is a standard uniform-deviation result conditional on unbiased targets E[Y|x,a]=Q*_b(x,a). There are no load-bearing self-citations, no imported uniqueness theorems from the authors, and no ansatz smuggled in via citation; the cited statistical tools (Azuma–Hoeffding, covering numbers, sequential complexity) are standard external results. The circularity enters at the proposed practical instantiation of the unbiased-label assumption. Remark 1's Monte Carlo rollout labeling defines Y as success under an unspecified 'continuation procedure.' For E[Y] to equal Q*_b, that continuation must already be an optimal policy for the remaining horizon. If it is not, the labels are unbiased for the value of the behavior/continuation policy, not for the optimal value, so the estimated h_b does not control the ε_b appearing in Theorem 4. If it is optimal, then the construction assumes the very object the paper aims to learn. Either way, the bridge from the theorem to real training pipelines is either circular or unsupported. This is load-bearing because Section 7 is explicitly presented as the way to obtain Assumption 2 ('How to obtain such bounds with high probability is addressed in Section 7'), and the main success-gap bound depends on it. The mathematical theorems themselves are not circular; the circularity is localized to the practical label-construction claim.

Axiom & Free-Parameter Ledger

4 free parameters · 7 axioms · 0 invented entities

The framework introduces the formal notions 'statistical provability' and 'provability certificate' as mathematical objects, but these are definitions rather than new postulated entities. The free parameters and axioms are structural assumptions required for the theorems; the most consequential is the assumption of unbiased Q* samples, which the paper's own label construction does not guarantee.

free parameters (4)
  • truncation mass W
    State space is truncated to M_{≤W}(G); W is a hand-chosen cap on the number of goals, or justified empirically, but is a free modeling parameter.
  • doubling dimension d_D
    Assumption 4: the relevant domain D is assumed to have covering number growth with exponent d_D. This is an ad hoc structural parameter controlling statistical rates, not measured.
  • margin exponent β and constant C_Δ
    Assumption 3 assumes ν_b(Δ^{(k)}_b ≤ t) ≤ C_Δ t^β. β is an ad hoc parameter that determines whether fast rates hold; if β=0 the bound collapses to linear. No evidence is given for any value.
  • Lipschitz constant L_H of score class
    Assumption 5: H_b ⊆ Lip_{L_H}(D,[0,1]). L_H is a free class parameter used in the metric entropy and estimation bounds.
axioms (7)
  • domain assumption Feller/weak continuity of the transition kernel P (Assumption 1).
    Assumed to guarantee existence of optimal policies via the maximum theorem. Not verified for actual LLM+proof-assistant pipelines.
  • domain assumption Compactness of action space A and truncated state space M_{≤W}(G).
    Needed for compactness and attainment of suprema; requires the goal-count bound W.
  • domain assumption The proof assistant verifier is faithful: transitions produce correct successor states.
    Section 3.3: 'the proof assistant acts as a verifier: it produces correct successor states.' This treats the verifier as exact, although external tools in real systems can be unsound or incomplete.
  • ad hoc to paper Existence of unbiased targets Y with E[Y|x,a] = Q*_b(x,a).
    Theorem 6 and Remark 1 assume such Y can be obtained by Monte Carlo rollouts; the construction given does not ensure unbiasedness unless the rollout continuation policy is optimal. This is the load-bearing practical assumption.
  • domain assumption Doubling/covering-number bound on the relevant domain D (Assumption 4).
    Used to bound metric entropy of Lipschitz score classes and hence the statistical error rate.
  • domain assumption Uniform Lipschitz score class (Assumption 5).
    Needed for uniform deviation and entropy bounds; restricts the hypothesis class.
  • ad hoc to paper Small-margin tail under occupancy (Assumption 3).
    The fast-rate result depends on this distributional condition on Q*-gaps; the paper offers no justification that it holds for theorem-proving workloads.

pith-pipeline@v1.3.0-alltime-deepseek · 16605 in / 12929 out tokens · 128587 ms · 2026-08-03T01:03:43.974240+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models." pith.science (2026). https://pith.science/paper/QFSGZ4MV

@misc{pith2026260210538,
  author       = {Pith},
  title        = {Pith review of: Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QFSGZ4MV}},
  note         = {Machine review of arXiv:2602.10538}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 3 canonical work pages

  1. [1]

    Achim, A

    T. Achim, A. Best, A. Bietti, K. Der, M. F^^c3^^a9d^^c3^^a9rico, S. Gukov, D. Halpern-Leistner, K. Henningsgard, Y. Kudryashov, A. Meiburg, M. Michelsen, R. Patterson, E. Rodriguez, L. Scharff, V. Shanker, V. Sicca, H. Sowrirajan, A. Swope, M. Tamas, V. Tenev, J. Thomm, H. Williams, and L. Wu. Aristotle: IMO-level Automated Theorem Proving https://arxiv.o...

    Pith/arXiv arXiv 2025

  2. [2]

    D. Angluin. Learning regular sets from queries and counterexamples https://www.sciencedirect.com/science/article/pii/0890540187900526. Information and Computation, 75: 0 87--106, 1987. ISSN 0890-5401

    arXiv 1987

  3. [3]

    Arlot and P

    S. Arlot and P. L. Bartlett. Margin-adaptive model selection in statistical learning https://doi.org/10.3150/10-BEJ288. Bernoulli, 17: 0 687--713, 5 2011. doi:10.3150/10-BEJ288

    work page doi:10.3150/10-bej288 2011

  4. [4]

    K. Baba, C. Liu, S. Kurita, and A. Sannai. Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs https://openreview.net/forum?id=sPdQfGQccH. In Second AI4Math workshop at ICML2025, 10 2025

    2025

  5. [5]

    Bansal, S

    K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox. https://proceedings.mlr.press/v97/bansal19a.html HOL ist: An Environment for Machine Learning of Higher Order Logic Theorem Proving . In Proceedings of the 36th International Conference on Machine Learning, volume 97 of Proceedings of Machine Learning Research, pages 454--463. PMLR, 2019

    2019

  6. [6]

    K. Barreto. Problem 728 and the use of ai on erd^^c5^^91s problems, 1 2026. URL https://www.erdosproblems.com/forum/thread/blog:2

    2026

  7. [7]

    Beirami, A

    A. Beirami, A. Agarwal, J. Berant, A. D'Amour, J. Eisenstein, C. Nagpal, and A. T. Suresh. Theoretical guarantees on the best-of-n alignment policy https://proceedings.mlr.press/v267/beirami25a.html. In Proceedings of the 42nd International Conference on Machine Learning, volume 267, pages 3580--3602. PMLR, 1 2025

    2025

  8. [8]

    Block, Y

    A. Block, Y. Dagan, and A. Rakhlin. Majorizing Measures, Sequential Complexities, and Online Learning https://proceedings.mlr.press/v134/block21a.html. In M. Belkin and S. Kpotufe, editors, Proceedings of Thirty Fourth Conference on Learning Theory, volume 134, pages 587--590. PMLR, 1 2021

    2021

  9. [9]

    Botta, Y

    E. Botta, Y. Li, A. Mehta, J. T. Ash, C. Zhang, and A. Risteski. On the Query Complexity of Verifier-Assisted Language Generation https://proceedings.mlr.press/v267/botta25a.html. In Proceedings of the 42nd International Conference on Machine Learning, volume 267, pages 5124--5155. PMLR, 1 2025

    2025

  10. [10]

    Bryan, B

    J. Bryan, B. Elek, F. Manners, G. Salafatinos, and R. Vakil. The motivic class of the space of genus 0 maps to the flag variety https://arxiv.org/abs/2601.07222. arXiv preprint: 2601.07222, 1 2026

    arXiv 2026

  11. [11]

    L. Chen, J. Gu, L. Huang, W. Huang, Z. Jiang, A. Jie, X. Jin, X. Jin, C. Li, K. Ma, C. Ren, J. Shen, W. Shi, T. Sun, H. Sun, J. Wang, S. Wang, Z. Wang, C. Wei, S. Wei, Y. Wu, Y. Wu, Y. Xia, H. Xin, F. Yang, H. Ying, H. Yuan, Z. Yuan, T. Zhan, C. Zhang, Y. Zhang, G. Zhang, T. Zhao, J. Zhao, Y. Zhou, and T. H. Zhu. Seed-Prover: Deep and Broad Reasoning for ...

    Pith/arXiv arXiv 2025

  12. [12]

    New record on frontiermath tier 4, 1 2026

    Epoch AI . New record on frontiermath tier 4, 1 2026. URL https://epochai.substack.com/p/new-record-on-frontiermath-tier-4

    2026

  13. [13]

    G. Feng, B. Zhang, Y. Gu, H. Ye, D. He, and L. Wang. Towards Revealing the Mystery behind Chain of Thought: A Theoretical Perspective https://papers.nips.cc/paper_files/paper/2023/hash/dfc310e81992d2e4cedc09ac47eff13e-Abstract-Conference.html. In Advances in Neural Information Processing Systems, volume 36, pages 70757--70798, 2023

    2023

  14. [14]

    Finzi, S

    M. Finzi, S. Qiu, Y. Jiang, P. Izmailov, J. Z. Kolter, and A. G. Wilson. From Entropy to Epiplexity: Rethinking Information for Computationally Bounded Intelligence https://arxiv.org/abs/2601.03220. arXiv preprint: 2601.03220, 1 2026

    arXiv 2026

  15. [15]

    Gauthier, C

    T. Gauthier, C. Kaliszyk, and J. Urban. TacticToe: Learning to Reason with HOL4 Tactics https://easychair.org/publications/paper/WsM. In T. Eiter and D. Sands, editors, LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46, pages 125--143. EasyChair, 2017. doi:10.29007/ntlb

    work page doi:10.29007/ntlb 2017

  16. [16]

    Gauthier, C

    T. Gauthier, C. Kaliszyk, J. Urban, R. Kumar, and M. Norrish. http://doi.org/10.1007/s10817-020-09580-x TacticToe: Learning to Prove with Tactics . J. Autom. Reason., 65 0 (2): 0 257--286, 2021

    doi:10.1007/s10817-020-09580-x 2021

  17. [17]

    A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu. https://openreview.net/forum?id=SMa9EAovKMC Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs . In The Eleventh International Conference on Learning Representations, 2023

    2023

  18. [18]

    Kojima, S

    T. Kojima, S. S. Gu, M. Reid, Y. Matsuo, and Y. Iwasawa. Large Language Models are Zero-Shot Reasoners https://papers.nips.cc/paper_files/paper/2022/hash/8bb0d291acd4acf06ef112099c16f326-Abstract-Conference.html. In Advances in Neural Information Processing Systems, volume 35, pages 22199--22213, 2022

    2022

  19. [19]

    D. Phan, M. D. Hoffman, D. Dohan, S. Douglas, T. A. Le, A. Parisi, P. Sountsov, C. Sutton, S. Vikram, and R. A. Saurous. Training Chain-of-Thought via Latent-Variable Inference https://proceedings.neurips.cc/paper_files/paper/2023/hash/e69a9560c450ca76584d9eb37e7f5ae8-Abstract-Conference.html. In Advances in Neural Information Processing Systems, volume 3...

    2023

  20. [20]

    Polu and I

    S. Polu and I. Sutskever. https://arxiv.org/abs/2009.03393 Generative Language Modeling for Automated Theorem Proving . arXiv preprint: 2009.03393, 2020

    Pith/arXiv arXiv 2009

  21. [21]

    Rakhlin, K

    A. Rakhlin, K. Sridharan, and A. Tewari. Sequential complexities and uniform martingale laws of large numbers https://doi.org/10.1007/s00440-013-0545-5. Probability Theory and Related Fields, 161: 0 111--153, 2015 a . ISSN 1432-2064. doi:10.1007/s00440-013-0545-5

    work page doi:10.1007/s00440-013-0545-5 2015

  22. [22]

    Rakhlin, K

    A. Rakhlin, K. Sridharan, and A. Tewari. Online Learning via Sequential Complexities http://jmlr.org/papers/v16/rakhlin15a.html. Journal of Machine Learning Research, 16: 0 155--186, 2015 b

    2015

  23. [23]

    Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. F. Wu, Z. Gou, S. Ma, H. Tang, Y. Liu, W. Gao, D. Guo, and C. Ruan. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition https://arxiv.org/abs/2504.21801. arXiv Preprint: 2504.21801, 7 2025

    Pith/arXiv arXiv 2025

  24. [24]

    Setlur, N

    A. Setlur, N. Rajaraman, S. Levine, and A. Kumar. Scaling Test-Time Compute Without Verification or RL is Suboptimal https://proceedings.mlr.press/v267/setlur25a.html. In Proceedings of the 42nd International Conference on Machine Learning, volume 267, pages 54058--54094. PMLR, 1 2025

    2025

  25. [25]

    Strobl, W

    L. Strobl, W. Merrill, G. Weiss, D. Chiang, and D. Angluin. What Formal Languages Can Transformers Express? A Survey https://doi.org/10.1162/tacl_a_00663. Transactions of the Association for Computational Linguistics, 12: 0 543--561, 5 2024

    doi:10.1162/tacl_a_00663 2024

  26. [26]

    Varambally, T

    S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye. Hilbert: Recursively Building Formal Proofs with Informal Reasoning https://arxiv.org/abs/2509.22819. arXiv preprint: 2509.22819, 9 2025

    arXiv 2025

  27. [27]

    Y. Wu, Z. Sun, S. Li, S. Welleck, and Y. Yang. Scaling Inference Computation: Compute-Optimal Inference for Problem-Solving with Language Models https://openreview.net/forum?id=j7DZWSc8qu. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024

    2024

  28. [28]

    H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data https://arxiv.org/abs/2405.14333. arXiv preprint: 2405.14333, 2024

    Pith/arXiv arXiv 2024

  29. [29]

    K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. https://openreview.net/forum?id=g7OX2sOJtn LeanDojo: Theorem Proving with Retrieval-Augmented Language Models . In Thirty-seventh Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023

    2023

  30. [30]

    Zheng, J

    K. Zheng, J. M. Han, and S. Polu. https://openreview.net/forum?id=9ZPegFuFTFv MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics . In International Conference on Learning Representations, 2022

    2022