Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

A planning-first decomposer that lets an LLM propose sublemmas and a hammer prove them lifts Rocq proof success by 7–13 percentage points.

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-02 11:00 UTC pith:24OAX45K

load-bearing objection A credible planning-then-hammer system with honest ablations; headline margins are plausible but rest on single stochastic runs. the 3 major comments →

arxiv 2606.17981 v2 pith:24OAX45K submitted 2026-06-16 cs.SE

Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs

Ning Zhang , Nongyu Di , Zenan Li , Yuan Yao , Xiaoxing Ma This is my paper
classification cs.SE
keywords formal verificationproof synthesisinteractive theorem provinglarge language modelsproof decompositiondifficulty estimationRocqhammer-style automation
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.

This paper tries to establish that the ceiling on automated verification proofs is not the strength of tactic-level search but the absence of long-range planning — and that a system which separates planning from execution can beat both a pure language-model prover and a pure hammer-style prover. Its proposal is to let an LLM propose decompositions of a hard goal into sublemmas, have the prover check that the plan would close the goal, and then pick the plan whose hardest piece is most likely solvable by automated tactics, recursing on any piece that is not. Under a uniform ten-minute budget the system reports success rates of 55%, 52%, and 16% on three Rocq benchmarks, outperforming the strongest baseline by seven to thirteen percentage points while using fewer LLM requests. If that claim holds, proof automation for program verification becomes a planning problem solvable with off-the-shelf language models plus a trusted tactic engine, rather than a search problem needing unbounded proof depth.

Core claim

At the center of the paper is the claim that a goal too hard for automation can be solved by turning it into several easier goals, and that the planner can decide which decomposition is worth trying before spending any proof budget. The system samples up to eight candidate decompositions from an LLM, each listing sublemmas and a target tactic script; Rocq verifies each candidate by type-checking it with the sublemmas temporarily admitted. A linear difficulty model then scores each sublemma from features of its normalized proof state, and the candidate whose hardest sublemma has the lowest predicted difficulty is tried first, recursively, with the same loop applied to any sublemma the hammer

What carries the argument

The load-bearing mechanism is the solvability-aware ranker: a learned linear score over 28 proof-state features. Nineteen features are computed after executing a short normalizing tactic prefix (repeated introductions) on each proposed sublemma, so they describe the proof state the automation backend will actually see; nine come from the raw lemma statement. Weights are learned offline, on traces in which every candidate at every node was attempted, using a pairwise margin-ranking objective that encodes 'the candidate whose hardest sublemma was solved should score lower.' Candidate plans are ranked by the maximum estimated difficulty over their sublemmas — a deliberate bottleneck policy, jus

Load-bearing premise

The load-bearing premise is that every hard proof goal can be split by an LLM into a tree of sublemmas that individual automated-tactic calls can each finish within a recursion depth of five; if a proof is one long sequential chain with no natural split points, the planner has nothing to work with and the method falls back to the hammer's own success level.

What would settle it

Collect about 50 Rocq theorems whose human proofs are single chains of 20 or more rewrites and unfolds with no intermediate assertions. The paper's own failure analysis predicts the system would solve roughly as many as the hammer alone, leaving the planning layer no purchase. If it solves a large share, decomposition is not the active ingredient; a complementary check is to replay recorded traces with the difficulty rankings inverted, which should push success below the unranked baseline if the ranker is doing the work.

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

If this is right

  • Most successful proofs finish under five minutes, with a median of one to two minutes, and solved goals require on average fewer than two sublemmas — so a single level of decomposition usually suffices.
  • The framework's gains compound with the execution engine: using a stronger leaf-goal solver in place of the default hammer adds ten more solved theorems across the three benchmark sets.
  • Ranking policy matters more than generation volume: bottleneck (maximum) aggregation beats mean and sum aggregations, and normalized proof-state features transfer across benchmark distributions better than raw statement statistics.
  • Raising per-node rollout beyond about twelve candidates yields diminishing returns, while swapping in a stronger LLM backend lifts success rates further — performance tracks both planning breadth and model capability.

