Pith. sign in

REVIEW 5 major objections 6 minor 3 cited by

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

T0 review · 5 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read A dual-model framework that blends whole-proof synthesis with stepwise tactic refinement reaches 59.4 percent on Isabelle's miniF2F benchmark, topping the prior 56.1 percent.

desk verdict The dual-model sketch-refinement idea is genuinely novel, but the 59.4% headline is not yet trustworthy because the evaluation never rules out `sorry` in the final proofs. read the letter →

arxiv 2505.15740 v1 pith:SR6U6AJG submitted 2025-05-21 cs.FL cs.AIcs.SE

Jilin Hu , Jianyu Zhang , Yongwang Zhao , Talia Ringer This is my paper
classification cs.FLcs.AIcs.SE
keywords automatedtheoremprovinglargelanguagemodelsIsabelle/HOLproofsketchestactic-basedgenerationwhole-proofsynthesisminiF2FSledgehammer
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper argues that the two dominant LLM strategies for automated theorem proving—generating a whole proof at once and generating one tactic at a time—are complementary, and that a system joining them outperforms either alone. HybridProver first produces whole proof candidates, checks them in Isabelle, and mechanically converts unsuccessful candidates into proof sketches by replacing tactic details with the placeholder 'sorry'. A second, tactic-focused model then refines each sketch subgoal by subgoal, with help from Sledgehammer, until the checker accepts a complete proof. On the 244-theorem Isabelle miniF2F test set the system proves 59.4 percent of theorems, improving on the reported 56.1 percent state of the art. The paper also reports ablations showing how dataset purification, training hyperparameters, and sampling diversity affect success.

What carries the argument

The load-bearing object is the proof sketch, built mechanically from a whole-proof candidate by replacing every subgoal's proof tactic with the keyword 'sorry' and then checking the result in Isabelle. The sketch carries the argument by separating high-level proof structure from low-level tactic detail: the whole-proof model supplies the structure, and the tactic-based model, augmented by Sledgehammer and a fixed set of heuristic proof methods, fills each placeholder. The two models are fine-tuned on a split of a purified PISA-extracted dataset, with Isar-style proofs training the whole-proof model and apply-style proofs training the tactic model.

What would settle it

Search the PISA-extracted AFP and Isabelle/HOL training corpora for exact or near-verbatim copies of each miniF2F test statement; if the theorems HybridProver solves are disproportionately the ones that appear in the training data, the 59.4 percent would be inflated by memorization rather than genuine proof synthesis.

Watch

Extended reading notes

Core claim

HybridProver's central claim is that proof sketches—high-level proof plans with detailed tactics deleted—let a system get the strengths of both LLM proof-writing styles. The paper reports that whole-proof synthesis alone solves 37.7 percent of the Isabelle miniF2F test set, tactic-based generation alone 34.8 percent, their simple union 41.4 percent, tactic-based generation combined with sketch refinement 56.1 percent, and the full HybridProver 59.4 percent. The authors attribute the improvement to the combination rather than to any single component, and note that roughly 90 percent of the mechanically built sketches pass Isabelle's checker when the detailed tactics are omitted, indicating that high-level proof structure is usually right and the remaining work is supplying correct tactics for each subgoal.

Load-bearing premise

The 59.4 percent figure stands on the assumption that the miniF2F test statements are not present or near-identical in the AFP and Isabelle/HOL corpora used to fine-tune the models, so the results reflect generalization rather than memorization.

Editorial extensions

