Pith. sign in

REVIEW 4 major objections 5 minor 62 references

A new proof-agent design claims that emitting proofs as JSON abstract-syntax trees and editing a proof tree instead of source text cuts API cost 2.3–4.7x, cuts tokens 2.9–6.9x, and lets general LLMs prove theorems in a language released aft

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-01 21:35 UTC pith:AMRU6MJF

load-bearing objection Genuinely novel tree-edit proof agent with a real confound at the center of its efficiency claims — worth peer review, but the RQ1 answer outruns the evidence. the 4 major comments →

arxiv 2607.16372 v1 pith:AMRU6MJF submitted 2026-07-17 cs.SE cs.AIcs.LGcs.PL

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Qiyuan Xu , Joshua Ong Jun Leang , Renxi Wang , Wenda Li , Haonan Li , Luke Ong , Conrad Watt This is my paper
classification cs.SE cs.AIcs.LGcs.PL
keywords interactive theorem provingLLM agentsabstract syntax treetree-edit proof modelMinilangAPI cost reductionverification-condition provingformal proof generation
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.

LLM-based theorem-proving agents are accurate but costly, with per-problem API costs reaching tens to hundreds of dollars. This paper traces that expense to a design shared by current agents: they emit proofs as source text and recover proof states through separate line-number-based queries, so every edit invalidates earlier locations. The proposed remedy, realized in the AoA agent, is to lift the agent onto the abstract syntax tree: the model writes proofs as JSON directly, and drives the prover by filling, amending, and deleting nodes in a single proof tree in which each operation already carries its own subgoal's state. On common solved problems, AoA uses 2.9–6.9x fewer tokens, 3.9–8.9x fewer tool calls, finishes 1.4–2.0x faster, and costs 2.3–4.7x less than a conventional same-platform agent, while solving more problems on the harder benchmark. A second experiment shows the approach works with a model whose training predates the language's corpus, suggesting new proof languages can be adopted without fine-tuning.

Core claim

LLM proving agents are accurate but costly, spending tens to hundreds of dollars per problem. This paper claims the cost comes from operating on serialized source text: agents patch proof files by line number, and every edit shifts later lines, forcing repeated state queries. AoA's remedy is to make the abstract syntax tree the working object. The model emits proofs as JSON representations of the language's AST, and edits a single proof tree in which each operation node carries its own subgoal's state. On common solved problems, AoA uses 2.9–6.9x fewer tokens, 3.9–8.9x fewer tool calls, finishes 1.4–2.0x faster, and costs 2.3–4.7x less than a conventional agent on the same prover, while solv

What carries the argument

The central object is a proof tree that interleaves operation nodes, goal nodes, and empty slots; each operation node records the prover's feedback and the resulting subgoal states. The agent edits the tree with four commands — fill, insert, amend, and delete — and after each edit receives only the changed proof-state overview, with completed subtrees collapsed. Proof steps are written as JSON conforming to a schema of the language's AST, a format tool-calling LLMs handle natively. This removes file-path and line-number navigation: the model reads everything it needs, including subgoal states and messages, directly off the node it is editing.

Load-bearing premise

The claim that the tree-edit/AST interface causes the cost reduction assumes the redesigned proof language and the tree-edit model are not confounded; the paper states there is no clean ablation separating their individual contributions.

What would settle it

Run a conventional line-number-based text agent on the same Minilang with the same model and API billing; if its token and cost figures match AoA's, the tree-edit model is not the driver. Conversely, apply AoA's tree-edit interface to an existing proof language's AST; if the cost advantage disappears, the advantage depends on language redesign rather than the interface.

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

If this is right

  • A newly designed proof language can be used by off-the-shelf LLM agents immediately, without waiting for corpus-scale training data or paying for fine-tuning.
  • Per-problem proof cost falls to a range that makes industrial-scale verification (thousands to hundreds of thousands of proof goals) economically conceivable.
  • On harder proof goals, the savings grow, so the interface is most valuable exactly where conventional agents are most expensive.
  • The efficiency gain is not bought with capability: the agent solves more verification-condition problems than the baseline and matches the best reported result on the mathematics benchmark.
  • The same 'agent-over-AST' pattern could be ported to other proof languages whose semantics can be exposed in a structured, LLM-friendly form.