Where Pith is reading between the lines

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

  • A natural stress test follows from the paper's own failure analysis: on theorems whose human proofs are long sequential rewrite chains with no intermediate assertions, the planner should contribute nothing and performance should sit near the hammer baseline; a system that passes this test would need an execution-feedback loop that the current one-shot pipeline lacks.
  • The same Generate–Rank–Solve scaffold is portable: any interactive prover with a trusted local automation could adopt it, with the difficulty model retrained on that backend's traces; the paper's transfer results suggest the normalized proof-state features are relatively backend-agnostic.
  • The bottleneck-ranking principle generalizes beyond proving: any synthesis task with a costly recursive step could rank candidates by the hardest sub-obligation, since the convexity argument for splitting tasks into balanced subtasks is not specific to logic.

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 presents Quarry, a Rocq proof-synthesis framework that separates planning from execution: an LLM proposes candidate decompositions into sublemmas and a target tactic script; Rocq-side verification (via SerAPI) checks conditional type-correctness of each candidate; a learned linear difficulty model ranks candidates by predicted hammer solvability; and CoqHammer recursively discharges sublemmas under a bounded budget (a Generate–Rank–Solve loop). The difficulty weights are trained offline on 200 CoqGym goals from projects disjoint from the three evaluation benchmarks. Evaluated on CoqGym100, Wigderson100, and a new TransBench58, Quarry reports success rates of 55%, 52%, and 16%, improving over the strongest baseline (PALM) by 7–13 percentage points under a uniform 10-minute budget. Ablations show that ranking and hammer-at-every-node contribute, that rollout budget gains plateau, and that offline replay is used for ranking ablations. The paper honestly acknowledges limitations: sequential proofs lacking decomposition structure remain the main failure mode, the pipeline is one-shot, and the overall ceiling is largely set by CoqHammer.

Significance. If the empirical claims are robust, this is a useful step for proof automation: it combines LLM high-level planning with hammer-style local execution, introduces arbitrary intermediate lemmas rather than only built-in subgoal splitting, and ranks candidates with a lightweight proof-state difficulty model that is not tuned on the test benchmarks. Strengths include project-level disjointness of difficulty-model training data from the test benchmarks, a reproducible artifact, a bounded-cost design, and a modular leaf-solver architecture. The main credibility gap is the empirical evaluation: the headline margins rest on single stochastic runs, some baseline entries are N/A without explanation, and the offline-replay evaluation assumes a strong order-independence property. These issues are load-bearing for the central claim but appear fixable, so the paper warrants major revision rather than rejection.

major comments (3)
  1. [Section 6.5 / Table 2] The headline margins rest on a single GPT-5.2 run at temperature 1.0. The text states that the reported main results are single runs, so there is no estimate of sampling variability for the claimed +7 to +13 percentage-point gains. The repeated MiniMax-M2.5 runs (at most 1.5 pp standard deviation) are a different backend and cannot be transferred to GPT-5.2. TransBench58 is especially fragile: 16% vs 3% is 9 vs 2 theorems out of 58, so a difference of two or three successful theorems on either side changes the claimed margin. Please report at least three independent GPT-5.2 runs (or a bootstrap over the theorem set) and the per-run success sets, and qualify the central claim accordingly.
  2. [Table 2 / Section 6.1.2] The text says 'All baselines are re-run under our Rocq toolchain and evaluation budget,' but Table 2 reports N/A for Tactician on CoqGym100 and for Rango on CoqGym100 and Wigderson100. No explanation is given. This is an internal inconsistency that weakens the 'outperforms all baselines' framing. Either run these baselines or state concretely why they are N/A (e.g., version incompatibility) and restrict the claim to the systems actually compared.
  3. [Section 5.5 / Table 5] The offline-replay evaluation assumes that re-ranking candidates at each node yields the same recursive outcomes as online execution regardless of the original execution order. This is not automatically true: the runner maintains a shared proven-context, so whether a sublemma is already available can depend on which candidates were attempted earlier; wall-clock and LLM-budget consumption also depend on trial order. The assertion that 're-ranking produces valid end-to-end results regardless of the original execution order' is stated without validation. Please either validate replay predictions against live runs on a subsample of theorems or state and justify the order-independence assumption and its limitations.