If this is right

  • If correct, HybridProver sets a new published bar on Isabelle miniF2F at 59.4 percent, ahead of SubgoalXL's 56.1 percent.
  • The dual-model design is compositional: any whole-proof synthesis model can be paired with any tactic-based model for the same proof assistant, so future gains in either component should feed directly into the combined system.
  • The roughly 90 percent sketch-pass rate suggests that for this benchmark the hard part is generating correct tactics for each subgoal, not planning the overall proof.
  • The ablation results give a concrete recipe—purified data, three epochs, learning rate e-5, moderate temperature around 0.6 to 0.9, and higher sampling rates—for practitioners fine-tuning LLMs for theorem proving.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the near-total reliability of mechanically built sketches extends beyond miniF2F, the field's bottleneck shifts toward local tactic synthesis, which would argue for investing in stronger step generators or reinforcement learning on step sequences rather than in better global planners.
  • Because the comparison with SubgoalXL pairs different base models and different training corpora, a same-base re-run would be needed to separate the contribution of the hybrid architecture itself from the contribution of the stronger Qwen-Coder model and improved data.
  • The apparently large effect of data purification and the near-irrelevance of lora_rank and few-shot examples are reported on this dataset and model family; whether they hold for other proof assistants or more diverse corpora remains an open question.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 6 minor

Summary. The paper proposes HybridProver, a dual-model framework for automated theorem proving in Isabelle/HOL that first generates whole-proof candidates with a fine-tuned LLM, mechanically extracts proof sketches (replacing subgoal details with the Isabelle keyword `sorry`), and then completes the sketches via a tactic-based generation model augmented with Sledgehammer. The authors report 59.4% success on the 244-problem miniF2F test set, claiming a 3.3% improvement over the previous Isabelle SOTA of 56.1% from SubgoalXL. They also present ablations on data purification, fine-tuning hyperparameters, sampling temperature and rate, and the marginal utility of premises, few-shot examples, and labels. All code, datasets, and fine-tuned models are said to be open source.

Significance. HybridProver is a sensible engineering contribution: it is the first framework we are aware of that mechanically extracts Isabelle proof sketches from whole-proof LLM candidates and then completes them with tactic-level generation and Sledgehammer, and the open release of code, datasets, and models is a strength. If the evaluation is sound, the reported 59.4% on miniF2F for Isabelle would be a useful practical advance, and the ablations on data quality, LoRA rank, epochs, and sampling diversity provide actionable guidance for the community. However, the central SOTA claim rests on evaluation-pipeline assumptions that are not stated or verified in the manuscript, and the comparison to prior work is not controlled across base models or training data.

major comments (5)
  1. [Section 3.1, Algorithm 1] The evaluation pipeline contains no check that the final proof returned by IsabelleVerify is free of `sorry`. Because `sorry` is an Isabelle oracle that admits the current goal as an axiom, any proof containing `sorry`—whether from the initial whole-proof model or from the refinement step—passes the checker and is counted as a success. Step 2's proof filter checks only syntax and JSON format, and Step 5's substituteSorry replaces placeholders with generated steps without validating that those steps do not themselves contain `sorry`. Please add an explicit token-level or lexer-level rejection of `sorry` in every candidate and final proof, and report how many of the 145 claimed successes (59.4% of 244) would be discarded under that check.
  2. [Section 4.1, Experimental setup] The base model was chosen as the one "with the highest proof success rate" among more than 15 open-source models. The text does not state that this selection was performed on a held-out validation set; if it was performed on the miniF2F test set, the reported 59.4% is a selection-on-the-test-metric result, not a valid out-of-sample evaluation. Please clarify the selection protocol, and unless selection used a disjoint development set, re-run the final evaluation on a properly held-out split.
  3. [Section 4.1, Dataset] No analysis is reported for overlap between the AFP and Isabelle/HOL training corpora and the miniF2F test set. Since the whole-proof model is trained on 200K+ theorems, memorization of statements similar to miniF2F would directly inflate the headline number. Please report a decontamination check (e.g., exact, normalized, or n-gram overlap of theorem statements) for all 244 test statements, or argue explicitly why overlap cannot occur.
  4. [Section 4.2, Table 1] The SOTA comparison is not controlled across base models, training data, or compute (Llama-3, GPT-3.5, Codex, GPT-4, Qwen-Coder). The claim of a 3.3% improvement over SubgoalXL therefore conflates the method with model and data choices. Please provide matched comparisons (e.g., both methods using the same base model and similar training sets) or clearly state that this is a cross-configuration comparison with the corresponding limitation noted in the text.
  5. [Section 4.2, final run; Section 4.3, Table 3] The sampling temperature T for the final Qwen-Coder-14B run that produced the 59.4% result is not reported. Table 3 shows that T changes the success rate from 20.5% to 31.3% on the 7B model at @32, so the missing T for the final configuration makes the central result irreproducible. Please report T, sampling rate, timeout, and all other sampling parameters for the final configuration in the experimental setup.