Where Pith is reading between the lines

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

  • Because the paper concedes that the redesigned language and the tree-edit interface are confounded, the cleanest test of the mechanism is a conventional text-editing agent over the same Minilang: if its cost approaches AoA's, the savings come from the language, not the tree.
  • The training-cutoff experiment suggests that the main barrier to adopting new formal languages is interface design rather than model weights; if true, language designers should treat an LLM-facing AST schema as part of the language's deliverable.
  • The approach likely transfers to code generation for experimental programming languages, where line-shift churn and unfamiliar syntax cause similar token waste; the authors point to this open problem themselves.
  • One threat to the quantitative claims is the pricing asymmetry between the two agents' API access; a fair replication would run both under identical billing and caching terms.

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

4 major / 5 minor

Summary. The paper presents AoA, a theorem-proving agent that operates on Minilang's abstract syntax tree rather than on concrete proof text. The agent emits proofs as JSON ASTs and interacts with the prover through a tree-edit model in which proof operations and resulting proof states are stored in a single proof tree. The authors evaluate AoA against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl, reporting large reductions in API cost, token usage, tool calls, and wall-clock time on common success sets, as well as higher pass rates on NTP4VC-Pearl. They also test a pre-corpus model (Claude Opus 4.5) to argue that AoA enables proving in Minilang without corpus-scale prior exposure.

Significance. If the central claim holds, the paper makes a useful contribution: it shows that abstracting away from concrete syntax and exposing a structured proof tree can reduce the token and tool-call overhead of LLM proof agents, and it provides evidence that a newly designed proof language can be used by general-purpose LLMs without fine-tuning. The paper includes a formalized tree-edit model with edit-command semantics (Fig. 3), an open-source implementation, an attempt to control for model choice by using the same underlying LLM for both agents, and a pre-corpus model experiment for RQ2. These are genuine strengths. The main weakness is that the comparison changes two variables at once—the proof language (Minilang vs. Isar) and the interaction paradigm (AST/tree-edit vs. source-text/line-based)—and the paper explicitly concedes that no clean ablation separates their contributions. The causal attribution of the reported cost reductions to the tree-edit/AST design is therefore not established by the current evidence.