minor comments (4)
  1. [Algorithm 2] Lines 5–6 compute scores using the weights θ before θ has been learned. The pseudocode should make clear that the margin objective is parameterized by θ, e.g., define s_i(θ) and s_j(θ) and then optimize over θ.
  2. [Section 6.2] The Quarry+Cobblestone leaf-solver comparison uses a 20-minute wall-clock budget, whereas Table 2 uses 10 minutes. This should be stated more prominently so the 'additional 10 theorems' result is not read as a controlled comparison under the same budget.
  3. [Table 2] Consider reporting the raw counts alongside percentages on TransBench58 (e.g., 16% (9/58)) in the table itself, since the percentage is rounded over a small denominator.
  4. [Section 6.1.4] The per-theorem LLM budget of 60 requests is stated as matching Cobblestone's effective budget, but it is not clear whether all LLM baselines (PALM, ChainOfThought, Rango) are subject to the same 60-request cap or only the 10-minute wall-clock limit. A sentence clarifying this would improve fairness of interpretation.

Circularity Check

0 steps flagged

No significant circularity: the central claim is an empirical comparison against external baselines, and the only learned component is trained on held-out, project-disjoint goals.

full rationale

The paper's central claim is empirical—Quarry's success rates on three benchmarks versus external baselines—not a derivation from a fitted parameter. The only learned component, the difficulty model, is explicitly trained on held-out data: "The difficulty model weights θ are trained on 200 goals from CoqGym projects disjoint from all three evaluation benchmarks" (Section 5.5/6.1.4), and is "applied without further tuning to the three benchmarks" (Table 5 caption). The training traces are collected in dense-supervision mode where the system "continues to attempt all remaining candidates at each node even after a success," so candidate outcomes are recorded independently of the ranking policy, avoiding a self-fulfilling prediction. The evaluation compares Quarry against external baselines (CoqHammer, Proverbot9001, Tactician, ChainOfThought, PALM, Rango, Cobblestone) under a uniform budget, and the final proofs are checked by the Rocq kernel. Self-citations appear only in related-work positioning (e.g., Goedel-Code-Prover, seL4-prover) and do not carry the argument. No equation reduces a prediction to a fitted input, no uniqueness theorem is imported from the authors' prior work, and no known result is merely renamed. The stated limitations (e.g., "the overall ceiling is largely determined by CoqHammer's capabilities") are honest boundary conditions, not circular steps.

Axiom & Free-Parameter Ledger

4 free parameters · 5 axioms · 0 invented entities

No new physical or logical entities are introduced. The framework's novelty is structural (planning/execution separation, difficulty ranker); the 'difficulty model' is a learned parameter vector, not a new entity. The main fitted components are the difficulty-model weights and search hyperparameters.

free parameters (4)
  • difficulty model weights θ (28 features + bias) = not reported numerically
    Learned offline via margin ranking loss on 200 CoqGym goals; used to score every sublemma in evaluation (Sections 5.4–5.5).
  • search budget hyperparameters = k=8, B=1, depth=5, LLM cap=60, hammer timeout=30s, LLM timeout=90s
    Chosen by hand (Section 6.1); success rates and cost depend on these.
  • aggregation function for candidate score = max over sublemma difficulties
    Chosen as default; ablation (Table 5) shows max is best, but it is a design choice not derived.
  • feature set composition = 28 features (19 intros-state + 9 statement)
    Hand-selected; ablation shows the full set is best, but selection is heuristic (Table 1, Section 5.3).