minor comments (6)
  1. [Abstract vs. Section 6] The abstract states the previous SOTA is 56.1%, while Section 6 says it is 56.4%; please make these consistent.
  2. [References] The reference "Nick Groom, The Vampire, Yale University Press, 2018" appears to be the novel, not the Vampire automated theorem prover; please cite the correct Vampire system paper.
  3. [Algorithm 1] The identifier T is overloaded: Line 1 uses T for the prompt template and Line 14 uses T for the set of tactic proof steps; please rename one of them to avoid confusion.
  4. [Section 3.1] Figure 1 is referenced but no figure appears in the submitted text; please ensure the framework diagram is included with a caption.
  5. [Section 4.3] Minor typo: "hallucinates many inexisted facts" should be "nonexistent facts."
  6. [Section 4.2] The statement that "most sketches built from the whole-proof synthesis model are correct" with a 90% sketch acceptance rate should be clarified as acceptance under `sorry`, i.e., structural validity of the sketch, not mathematical correctness of the high-level plan.

Circularity Check

1 steps flagged · score 6.0 of 10

The success predicate is defined by an Isabelle checker that the algorithm itself uses to accept `sorry` placeholders, so the reported success rate can reduce to placeholder emission rather than proof.

  1. self definitional [Section 3.1, Steps 3 and 5; Algorithm 1, lines 10-16]
    "we substitute all proof tactics for each subgoal with the keyword sorry in Isabelle. The checker will assume the subgoal is correct when it meet sorry. ... Refine proof sketch p_refined ← substituteSorry(s,T); If IsabelleVerify(p_refined, L)=True return p_refined."

    The headline success rate is defined by IsabelleVerify(p_refined, L). In Isabelle, `sorry` is an oracle that makes the checker accept the current goal as an axiom, so any final proof containing an unreplaced or generated `sorry` satisfies this predicate. Step 3 explicitly uses `sorry` to make sketches pass the checker, and Algorithm 1 does not check that Step 5 eliminates every `sorry` or that the generated proof steps avoid `sorry`. A candidate that is or contains `by sorry` is therefore accepted by the same criterion that defines success; the reported 59.4% and the 90%-sketch-correct ablation can be realized by emitting the placeholder rather than by proving the theorem. The success metric is thus defined, in part, in terms of the placeholder the pipeline is supposed to replace.

full rationale

Aside from the `sorry`-acceptance issue, the paper's derivation chain is not circular. The 59.4% figure is an evaluated benchmark result, not a fitted constant; the whole-proof and tactic-based components are measured against an external dataset, and the ablation comparisons are self-contained. The choice of Qwen-Coder-14B after initial small-model experiments is model selection on a metric, which is a possible selection-bias concern but not circularity: the final number is still produced by running the chosen pipeline, not by renaming the selection criterion as a prediction. The absence of a train/test overlap check between the AFP/Isabelle-HOL training corpora and miniF2F is a data-contamination risk, not a definitional equivalence. Self-citations are used only as related-work context and are not load-bearing. The one substantive circularity is the verifier semantics: because the checker accepts `sorry`, the success predicate is permissive by construction, so the central benchmark claim is not guaranteed to measure theorem proving rather than placeholder generation.

Assumptions & free parameters 6 free parameters · 4 assumptions · 0 invented entities

HybridProver is an empirical ML system, so there are no invented entities and few free parameters in the theory sense. The free parameters are training and sampling choices, most of which were selected on the evaluation metric. The axioms are standard trust assumptions about Isabelle's checker and an unstated benchmark-disjointness assumption that is load-bearing for the SOTA claim.