major comments (4)
  1. [§IV-A6 (Analysis) and Answer to RQ1] The paper states: 'There is no clean ablation that can separate their individual contributions.' This is load-bearing because RQ1 asks for cost reduction 'from the side of agent design,' yet the Answer to RQ1 attributes the gains to 'redesigning the proof language and exposing its AST within a tree-edit proof model.' Since Minilang itself already achieves SOTA LLM proving with ATP delegation and high-level structural commands, the reported 2.3–4.7x cost reduction may be substantially a language-level effect rather than an effect of the tree-edit/AST interface. To make the claim defensible, the authors should provide at least one additional comparison that varies only one factor—for example, a conventional text-editing agent over Minilang (with grammar documentation injected), or a tree-edit agent over a restricted Isar subset—or explicitly bound the language contribution using existing M
  2. [§IV-A3 and Table III] The baseline is evaluated only on randomly sampled subsets: 73 miniF2F problems (~30%) and 50 NTP4VC-Pearl problems (~18%), with no confidence intervals or variance reporting. Resource metrics are then compared only on the common success sets, which may differ systematically between agents because the agents solve different problems (e.g., AoA solves all 73 miniF2F cases, Amazon's solves 65). The reported per-case token and cost multipliers could be sensitive to which problems fall into the common success set. Please report per-problem distributions, confidence intervals, and the list of common-success problems, and show that the qualitative multipliers are stable across random subsamples.
  3. [§IV-A3 and §IV-A5, Table II/III] The cost comparison uses asymmetric pricing schemes: AoA runs under Claude Code subscription pricing, while Amazon's agent calls the Claude API directly. The 'normalized input-cache accounting' only adjusts for cache rates; it does not remove the per-token price asymmetry or the subscription overhead. Moreover, on NTP4VC-Pearl the full 50-case evaluation uses GPT-5.5, and the Claude-based baseline was stopped after 31 cases because the budget was exceeded. These are acknowledged in the text, but the absolute dollar figures in Table II and the normalized multipliers in Table III should be accompanied by a transparent statement of the exact per-token prices assumed, and ideally by a sensitivity analysis. Without this, the cost multipliers are not as robust as the abstract suggests.
  4. [§IV-B (RQ2)] The pre-corpus experiment with Claude Opus 4.5 is a good idea, but the claim 'without corpus-scale exposure' is only tested on a 73-problem miniF2F subset, not on NTP4VC-Pearl. In addition, Minilang and NTP4VC-Pearl are both artifacts from the same research group, and the model may have seen related Isabelle/AFP material or earlier Minilang snapshots. The paper's conclusion is appropriately scoped to Minilang, but the RQ2 answer would be stronger with a second, independent new language or with an explicit contamination check (e.g., probing the model on Minilang syntax from the released corpus). As written, the evidence supports 'works for Minilang with a pre-corpus model' more strongly than the general claim 'enables proving in a language without corpus-scale exposure.'
minor comments (5)
  1. [§III-B3] The formalization of the re-evaluation mechanism is deferred to the released source code. Since the correctness of the tree-edit model depends on this mechanism, a brief formal statement or a reference to a specific file/function in the repository would help reviewers and readers verify the claims.
  2. [Table III] The notation 'Amazon's O' and 'Amazon's N' is not defined in the table caption; the note defines it but the caption should be self-contained. Also, the 'cost' column for normalized rows is recomputed only for input-cache effects, but the table does not state the assumed cache hit ratio; please state it explicitly.
  3. [§IV-A5] The sentence 'the cost of evaluating Amazon’s agent had already exceeded USD 1,500 after completing only 31 cases' is a useful detail, but it would be clearer to report the exact budget and the number of cases in a single place in the main text rather than splitting across §IV-A3 and §IV-A5.
  4. [Abstract and §I] The abstract says 'cuts API cost by 2.3–4.7x' without immediately noting that this is on common success sets and with normalized accounting. Please add a qualifier in the abstract, as the current wording could overstate the result.
  5. [§III-C] The description of the compressed EDIT response is clear, but it would help to include a short pseudocode or a formal definition of the compression policy (which nodes are omitted, when subtrees are collapsed) so that the implementation can be reproduced without reverse-engineering.

Circularity Check

0 steps flagged

No circular derivation; the efficiency comparisons are empirical against an external baseline, with confounds that are validity threats rather than reductions.

full rationale

The paper's central claims are empirical evaluations, not derivations. AoA's token, tool-call, time, and cost reductions are measured against Amazon's Isabelle Agent on two benchmarks; no parameter is fitted and then renamed as a prediction, and the tree-edit model's efficiency is not defined in terms of the cost ratios. The main caveat is stated in §IV-A6: "There is no clean ablation that can separate their individual contributions" — this is a causal-identification confound (Minilang vs tree-edit), not circularity. The self-citations to Minilang [18] and NTP4VC-Pearl [33] involve overlapping authors, but those are separate prior artifacts, and the paper does not rest a derivation on them; the Opus 4.5 experiment in §IV-B provides independent support for RQ2 by using a model released before the public Minilang corpus. Benchmark and pricing choices in §IV-A3 (subscription vs direct API, sampled subsets, cache normalization) are fairness threats, not circular steps. No equation is equivalent to its input, and no uniqueness or ansatz result is imported from a self-citation chain.

Axiom & Free-Parameter Ledger

1 free parameters · 4 axioms · 0 invented entities

The paper introduces no new physical or formal entities; its empirical claims rest on assumptions about Minilang's design, LLM tool-calling reliability, and the comparability of the baseline. The one hand-tuned number is the cache-rate normalization used to compute the headline cost multiplier.

free parameters (1)
  • Baseline input-cache rate normalization = set equal to AoA's observed cache rate (≈87% miniF2F, ≈94% NTP4VC)
    The reported 2.3–4.7x cost reduction depends on assuming Amazon's agent would reuse cached input at the same rate as AoA; this is a hand-set normalization rather than a measured quantity. See §IV-A4 and Table III.
axioms (4)
  • domain assumption Minilang's proof-state effects are block-local, so only following siblings need re-evaluation after an edit.
    The re-evaluation mechanism relies on this property of Minilang, stated in §II-C and §III-B3; the exact formalization is deferred to source code.
  • domain assumption General-purpose LLMs can reliably emit valid Minilang ASTs as JSON via tool calling.
    This is the central feasibility premise of the whole approach; empirical pass rates support it, but it is not independently proven.
  • ad hoc to paper Amazon's Isabelle Agent, with cache normalization and modified cache-control directives, is a fair baseline for cost comparison.
    The headline cost ratios are computed against a baseline that was modified and normalized in ways that materially affect the numbers. See §IV-A3 and §IV-A4.
  • domain assumption The sampled subsets of miniF2F (73 problems) and NTP4VC-Pearl (50 problems) are representative of the full benchmarks.
    Only about 30% and 18% of benchmarks are used for the baseline comparison, without reported seeds or confidence intervals. See §IV-A3.

pith-pipeline@v1.3.0-alltime-deepseek · 20336 in / 11187 out tokens · 104378 ms · 2026-08-01T21:35:34.604584+00:00 · methodology

0 comments
read the original abstract

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.

Figures

Figures reproduced from arXiv: 2607.16372 by Conrad Watt, Haonan Li, Joshua Ong Jun Leang, Luke Ong, Qiyuan Xu, Renxi Wang, Wenda Li.

Figure 1
Figure 1. Figure 1: The agent pipeline of AoA it opens. A proof block can contain zero or more commands (Minilang Cmd∗ ). III. METHOD: OVER THE ABSTRACT SYNTAX TREE As motivated in § I, AoA interacts with the prover through a tree-edit proof model over Minilang’s AST. This section develops this design. § III-A first presents a running example to illustrate how AoA constructs a proof by editing the proof tree. § III-B then for… view at source ↗
Figure 2
Figure 2. Figure 2: Examples of Minilang, the JSON representation of its AST, and the YAML representation of the proof tree. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The behaviors of the tree edit commands. Here, we use [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Pass rate under increasing per-case budgets. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗

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

62 extracted references · 2 canonical work pages

  1. [1]

    Generative language modeling for automated theorem proving,

    S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”arXiv preprint arXiv:2009.03393, 2020

    Pith/arXiv arXiv 2009

  2. [2]

    Leandojo: Theorem proving with retrieval-augmented language models,

    K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “Leandojo: Theorem proving with retrieval-augmented language models,”Advances in Neural Information Processing Systems, vol. 36, pp. 21 573–21 612, 2023

    2023

  3. [3]

    Refinedc: automating the foundational verification of c code with refined ownership types,

    M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg, “Refinedc: automating the foundational verification of c code with refined ownership types,” inProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 158–174

    2021

  4. [4]

    Foundational multi-modal program verifiers,

    V . Gladshtein, G. Pˆırlea, Q. Zhao, V . Kurin, and I. Sergey, “Foundational multi-modal program verifiers,”Proc. ACM Program. Lang., vol. 10, no. POPL, Jan. 2026. [Online]. Available: https://doi.org/10.1145/3776719

    doi:10.1145/3776719 2026

  5. [5]

    Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience,

    J. Chen, W. Chen, J. Du, J. Hu, Z. Jiang, A. Jie, X. Jin, X. Jin, C. Li, W. Shi, Z. Wang, M. Wang, C. Wei, S. Wei, H. Xin, F. Yang, W. Gao, Z. Yuan, T. Zhan, Z. Zheng, T. Zhou, and T. H. Zhu, “Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience,” 2025. [Online]. Available: https://arxiv.org/abs/2512.17260

    arXiv 2025

  6. [6]

    DeepSeek-Prover- V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition,

    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,” 2025. [Online]. Available: https://arxiv.org/abs/2504.21801

    Pith/arXiv arXiv 2025

  7. [7]

    A minimal agent for automated theorem proving,

    B. Requena, A. Letson, K. Nowakowski, I. B. Ferreiro, and L. Sarra, “A minimal agent for automated theorem proving,” inICLR 2026 Workshop: VerifAI-2: The Second Workshop on AI Verification in the Wild, 2026. [Online]. Available: https://openreview.net/forum?id=E30g7bO7rU

    2026

  8. [8]

    Numina- lean-agent: An open and general agentic reasoning system for formal mathematics,

    J. Liu, Z. Zhou, Z. Zhu, M. D. Santos, W. He, J. Liu, R. Wang, Y . Xie, J. Zhao, Q. Wang, L. Zhi, J. Li, and W. Li, “Numina- lean-agent: An open and general agentic reasoning system for formal mathematics,”CoRR, vol. abs/2601.14027, 2026. [Online]. Available: https://doi.org/10.48550/arXiv.2601.14027

    doi:10.48550/arxiv.2601.14027 2026

  9. [9]

    Merlean: An agentic framework for autoformalization in quantum computation,

    Y . Ren, J. Li, and Y . Qi, “Merlean: An agentic framework for autoformalization in quantum computation,” 2026. [Online]. Available: https://arxiv.org/abs/2602.16554

    arXiv 2026

  10. [10]

    Neural theorem proving: Generating and structuring proofs for formal verification,

    B. Rao, W. Eiers, and C. Lipizzi, “Neural theorem proving: Generating and structuring proofs for formal verification,” inProceedings of The 19th International Conference on Neurosymbolic Learning and Reasoning, ser. Proceedings of Machine Learning Research, L. H. Gilpin, E. Giunchiglia, P. Hitzler, and E. van Krieken, Eds., vol. 284. PMLR, 08–10 Sep 2025,...

    2025

  11. [11]

    Verisoftbench: Repository- scale formal verification benchmarks for lean,

    Y . Xin, Q. Chen, G. Durrett, and I. Dillig, “Verisoftbench: Repository- scale formal verification benchmarks for lean,”arXiv preprint arXiv:2602.18307, 2026

    arXiv 2026

  12. [12]

    Aleph prover: State-of-the-art formal theorem prover,

    Logical Intelligence, “Aleph prover: State-of-the-art formal theorem prover,” https://logicalintelligence.com/aleph-prover, 2025, accessed: 2026-06-21

    2025

  13. [13]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,

    G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri, “Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition,”Advances in Neural Information Processing Systems, vol. 37, pp. 11 545–11 569, 2024

    2024

  14. [14]

    William Lowell Putnam Math- ematical Competition,

    Mathematical Association of America, “William Lowell Putnam Math- ematical Competition,” https://maa.org/putnam/, accessed: 2026-05-23

    2026

  15. [15]

    Putnambench leaderboard,

    Trishul Lab, “Putnambench leaderboard,” https://trishullab.github.io/ PutnamBench/leaderboard.html, 2026, accessed: 2026-05-22

    2026

  16. [16]

    A minimal agent for automated theorem proving,

    B. Requena, A. Letson, K. Nowakowski, I. Beltran-Ferreiro, and L. Sarra, “A minimal agent for automated theorem proving,”arXiv preprint arXiv:2602.24273, 2026

    Pith/arXiv arXiv 2026

  17. [17]

    Automated conjecture resolution with formal verification,

    H. Ju, G. Gao, J. Jiang, B. Wu, Z. Sun, L. Chen, Y . Wang, Y . Wang, Z. Wang, W. He, P. Wu, L. Xiao, R. Liu, B. Dai, and B. Dong, “Automated conjecture resolution with formal verification,”

  18. [18]

    A minimalist proof language for neural theorem proving over Isabelle/HOL,

    Q. Xu, R. Wang, P. Wang, H. Li, and C. Watt, “A minimalist proof language for neural theorem proving over Isabelle/HOL,”Proceedings of the ACM on Programming Languages, vol. 10, no. OOPSLA1, pp. 2073–2098, 2026, also available as arXiv:2507.18885

    arXiv 2073

  19. [19]

    Coqpilot, a plugin for llm-based generation of proofs,

    A. Kozyrev, G. Solovev, N. Khramov, and A. Podkopaev, “Coqpilot, a plugin for llm-based generation of proofs,” inProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’24. New York, NY , USA: Association for Computing Machinery, 2024, p. 2382–2385. [Online]. Available: https://doi.org/10.1145/3691620.3695357

    arXiv 2024

  20. [20]

    AutoCorrode software verification framework for Isabelle/HOL,

    H. Becker, N. Chong, R. Dockins, J. Grundy, J. Z. S. Hu, I. Mulder, D. P. Mulligan, P. Mure, L. C. Paulson, and K. Slind, “AutoCorrode software verification framework for Isabelle/HOL,” https://github.com/ awslabs/autocorrode, 2025

    2025

  21. [21]

    Why do large language models (LLMs) struggle to count letters?

    T. Fu, R. Ferrando, J. Conde, C. Arriaga, and P. Reviriego, “Why do large language models (LLMs) struggle to count letters?” arXiv preprint arXiv:2412.18626, 2024. [Online]. Available: https: //arxiv.org/abs/2412.18626

    Pith/arXiv arXiv 2024

  22. [22]

    CUTE: Measuring LLMs’ understanding of their tokens,

    L. Edman, H. Schmid, and A. Fraser, “CUTE: Measuring LLMs’ understanding of their tokens,” inProceedings of the 2024 Conference on Empirical Methods in Natural Language Processing (EMNLP). Association for Computational Linguistics, 2024. [Online]. Available: https://aclanthology.org/2024.emnlp-main.177/

    2024

  23. [23]

    A machine-oriented logic based on the resolution principle,

    J. A. Robinson, “A machine-oriented logic based on the resolution principle,”Journal of the ACM, vol. 12, no. 1, pp. 23–41, 1965

    1965

  24. [24]

    Rewrite-based equational theorem proving with selection and simplification,

    L. Bachmair and H. Ganzinger, “Rewrite-based equational theorem proving with selection and simplification,”Journal of Logic and Com- putation, vol. 4, no. 3, pp. 217–247, 1994

    1994

  25. [25]

    Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T),

    R. Nieuwenhuis, A. Oliveras, and C. Tinelli, “Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T),”Journal of the ACM, vol. 53, no. 6, pp. 937– 977, 2006

    2006

  26. [26]

    Autoformalization with large language models,

    Y . Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy, “Autoformalization with large language models,” inAdvances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022,

    2022

  27. [27]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,

    A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y . Wu, “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,” inThe Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. [Online]. Available: https://openreview.net/f...

    2023

  28. [28]

    Z3: An efficient SMT solver,

    L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” inTools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), ser. Lecture Notes in Computer Science, vol. 4963. Springer, 2008, pp. 337–340

    2008

  29. [29]

    cvc5: A versatile and industrial-strength SMT solver,

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzli, A. Ozdemir, M. Preiner, A. Reynolds, Y . Sheng, C. Tinelli, and Y . Zohar, “cvc5: A versatile and industrial-strength SMT solver,” inTools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), ser. Lecture Notes in Comput...

    2022

  30. [30]

    Faster, higher, stronger: E 2.3,

    S. Schulz, S. Cruanes, and P. Vukmirovi ´c, “Faster, higher, stronger: E 2.3,” inAutomated Deduction – CADE 27, ser. Lecture Notes in Computer Science, vol. 11716. Springer, 2019, pp. 495–507

    2019

  31. [31]

    First-order proof tactics in higher-order logic theorem provers,

    J. Hurd, “First-order proof tactics in higher-order logic theorem provers,” inDesign and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), ser. NASA Conference Publication, no. NASA/CP- 2003-212448, 2003, pp. 56–68

    2003

  32. [32]

    MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics,

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

    2022

  33. [33]

    Neural theorem proving for verification conditions: A real-world benchmark,

    Q. Xu, X. Luan, R. Wang, J. O. J. Leang, P. Wang, H. Li, W. Li, and C. Watt, “Neural theorem proving for verification conditions: A real-world benchmark,”CoRR, vol. abs/2601.18944, 2026. [Online]. Available: https://doi.org/10.48550/arXiv.2601.18944

    work page doi:10.48550/arxiv.2601.18944 2026

  34. [34]

    Prompt caching,

    Anthropic, “Prompt caching,” Claude Platform Documentation, https://platform.claude.com/docs/en/build-with-claude/prompt-caching, accessed 2026-06-21

    2026

  35. [35]

    Minilang-afp-v1,

    A Neural Theorem Proving Group, “Minilang-afp-v1,” https:// huggingface.co/datasets/ANTPG/Minilang-AFP-v1, Dec. 2025, hugging Face dataset. License: CC-BY-4.0

    2025

  36. [36]

    An in-context learning agent for formal theorem-proving,

    A. Thakur, G. Tsoukalas, Y . Wen, J. Xin, and S. Chaudhuri, “An in-context learning agent for formal theorem-proving,” in First Conference on Language Modeling, 2024. [Online]. Available: https://openreview.net/forum?id=V7HRrxXUhN

    2024

  37. [37]

    Prover agent: An agent-based framework for formal mathematical proofs,

    K. Baba, C. Liu, S. Kurita, and A. Sannai, “Prover agent: An agent-based framework for formal mathematical proofs,”CoRR, vol. abs/2506.19923,

    arXiv

  38. [38]

    Archon: An architecture search framework for inference-time techniques,

    J. Saad-Falcon, A. G. Lafuente, S. Natarajan, N. Maru, H. Todorov, E. K. Guha, E. K. Buchanan, M. F. Chen, N. Guha, C. R ´e, and A. Mirhoseini, “Archon: An architecture search framework for inference-time techniques,”CoRR, vol. abs/2409.15254, 2024. [Online]. Available: https://doi.org/10.48550/arXiv.2409.15254

    Pith/arXiv arXiv doi:10.48550/arxiv.2409.15254 2024

  39. [39]

    Leap: Supercharging llms for formal mathematics with agentic frameworks,

    P.-N. Kung, L. Song, D. Hwang, J. Yoon, C.-L. Li, S. Severini, M. Olˇs´ak, E. Lockhart, Q. V . Le, B. Gokturket al., “Leap: Supercharging llms for formal mathematics with agentic frameworks,”arXiv preprint arXiv:2606.03303, 2026

    Pith/arXiv arXiv 2026

  40. [40]

    Abstract syntax networks for code generation and semantic parsing,

    M. Rabinovich, M. Stern, and D. Klein, “Abstract syntax networks for code generation and semantic parsing,” inProceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), R. Barzilay and M.-Y . Kan, Eds. Vancouver, Canada: Association for Computational Linguistics, Jul. 2017, pp. 1139–1149. [Online]. Ava...

    2017

  41. [41]

    Tree-to-tree neural networks for program translation,

    X. Chen, C. Liu, and D. Song, “Tree-to-tree neural networks for program translation,” inProceedings of the 32nd International Conference on Neural Information Processing Systems, ser. NIPS’18. Red Hook, NY , USA: Curran Associates Inc., 2018, p. 2552–2562

    2018

  42. [42]

    TRANX: A transition-based neural abstract syntax parser for semantic parsing and code generation,

    P. Yin and G. Neubig, “TRANX: A transition-based neural abstract syntax parser for semantic parsing and code generation,” inProceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, EMNLP 2018: System Demonstrations, Brussels, Belgium, October 31 - November 4, 2018, E. Blanco and W. Lu, Eds. Association for Computational Ling...

    work page doi:10.18653/v1/d18-2002 2018

  43. [43]

    Treegen: A tree-based transformer architecture for code generation,

    Z. Sun, Q. Zhu, Y . Xiong, Y . Sun, L. Mou, and L. Zhang, “Treegen: A tree-based transformer architecture for code generation,” inThe Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial...

    2020

  44. [44]

    Learning to fix build errors with graph2diff neural networks,

    D. Tarlow, S. Moitra, A. Rice, Z. Chen, P. Manzagol, C. Sutton, and E. Aftandilian, “Learning to fix build errors with graph2diff neural networks,” inICSE ’20: 42nd International Conference on Software Engineering, Workshops, Seoul, Republic of Korea, 27 June - 19 July, 2020. ACM, 2020, pp. 19–20. [Online]. Available: https://doi.org/10.1145/3387940.3392181

    arXiv 2020

  45. [45]

    Graph-based, self-supervised program repair from diagnostic feedback,

    M. Yasunaga and P. Liang, “Graph-based, self-supervised program repair from diagnostic feedback,” inInternational Conference on Machine Learning. PMLR, 2020, pp. 10 799–10 808

    2020

  46. [46]

    Kimi k2: Open agentic intelligence,

    K. Team, Y . Bai, Y . Bao, Y . Charles, C. Chen, G. Chen, H. Chen, H. Chen, J. Chen, N. Chenet al., “Kimi k2: Open agentic intelligence,” arXiv preprint arXiv:2507.20534, 2025

    Pith/arXiv arXiv 2025

  47. [47]

    Glm-5: from vibe coding to agentic engineer- ing,

    A. Zeng, X. Lv, Z. Hou, Z. Du, Q. Zheng, B. Chen, D. Yin, C. Ge, C. Huang, C. Xieet al., “Glm-5: from vibe coding to agentic engineer- ing,”arXiv preprint arXiv:2602.15763, 2026

    Pith/arXiv arXiv 2026

  48. [48]

    Proof by pointing,

    Y . Bertot, G. Kahn, and L. Th ´ery, “Proof by pointing,” inTheoretical Aspects of Computer Software, M. Hagiya and J. C. Mitchell, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1994, pp. 141–160

    1994

  49. [49]

    Proofviz: An interactive visual proof ex- plorer,

    D. Melcer and S. Chang, “Proofviz: An interactive visual proof ex- plorer,” inTrends in Functional Programming, V . Zs ´ok and J. Hughes, Eds. Cham: Springer International Publishing, 2021, pp. 116–135

    2021

  50. [50]

    Henblocks: Structured editing for coq,

    B. Boey and M. D. Adams, “Henblocks: Structured editing for coq,” in The Coq Workshop, vol. 2022, 2022, p. 2

    2022

  51. [51]

    Pythagoras-prover: Advancing efficient formal proving via augmented lean formalisation,

    J. O. J. Leang, Z. Zhao, M. C. Stoian, Q. Xu, H. Li, W. Li, S. B. Cohen, and E. Giunchiglia, “Pythagoras-prover: Advancing efficient formal proving via augmented lean formalisation,”arXiv preprint arXiv:2606.12594, 2026

    Pith/arXiv arXiv 2026

  52. [52]

    Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction,

    Y . Lin, S. Tang, B. Lyu, Z. Yang, J.-H. Chung, H. Zhao, L. Jiang, Y . Geng, J. Ge, J. Sun, J. Wu, J. Gesi, X. Lu, D. Acuna, K. Yang, H. Lin, Y . Choi, D. Chen, S. Arora, and C. Jin, “Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction,” inThe Fourteenth International Conference on Learning Representations, ...

    2026

  53. [53]

    Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning,

    H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, J. Lu, H. de Saxc ´e, B. Bailey, C. Song, C. Xiao, D. Zhang, E. Zhang, F. Pu, H. Zhu, J. Liu, J. Bayer, J. Michel, L. Yu, L. Dreyfus-Schmidt, L. Tunstall, L. Pagani, M. Machado, P. Bourigault, R. Wang, S. Polu, T. Barroyer, W.-D. Li, Y . Niu, Y . Fleureau, Y ....

    Pith/arXiv arXiv 2025

  54. [54]

    Oprover: A unified framework for agentic formal theorem proving,

    D. Ma, K. Ma, S. Guo, Y . Shi, E. Zhao, J. Shi, Z. Zhang, G. Cheung, J. Liu, and Z. Wang, “Oprover: A unified framework for agentic formal theorem proving,”arXiv preprint arXiv:2605.17283, 2026

    Pith/arXiv arXiv 2026

  55. [55]

    Longcat-flash- prover: Advancing native formal reasoning via agentic tool-integrated reinforcement learning,

    J. Wang, J. Zhang, Q. Guo, L. Guo, R. Li, C. Zhang, C. Peng, C. Wang, D. Zhao, J. Shi, J. Wang, L. Feng, M. Shen, Q. Li, S. An, S. Wang, W. Shi, X. Xi, X. Li, X. Cao, Y . Lu, Y . Zhao, Z. Chen, Z. Lin, W. Wang, P. Pei, and X. Cai, “Longcat-flash- prover: Advancing native formal reasoning via agentic tool-integrated reinforcement learning,”CoRR, vol. abs/2...

    doi:10.48550/arxiv.2603.21065 2026

  56. [56]

    STP: self-play LLM theorem provers with iterative conjecturing and proving,

    K. Dong and T. Ma, “STP: self-play LLM theorem provers with iterative conjecturing and proving,” inForty-second International Conference on Machine Learning, ICML 2025, Vancouver, BC, Canada, July 13-19, 2025, ser. Proceedings of Machine Learning Research, A. Singh, M. Fazel, D. Hsu, S. Lacoste-Julien, F. Berkenkamp, T. Maharaj, K. Wagstaff, and J. Zhu, E...

    2025

  57. [57]

    Theorem prover as a judge for synthetic data generation,

    J. O. J. Leang, G. Hong, W. Li, and S. B. Cohen, “Theorem prover as a judge for synthetic data generation,” inProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), W. Che, J. Nabende, E. Shutova, and M. T. Pilehvar, Eds. Vienna, Austria: Association for Computational Linguistics, Jul. 2025, pp. 29...

    2025

  58. [58]

    FATE: A formal benchmark series for frontier algebra of multiple difficulty levels,

    J. Jiang, W. He, Y . Wang, G. Gao, Y . Hu, J. Wang, N. Guan, P. Wu, C. Dai, L. Xiao, and B. Dong, “FATE: A formal benchmark series for frontier algebra of multiple difficulty levels,”CoRR, vol. abs/2511.02872, 2025. [Online]. Available: https://doi.org/10.48550/ arXiv.2511.02872

    doi:10.48550/arxiv.2511.02872 2025

  59. [59]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics,

    Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad, “Proofnet: Autoformalizing and formally proving undergraduate-level mathematics,”CoRR, vol. abs/2302.12433, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2302.12433

    Pith/arXiv arXiv doi:10.48550/arxiv.2302.12433 2023

  60. [2022]

    Available: http://papers.nips.cc/paper files/paper/2022/ hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html

    [Online]. Available: http://papers.nips.cc/paper files/paper/2022/ hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html

    2022

  61. [2025]

    Available: https://doi.org/10.48550/arXiv.2506.19923

    [Online]. Available: https://doi.org/10.48550/arXiv.2506.19923

    doi:10.48550/arxiv.2506.19923

  62. [2026]

    Available: https://arxiv.org/abs/2604.03789

    [Online]. Available: https://arxiv.org/abs/2604.03789

    Pith/arXiv arXiv