axioms (5)
  • standard math Rocq kernel and CoqHammer's reconstruction are sound (final proofs are kernel-checked).
    Evaluation treats any theorem closed by Rocq's kernel as proved; CoqHammer reconstruction is trusted (Sections 2.2, 4.3).
  • domain assumption The LLM produces at least one valid candidate decomposition for a nontrivial fraction of provable goals.
    Generate phase depends on LLM outputs being parseable and type-checking with Admitted sublemmas; without this the system reduces to CoqHammer alone (Section 4.2).
  • domain assumption Sublemma difficulty (hammer solvability) correlates with the 28 hand-chosen proof-state features.
    The ranking pipeline (Sections 5.2–5.4) is built on this correlation; it is tested indirectly via RQ5 but not proven.
  • domain assumption Candidate outcomes in recorded traces are order-independent under re-ranking (shared proven-context does not change success).
    Offline replay claims re-ranking produces valid end-to-end results 'regardless of the original execution order' (Section 5.5); the shared proven-context could break this.
  • domain assumption TransBench58 translations faithfully represent Rust/Verus verification problems.
    The new benchmark is used for the third evaluation; correctness of translation is asserted via automated pipeline + LLM + manual review (Section 6.1.1).

pith-pipeline@v1.3.0-alltime-deepseek · 24360 in / 14134 out tokens · 125401 ms · 2026-08-02T11:00:39.779626+00:00 · methodology

0 comments
read the original abstract

As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor, while automated tactics such as CoqHammer can reliably discharge many local goals but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model that estimates hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7% to 13% in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either.

Figures

Figures reproduced from arXiv: 2606.17981 by Ning Zhang, Nongyu Di, Xiaoxing Ma, Yuan Yao, Zenan Li.