free parameters (6)
  • sampling_rate_n = 128
    Number of whole-proof candidates and tactic candidates sampled per theorem; set to match prior work, directly trades compute for success rate.
  • sampling_temperature_T = 0.6 to 0.9 (ablation best); final value not stated
    Ablation on Qwen-Coder-7B shows 0.6-0.9 is the best band; the temperature used for the 59.4 percent run with Qwen-Coder-14B is not explicitly reported.
  • learning_rate = 1e-5
    Best among six values tested in Section 4.3; affects fine-tuning quality.
  • epochs = 3
    Best among 1, 3, 6, and 10; chosen to avoid overfitting in Section 4.3.
  • lora_rank = 32
    Used for all main runs; ablation shows rank has trivial impact.
  • base_model_choice = Qwen-Coder-14B
    Selected from 15 or more open models by highest proof success rate; this is a selection on the target metric.
assumptions (4)
  • domain assumption Isabelle's trusted kernel only accepts correct proofs, so passing the checker certifies a valid proof.
    Invoked throughout Section 3 and Appendix A.1; all evaluation results depend on it.
  • domain assumption The AFP and Isabelle/HOL training corpora are disjoint from the miniF2F test set.
    Never stated or checked in Section 4.1; the 59.4 percent result assumes no benchmark contamination via memorization.
  • domain assumption Mechanically replacing tactics with the keyword sorry yields a proof sketch whose subgoals are meaningful and independently provable.
    Section 3.1 Step 3 and Algorithm 1; the refinement pipeline assumes these sketches are a reliable decomposition.
  • domain assumption SubgoalXL's 56.1 percent baseline was obtained under comparable evaluation conditions.
    Table 1 uses the published number without a controlled reimplementation; the claimed 3.3 point improvement depends on comparability.

how reviews work

0 comments
Cite this review

Pith. "Pith review of HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement." pith.science (2026). https://pith.science/paper/SR6U6AJG

@misc{pith2026250515740,
  author       = {Pith},
  title        = {Pith review of: HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SR6U6AJG}},
  note         = {Machine review of arXiv:2505.15740}
}
read the original abstract

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent advancements in large language models (LLMs) offer new opportunities for automated theorem proving. Two promising approaches are generating tactics step by step and generating a whole proof directly with an LLM. However, existing work makes no attempt to combine the two approaches. In this work, we introduce HybridProver, a dual-model proof synthesis framework that combines tactic-based generation and whole-proof synthesis to harness the benefits of both approaches. HybridProver generates whole proof candidates for evaluation directly, then extracts proof sketches from those candidates. It then uses a tactic-based generation model that integrates automated tools to complete the sketches via stepwise refinement. We implement HybridProver for the Isabelle theorem prover and fine-tune LLMs on our optimized Isabelle datasets. Evaluation on the miniF2F dataset illustrates HybridProver's effectiveness. We achieve a 59.4% success rate on miniF2F, where the previous SOTA is 56.1%. Our ablation studies show that this SOTA result is attributable to combining whole-proof and tactic-based generation. Additionally, we show how the dataset quality, training parameters, and sampling diversity affect the final result during automated theorem proving with LLMs. All of our code, datasets, and LLMs are open source.

Figures

Figures reproduced from arXiv: 2505.15740 by the authors.

Figure 1
Figure 1. HybridProver Framework Overview 3.1 Framework overview Our framework is depicted in [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

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

  1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  2. LeanExplore: A search engine for Lean 4 declarations

    cs.SE 2025-06 conditional novelty 6.0 of 10

    LeanExplore combines semantic embeddings, BM25+ lexical matching, and PageRank to retrieve Lean 4 declarations from natural language queries, and reports an LLM-judged win rate over existing tools.

  3. TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

    cs.CL 2026-07 conditional novelty 5.5 of 10

    TreeThink provides a modular, asynchronous tree-search library for neural theorem proving with unified REPL clients for Lean, Rocq, and Isabelle and up to 6.3× wall-clock speedup.

Reference graph

Works this paper leans on

22 extracted references · 12 canonical work pages · cited by 3 Pith papers

  1. [9]

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al

    URLhttps://arxiv.org/abs/2406.00515. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. InProceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–220,

    arXiv

  2. [11]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer,

    2021

  3. [14]

    A Mechanised Proof of G\"odel's Incompleteness Theorems using Nominal Isabelle

    URLhttps://arxiv.org/abs/2104.13792. Benjamin C Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C˘at˘alin Hri¸ tcu, Vilhelm Sjöberg, and Brent Yorgey. Software foundations.Webpage: http://www. cis. upenn. edu/bcpierce/s- f/current/index. html, 16,

    work page Pith review arXiv

  4. [17]

    Code2inv: A deep learning framework for program verification

    Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2inv: A deep learning framework for program verification. InComputer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II 32, pages 151–164. Springer,

    work page 2020

  5. [18]

    Formal api specification of the pikeos separation kernel

    Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan, Burkhart Wolff, and Yakoub Nemouchi. Formal api specification of the pikeos separation kernel. InNASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings 7, pages 375–389. Springer,

    work page 2015

  6. [19]

    Lego-prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In12th International Conference on Learning Representations (ICLR 2024). International Conference on Learning Representations, ICLR, 2024a. Qingxiang Wang, Cezary ...

    work page 2024

  7. [20]

    Theoreml- lama: Transforming general-purpose llms into lean4 experts.arXiv preprint arXiv:2407.03203, 2024b

    Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoreml- lama: Transforming general-purpose llms into lean4 experts.arXiv preprint arXiv:2407.03203, 2024b. Christoph Weidenbach, Bernd Gaede, and Georg Rock. Spass & flotter version 0.42. InAutomated Deduction—Cade-13: 13th International Conference on Automated Deduct...

    arXiv 1996

  8. [21]

    Subgoal-based demonstration learning for formal theorem proving

    Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-based demonstration learning for formal theorem proving. InForty-first International Conference on Machine Learning, 2024a. Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving.arXiv preprint arXiv:2408.11172, 202...

    arXiv

Show all 22 references
  1. [23]

    automate reasoning over large libraries developed with formal proof assistants

    define hammers as methods that “automate reasoning over large libraries developed with formal proof assistants.” Most ITPs have their own hammers, e.g., Coqhammer in Rocq and Sledgehammer in Isabelle. Sledgehammer in Isabelle is the most powerful one Paulson [2012]. Providing ...

    2012

  2. [2002]

    Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers

    Lawrence Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors, PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reaso...

    2010

  3. [2010]

    Generative language modeling for automated theorem proving

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393,

    2009 arXiv

  4. [2011]

    40 years of formal methods

    Dines Bjørner and Klaus Havelund. 40 years of formal methods. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors,FM 2014: Formal Methods, pages 42–61, Cham,

    2014

  5. [2015]

    Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu

    URLhttps://arxiv.org/abs/1501.02155. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. InInternational Conference on Learning Representations,

    arXiv

  6. [2016]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433,

    arXiv

  7. [2017]

    Lyra: Orchestrating dual correction in automated theorem proving

    Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806,

    arXiv

  8. [2018]

    Formal specifications from natural language.arXiv preprint arXiv:2206.01962,

    Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language.arXiv preprint arXiv:2206.01962,

    arXiv

  9. [2020]

    Proof repair infrastructure for supervised models: Building a large proof repair dataset

    Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof repair infrastructure for supervised models: Building a large proof repair dataset. In14th International Conference on Interactive Theorem Proving (ITP 2023), pages 26–1. Schloss Dagstuhl–Leibniz...

    2023

  10. [2021]

    Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan

    URLhttps://arxiv.org/abs/2107.03374. Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. Nl2tl: Transforming natural languages to temporal logics using large language models.arXiv preprint arXiv:2305.07766,

    arXiv

  11. [2022]

    Compcert-a formally verified optimizing compiler

    Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. Compcert-a formally verified optimizing compiler. InERTS 2016: Embedded Real Time Software and Systems, 8th European Congress,

    2016

  12. [2023]

    Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli. cvc4. InComputer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,

    2011

  13. [2024]

    doi: 10.1109/TDSC.2024.3375311

    ISSN 1941-0018. doi: 10.1109/TDSC.2024.3375311. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392,

    1941

  14. [2025]

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun

    URL https: //arxiv.org/abs/2502.09955. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. 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 ...

    arXiv

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.