Figure 1
Figure 1. Figure 1: Proof tree for max_deg_remove_node found by Quarry. The tree has depth 3 and 12 nodes. Green leaves are discharged by CoqHammer or simple induction; blue nodes required further decomposition. Each leaf involves only one or two definitions, making it tractable for automation. • degree_remove_node_preserve: removing a non-adjacent node preserves the degree of 𝑣 (re￾quires one further sublemma about set cardi… view at source ↗
Figure 2
Figure 2. Figure 2: Quarry workflow. Given a goal, the system enters the Generate–Rank–Solve loop: the LLM proposes 𝑘 candidate decompositions, which are filtered by Rocq-side verification (Admitted sublemmas); the diffi￾culty model ranks survivors by estimated solvability; and the top-𝐵 candidates are recursively solved using automation tools (e.g., CoqHammer). Unsolved subgoals re-enter the loop (dashed arrow). The bottom r… view at source ↗
Figure 3
Figure 3. Figure 3: How Quarry processes the root goal of the running example through the Generate–Rank pipeline. The LLM produces a structured decomposition; Rocq verification (part of Generate) confirms conditional correctness; the difficulty model estimates sublemma solvability. candidate–outcome mapping needed to evaluate alternative ranking policies without new LLM calls. 5 Difficulty-Aware Ranking and Learning Recall th… view at source ↗
Figure 4
Figure 4. Figure 4: Cumulative success rate vs. wall-clock time. Over 90% of successful proofs complete within 5 minutes; [PITH_FULL_IMAGE:figures/full_fig_p017_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: reports per-theorem token usage and LLM request counts for Quarry and Cobblestone on the three benchmarks. Quarry uses fewer requests per theorem than Cobblestone on all benchmarks (e.g., 7.2 vs. 11.5 on CoqGym100) while proving more theorems, reflecting the efficiency of difficulty-aware ranking in avoiding fruitless decomposition paths. On Wigderson100, Quarry’s per-theorem token usage is higher (45.6K v… view at source ↗
Figure 6
Figure 6. Figure 6: Effect of rollout budget 𝑘 on the number of proved theorems. The default 𝑘=8 captures most of the benefit; gains plateau beyond 𝑘=12. Takeaway. Both ranking and deep CoqHammer integration are individually significant. Ranking steers the budget toward hammer-solvable decompositions, while invoking CoqHammer at every node captures leaf-level goals that LLM-only methods miss. 6.5 RQ4: Budget Sensitivity, LLM … view at source ↗
Figure 7
Figure 7. Figure 7: Effect of leaf-goal solver. Replacing CoqHam [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗

Review history (2 revisions) →

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

    cs.AI 2026-07 conditional novelty 6.0

    Typed local edits on Lean proof blueprints match free-form repair coverage on localized defects while using far fewer tokens and lower cost.

Reference graph

Works this paper leans on

28 extracted references · 4 linked inside Pith · cited by 1 Pith paper

  1. [7]

    InIEEE Symposium on Security and Privacy (S&P)

    Simple High-Level Code for Crypto- graphic Arithmetic — With Proofs, Without Compromises. InIEEE Symposium on Security and Privacy (S&P). 1202–1219. doi:10.1109/SP.2019.00005 Proc. ACM Program. Lang., Vol. 1, No. 1, Article . Publication date: June

    arXiv 2019

  2. [8]

    Emily First, Markus N

    TacTok: Semantics-aware proof synthesis.Proceedings of the ACM on Programming Languages4, OOPSLA (2020), 1–31. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun

    2020

  3. [10]

    Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever

    Neuro-symbolic proof generation for scaling systems software verification.arXiv preprint arXiv:2603.19715(2026). Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever

    Pith/arXiv arXiv 2026

  4. [12]

    InProceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE)

    Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification. InProceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE). Rio de Janeiro, Brazil. doi:10.1145/3744916.3773178 Xavier Leroy

    arXiv

  5. [15]

    Aixin Liu, Aoxue Mei, Bangcai Lin, Bing Xue, Bingxuan Wang, Bingzheng Xu, Bochao Wu, Bowei Zhang, Chaofan Lin, Chen Dong, et al

    Goedel-code-prover: Hierarchical proof search for open state-of-the-art code verification.arXiv preprint arXiv:2603.19329(2026). Aixin Liu, Aoxue Mei, Bangcai Lin, Bing Xue, Bingxuan Wang, Bingzheng Xu, Bochao Wu, Bowei Zhang, Chaofan Lin, Chen Dong, et al

    arXiv 2026

  6. [17]

    In39th IEEE/ACM International Conference on Automated Software Engineering (ASE ’24), October 27-November 1, 2024, Sacramento, CA, USA

    Proof Automation with Large Language Models. In39th IEEE/ACM International Conference on Automated Software Engineering (ASE ’24), October 27-November 1, 2024, Sacramento, CA, USA. ACM, New York, NY, USA, 1509–1520. doi:10.1145/3691620.3695521 Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian ...

    arXiv 2024

  7. [18]

    InThe Twelfth International Conference on Learning Representations

    Magnushammer: A Transformer-Based Approach to Premise Selection. InThe Twelfth International Conference on Learning Representations. https://openreview.net/forum?id=oYjPk8mqAV MiniMax. 2026.MiniMax M2.5: Built for Real-World Productivity.Technical Report. https://minimaxi.com/news/minimax-m25 Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002.Isab...

    2026

  8. [19]

    InCompanion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software Proc

    Towards the Formal Verification of Wigderson’s Algorithm. InCompanion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software Proc. ACM Program. Lang., Vol. 1, No. 1, Article . Publication date: June

    2023

  9. [20]

    for Humanity(Cascais, Portugal)(SPLASH 2023)

    26 Zhang et al. for Humanity(Cascais, Portugal)(SPLASH 2023). Association for Computing Machinery, New York, NY, USA, 40–42. doi:10.1145/3618305.3623600 Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman

    arXiv 2023

  10. [22]

    InProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL ’20), June 15, 2020, London, UK

    Generating Correctness Proofs with Neural Networks. InProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL ’20), June 15, 2020, London, UK. ACM, New York, NY, USA, 1–10. https://doi.org/10.1145/3394450.3397466 Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer

    arXiv 2020

  11. [23]

    Passport: Improving Automated Formal Verification Using Identifiers.ACM Trans. Program. Lang. Syst.45, 2, Article 12 (2023), 30 pages. https://doi.org/10.1145/3593374 The Coq Development Team

    doi:10.1145/3593374 2023

  12. [24]

    Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng YANG, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang

    Hilbert: Recursively building formal proofs with informal reasoning.arXiv preprint arXiv:2509.22819(2025). Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng YANG, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2024a. Proving Theorems Recursively. InThe Thirty-eighth Annual Conference on Neural Information Processi...

    arXiv 2025

  13. [25]

    Chain-of-Thought Prompting Elicits Reasoning in Large Language Models.Advances in Neural Information Processing Systems35 (2022), 24824–24837. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson

    2022

  14. [26]

    InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

    Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, New York, NY, USA, 357–368. doi:10.1145/2737924.2737958 Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuve...

    arXiv 2025

  15. [27]

    ACM69, 3 (2026), 66–73

    Formal reasoning meets llms: Toward ai for mathematics and verification.Commun. ACM69, 3 (2026), 66–73. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    2026

  16. [36]

    21573–21612. Proc. ACM Program. Lang., Vol. 1, No. 1, Article . Publication date: June 2026

    2026

  17. [2009]

    doi:10.1145/1538788.1538814 Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh

    Formal verification of a realistic compiler.Communications of the ACM (CACM)52, 7 (2009), 107–115. doi:10.1145/1538788.1538814 Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh

    arXiv 2009

  18. [2014]

    doi:10.1007/s10817-013-9286-5 Alexander A

    Premise selection for mathematics by corpus analysis and kernel methods.Journal of Automated Reasoning52, 2 (2014), 191–213. doi:10.1007/s10817-013-9286-5 Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban

    doi:10.1007/s10817-013-9286-5 2014

  19. [2015]

    InProceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP)

    Using Crash Hoare Logic for Certifying the FSCQ File System. InProceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP). ACM, New York, NY, USA, 18–37. doi:10.1145/2815400.2815402 Łukasz Czajka and Cezary Kaliszyk

    arXiv

  20. [2018]

    doi:10.1007/s10817-018-9458-4 Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala

    Hammer for Coq: Automation for Dependent Type Theory.Journal of Automated Reasoning61, 1-4 (2018), 423–453. doi:10.1007/s10817-018-9458-4 Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala

    doi:10.1007/s10817-018-9458-4 2018

  21. [2019]

    Lasse Blaauwbroek, Mirek Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun

    Learning to Reason in Large Theories without Imitation.arXiv preprint arXiv:1905.10501(2019). Lasse Blaauwbroek, Mirek Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun

    Pith/arXiv arXiv 1905

  22. [2020]

    InInternational Conference on Intelligent Computer Mathematics

    The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq. InInternational Conference on Intelligent Computer Mathematics. 271–277. doi:10.1007/978-3-030-53518-6_17 Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang

    doi:10.1007/978-3-030-53518-6_17

  23. [2021]

    InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21), June 20-25, 2021, Virtual, Canada

    Proof Repair Across Type Equivalences. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21), June 20-25, 2021, Virtual, Canada. ACM, New York, NY, USA, 112–127. doi:10.1145/3453483.3454033 Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner

    arXiv 2021

  24. [2022]

    In Advances in Neural Information Processing Systems

    Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems. 8360–8373. https://proceedings.neurips.cc/paper_files/paper/2022/ file/377c25312668e48f2e531e2f2c422483-Paper-Conference.pdf Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Ma...

    2022

  25. [2023]

    Baldur: Whole-Proof Generation and Repair with Large Language Models. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’23), December 3-9, 2023, San Francisco, CA, USA. ACM, New York, NY, USA, 1229–1241. https://doi.org/10.1145/3611643.3616243 Emilio Jesús Galle...

    arXiv 2023

  26. [2024]

    Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, and Chi Jin

    A Survey on Deep Learning for Theorem Proving.arXiv preprint arXiv:2404.09939(2024). Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, and Chi Jin

    Pith/arXiv arXiv 2024

  27. [2025]

    Minghai Lu, Benjamin Delaware, and Tianyi Zhang

    Deepseek-v3.2: Pushing the frontier of open large language models.arXiv preprint arXiv:2512.02556 (2025). Minghai Lu, Benjamin Delaware, and Tianyi Zhang

    Pith/arXiv arXiv 2025

  28. [2026]

    Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M

    Reviving DSP for advanced theorem proving in the era of reasoning models.Advances in Neural Information Processing Systems38 (2026), 74116– 74154. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

    2026