Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read This case study claims that large language models can produce correct, complete Rocq proof scripts for program-correctness theorems, with success rates that rise sharply when the prompt includes external dependencies and same-file context.

desk verdict A careful, reproducible case study whose main dependency result is partly an oracle artifact—still worth a serious read for anyone working on LLM proof generation. read the letter →

arxiv 2508.18587 v1 pith:6AWHMBXO submitted 2025-08-26 cs.PL cs.AI

Bar{i}ş Bayaz{i}t , Yao Li , Xujie Si This is my paper · ORCID
classification cs.PLcs.AI
keywords proofassistantsRocqProverlargelanguagemodelsprogramverificationgenerationpromptcontextablationhs-to-coqVerdi
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

This paper tries to establish that large language models can generate correct, complete proof scripts for program-correctness theorems in the Rocq proof assistant, and that the right prompt makes them dramatically better at it. Across two mature open-source verification projects—hs-to-coq's theory of Haskell's base library and the Verdi distributed-systems framework—five models were asked to produce proofs under four prompt conditions. The consistent pattern is that including external dependencies, the lines of the source file before the theorem, or both, raised verified success rates, and that removing both lowered them (for GPT-4o on hs-to-coq, from 49.2% to 25.7%). The paper also claims that models succeed often on small proofs and sometimes on large ones, that the two projects behave differently, and that models can find genuinely shorter proofs while occasionally emitting nonsensical repeating-tactic scripts. If this is right, context-aware, single-pass LLM proof generation becomes a practical aid for verification, with the proof assistant's own checker as the safety net.

What carries the argument

The central mechanism is the prompt-ablation design. For each theorem the authors extracted its signature, the full in-file context (every line before it in the source file), and the signatures of external dependencies via SerAPI, then prompted models under four conditions: informed (both context sources), no in-file context, no dependencies, and neither. Success is judged entirely by whether SerAPI's sertop accepts the generated script in Rocq, so the proof assistant's own kernel is the arbiter. A second component is the tactic-count histogram, which groups theorems by the size of the original proof and tracks success and byte-identical reproduction in each interval; a third is the qualitative reading of generated proofs, including the use of case analysis on the inductively defined reflect proposition as a classical proof technique.

What would settle it

Perturb the prompts by renaming all user-defined identifiers, lemmas, and definitions in the in-file context and dependency list without changing the theorem's logical content; if informed-mode success rates collapse under renaming, the context effect would be shown to depend on memorized surface form rather than on the reasoning support the paper claims.

Watch

Extended reading notes

Core claim

The paper's central claim is that LLMs can write whole proofs for real program-correctness theorems, and that the ingredients a human would need—the definitions and lemmas from other files, and everything already defined earlier in the current file—are the same ingredients that make the models succeed. The informed condition, which supplied both, gave every model its best or near-best verified success rate in both projects (e.g., GPT-4o reaching 49.2% on hs-to-coq and o4-mini 29.7% on Verdi), while the condition with neither dropped to 25.7% and 7.8% respectively. Proof size matters: success rates are high for small proofs and decline as tactic counts grow, but models still complete some proofs past twenty tactics. The paper further claims that project differences are real, with Verdi depending more heavily on same-file context, and that quality is mixed: generated proofs can be shorter and more elegant than the originals, such as a four-tactic proof that applies an earlier contrapositive theorem instead of a 24-line induction, but they can also be failed scripts that repeat a single tactic indefinitely. These observations support the conclusion that LLMs are effective enough for further investment, with the proof assistant's checking step serving as a guarantee of correctness.

Load-bearing premise

The evaluation assumes that unless an LLM's output is byte-for-byte identical to the original proof, a successful generation reflects genuine proof-generation ability; if models have partially memorized these open-source proofs, the measured context benefits could be improved retrieval rather than improved reasoning.

Editorial extensions

If this is right

  • Verification tooling should treat prompt construction as a first-class knob: automatically prepending dependency signatures and preceding file lines is a free, effective boost over bare theorem statements.
  • Because a proof assistant only counts a proof as successful when its kernel accepts it, even a model that sometimes hallucinates can be used safely: the generated script is either accepted or discarded, with no risk of admitting a wrong proof.
  • Automation efforts should prioritize small-to-medium proofs, where models already reach high success rates, while treating 20-plus-tactic proofs as an open challenge rather than a closed one.
  • Benchmark results from one verification project should not be assumed to transfer to another; the paper's two projects show different sensitivity to in-file context and dependencies.
  • Human-written proofs are not the only good proofs: models can find shorter, structurally different scripts, which means proof corpora may hide simpler proofs that automation can expose.

Reading between the lines

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

  • If the context effect is causal rather than correlational, the result implies a cheap scaling law: richer project context should push success rates up across models without any fine-tuning, so dependency extraction becomes a high-value component for future proof-generation systems.
  • The byte-for-byte plagiarism check is only a lower bound on memorization; a stronger test would systematically rename identifiers and definitions in the prompt to see whether success survives when retrieval is blocked, which the paper's own large identical Verdi proofs suggest has not yet been settled.
  • The repeating-tactic failures suggest a concrete engineering fix worth testing: generation temperature or a stutter-detection early stop could eliminate the most common failure mode at near-zero cost.
  • The transfer of a Lean-focused theorem-proving model to Rocq hints that formal-proof competence generalizes across proof assistants, so training on one assistant's corpus may produce usable proofs in another, a hypothesis the paper does not test directly.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. This paper reports a case study of five large language models (GPT-4o-mini, GPT-4o, o4-mini, DeepSeek Prover V2, DeepSeek R1-0528) generating whole Rocq proof scripts for theorems from two real projects: the hs-to-coq theory of Haskell's base library (187 theorems) and Verdi (579 theorems). The authors vary the prompt across four conditions: informed (external dependencies plus in-file context), no external dependencies, no in-file context, and neither, with proof success determined by SerAPI checking the generated proof with the original theorem and in-file context. The paper answers four research questions: RQ1 on the effect of dependencies and in-file context; RQ2 on proof-size trends; RQ3 on cross-project differences; and RQ4 on qualitative proof quality, including examples of concise proofs, use of classical techniques, and repeated-tactic failures. The main claims are that external dependencies and in-file context significantly improve proof generation, that small proofs are much easier but large proofs are sometimes produced, that the two projects differ substantially, and that LLMs can produce smart but also odd proofs.

Significance. If the quantitative claims hold, this is a useful data point for the growing literature on LLM-based proof generation: it evaluates whole-proof generation rather than tactic prediction, uses mature open-source verification projects, and checks successes with an external proof checker (SerAPI), which makes the acceptance criterion trustworthy. The artifact availability and the inclusion of open-weight models are also strengths. However, the central comparative claim about dependencies is confounded by the oracle-like extraction of dependencies from the original proofs, and the contamination control via exact-match checking is too coarse to support the current interpretation of the size-based results. As a case study of two projects, the paper's scope is modest, but the methodology is clearly described and the qualitative analysis is informative.

major comments (3)
  1. [Section 4, Tables 1a and 1b] The dependency condition is an oracle condition: Section 4 defines external dependencies as 'any signatures that the original proof relies on' extracted via SerAPI, so the informed mode hands the model the exact premise set used by the original proof. Consequently, the improved success rates in the informed condition do not establish that a realistic dependency-selection mechanism helps; they show that giving the model the original proof's premises helps. This is load-bearing for RQ1 and for the conclusion that 'external dependencies and in-file context can significantly help with proof generation.' For example, GPT-4o on hs-to-coq improves from 25.7% in the 'neither' condition to 49.2% in the informed condition, but the improvement bundles oracle dependency extraction with in-file context. The paper should either compare against a non-oracle dependency-selection baseline (such as TF-IDF/KNN as in PALM or a simple retrieval heuristic) or explicitly reframe the result as an upper-bound measurement rather than a practical prompting recommendation.
  2. [Section 5, RQ2, Figures 4a and 4b] The contamination check only marks proofs that are byte-for-byte identical to the original proofs, and the authors do not exclude these from the reported success rates or quantify their share by model and condition. The paper's own observation that some larger Verdi proofs are identical to originals, 'suggesting that the proof might have been in these models' knowledge set,' is an acknowledged threat that is not controlled. Since both projects are open source and likely present in training corpora, exact-match checking is too weak to rule out partial memorization or near-verbatim retrieval, which would also affect the interpretation of RQ1 and RQ2 as evidence of reasoning ability. Please report success rates after removing identical proofs and, ideally, a sensitivity analysis with a near-duplicate metric such as edit distance.
  3. [Tables 1a, 1b, 3a, and 3b] The paper repeatedly uses 'significantly' (abstract, introduction, RQ1, conclusion) without any uncertainty quantification. Each success rate is a single-sample point estimate (one generation per theorem and condition), and the paper provides no confidence intervals, significance tests, or repeated sampling. For instance, the GPT-4o hs-to-coq difference between informed (49.2%) and no-dependencies (44.4%) is a difference of 9 successes out of 187 theorems, which is within plausible binomial sampling noise. The authors should either add confidence intervals or a statistical test, or replace 'significantly' with a non-statistical description such as 'in our sample.'
minor comments (4)
  1. [Section 4, Model and parameter selection] The parameter description is incomplete: the paper states temperature 0.1 for models that support it and default 1.0 for o4-mini, but it does not specify the temperature settings used for the two DeepSeek models, nor whether the reasoning-effort parameter for o4-mini was the only non-default setting. Please clarify.
  2. [Section 4, External dependencies] The paper notes that dependency extraction may include unrelated signatures due to identifier overloading, but it does not report how often this over-approximation occurs or whether it affects the ablation comparisons. A sentence with counts or a robustness check would help.
  3. [Section 5, RQ4] The claim that the EqExact_pair theorem 'cannot be solved by CoqHammer' is stated without supporting evidence. Please either cite a run configuration, report the command and result, or soften the claim to 'did not find a proof in our experiments.'
  4. [Section 5, RQ2] In Figures 4a and 4b, the dark-color segments represent identical proofs, but the figure caption and text do not state explicitly whether those proofs are a subset of the success counts or are subtracted from them; the surrounding text implies they are a subset, but this should be stated directly to avoid ambiguity.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper is an empirical evaluation with externally checked proof acceptance; the oracle-like dependency extraction is a validity caveat, not a circular step.

full rationale

This paper is an empirical case study rather than a derivation: a proof is counted as successful only when SerAPI's assertop accepts it, an external checker independent of the LLM, and no model parameter is fitted to the benchmark before evaluation. The four prompt conditions are ablations, not calibrated quantities, so the informed-versus-ablated comparisons in Tables 1a and 1b are measurements rather than constructions. The authors' self-citations to the hs-to-coq tool and related papers are dataset and background references, not load-bearing evidence for the paper's central claims about LLM proof-generation effectiveness. The strongest concern is that RQ1's 'dependencies' condition is oracle-like: Section 4 defines external dependencies as 'any signatures that the original proof relies on,' so the informed mode supplies the exact premise set used by the target proof. This means the measured benefit is an upper bound for a realistic premise-selection workflow and may overstate the practical value of adding external dependencies. However, this is an external-validity threat, not circular reasoning: the acceptance outcome is verified independently, the dependency list does not by itself guarantee a successful proof, and the paper does not rename a fitted value as a prediction. No circular step meets the required evidentiary bar.

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

This is an empirical study rather than a derivation, so the ledger contains no fitted math constants or invented entities. It records the evaluation-configuration choices and background assumptions that the measured success rates rest on, especially the reliability of SerAPI-based checking, dependency extraction, and the contamination check.

free parameters (3)
  • temperature = 0.1 for GPT-4o-mini, GPT-4o, DeepSeek Prover V2, DeepSeek R1-0528; default (1.0) for o4-mini
    Chosen by the authors as a fixed sampling setting; it affects absolute success rates and reduces but does not remove run-to-run variance, yet no repeated runs are reported.
  • reasoning effort = medium (default) for o4-mini
    Selected to match the model's default; the reasoning effort level can change proof quality and success rate.
  • maximum output tokens = 16,384
    Cap on generated proof length; could truncate long proofs and affect the large-proof analysis in RQ2.
assumptions (6)
  • domain assumption Rocq's proof checker (via SerAPI's sertop) correctly determines whether a generated proof body proves the theorem.
    The study defines success exclusively as acceptance by SerAPI in the matching Rocq version (Section 4, 'Checking successful proofs').
  • domain assumption The dependency extraction includes enough external signatures and notations for a model to construct a proof; missing a needed dependency would be a failure of extraction rather than the LLM.
    Dependencies are collected from qualified identifiers and can include extra matches; Section 4 states extraction 'may include unnecessary dependencies', while omission risk is not quantified.
  • domain assumption Exact identity between a generated proof and the original proof is a sufficient check for memorization in RQ2.
    Section 5 RQ2 marks identical proofs in dark colors and treats them as potential memorization, but partial memorization or training-data familiarity is not controlled.
  • domain assumption The two selected projects, hs-to-coq base and Verdi, are enough to support the paper's comparative claims about LLM proof effectiveness.
    The authors choose them as mature, accessible, and free of advanced program logics (Section 3), and list the two-project scope as a limitation in the Limitations paragraph.
  • domain assumption Single-pass, one-shot generation without feedback is a meaningful measure of LLM effectiveness for the research questions.
    Acknowledged in Limitations: 'our experimental setup focused exclusively on single-pass proof generation, without incorporating a feedback loop.'
  • domain assumption One generation per theorem and setting is sufficient to estimate success rates.
    No repeated runs are reported; the paper treats the point estimates in Tables 1 and 3 as stable enough for its claims.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants." pith.science (2026). https://pith.science/paper/6AWHMBXO

@misc{pith2026250818587,
  author       = {Pith},
  title        = {Pith review of: A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6AWHMBXO}},
  note         = {Machine review of arXiv:2508.18587}
}
read the original abstract

Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi. We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis. Our study finds that: (1) external dependencies and context in the same source file can significantly help proof generation; (2) LLMs perform great on small proofs but can also generate large proofs; (3) LLMs perform differently on different verification projects; and (4) LLMs can generate concise and smart proofs, apply classical techniques to new definitions, but can also make odd mistakes.

Figures

Figures reproduced from arXiv: 2508.18587 by the authors.

Figure 1
Figure 1. The process of proving a theorem in Rocq Prover. where N is the set of all natural numbers. We can then write a proof script that instructs the proof as￾sistant to prove this theorem, as shown in lines 2–7. However, in Rocq Prover, we typically do not directly write the entire proof script. Instead, we enter an interactive proof mode. This step is typically marked by the Proof keyword (line 2). When we enter the pro… view at source ↗
Figure 3
Figure 3. Laws for the Eq typeclass stated in Rocq Prover in hs-to-coq [10, 81]. Other theories, such as theories for containers, graph, or the GHC compiler, contain much more complicated proofs. For example, the theorem insertBM_Desc is about the prop￾erty of the insertBM function of container’s IntSet data structure.4 The handcrafted proof of this theorem is 42 lines of proof script, makes heavy use of proven lemmas, uses c… view at source ↗
Figure 2
Figure 2. The take function defined in Haskell’s base library and its translation in Rocq Prover produced by hs-to-coq. Haskell and Rocq Prover [37, 79, 88]. A few examples of type￾classes implemented in the base library include: Eq for equal￾ity tests, Ord for total orders, Semigroup for concatenation, Foldable for “congregating” a data structure, and abstract in￾terfaces like Functor, Applicative [56], and Monad [58, 87], e… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Success rates (light) vs. identically generated proofs (dark) by tactic count intervals for hs-to-coq and Verdi. rates for certain models. Conversely, simpler proofs with fewer tactics appeared to benefit from the in-file context. In contrast, for Verdi, adding in-file…
Figure 5
Figure 5. Figure 5: A comparison between the original proof and a proof generated by LLMs for theorem instance_MonoidLaws_unit in hs-to-coq. net, when they are both in a multi-step transition relation [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: A Rocq theorem found in Verdi (in the file core/DynamicNetLemmas.v) and a proof generated by OpenAI o4-mini. We omit the original proof found in Verdi because the proof script is 29 tactics long. defined by step_ordered_dynamic_failure_star—the exact definition of this…
Figure 8
Figure 8. Figure 8: A comparison between the original proof and a failed proof generated by LLMs for theorem simpl_list_cons_eq in hs-to-coq. straightforward. However, GPT-4o-mini generates a failed proof in the informed mode shown in Fig. 8b. The proof fails at the first unfold. However,…

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability

    cs.CL 2026-08 reject novelty 7.0 of 10

    The paper introduces TCS-Bench, a 300-task proof-generation benchmark from top TCS papers, and reports frontier LLM accuracies from 30% to 68% using an automated verifier.

Reference graph

Works this paper leans on

111 extracted references · 26 canonical work pages · cited by 1 Pith paper

  1. [1]

    Agda Developers. 2025. Agda. https://agda.readthedocs.io/

    2025

  2. [2]

    AlphaProof. 2024. AI achieves silver-medal standard solv- ing International Mathematical Olympiad problems Published. https://deepmind.google/discover/blog/ai-solves-imo-problems-at- silver-medal-level/

    2024

  3. [3]

    Andrew W. Appel. 2014. Program Logics - for Certified Compilers . Cambridge University Press. http://www.cambridge.org/de/ academic/subjects/computer-science/programming-languages- and-applied-logic/program-logics-certified-compilers?format=HB

    2014

  4. [4]

    Andrew W. Appel. 2022. Coq’s vibrant ecosystem for verification en- gineering (invited talk). In CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 , Andrei Popescu and Steve Zdancewic (Eds.). ACM, 2–11. https://doi.org/10.1145/3497775.3503951

    work page arXiv 2022

  5. [5]

    Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. 2011. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 7086) , J...

    doi:10.1007/978-3-642-25379-9_12 2011

  6. [6]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Ed- ward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathe- matics. CoRR abs/2302.12433 (2023). https://doi.org/10.48550/ARXIV. 2302.12433 arXiv:2302.12433

    arXiv doi:10.48550/arxiv.2302.12433 2023

  7. [7]

    A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

    Barış Bayazıt, Xujie Si, and Yao Li. 2025. Replication Package for "A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants". https://doi.org/10.5281/zenodo.16939067

    work page doi:10.5281/zenodo.16939067 2025

  8. [8]

    Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. 2020. The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. In Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12236), Christoph Benzmüller and Bruce R. Miller (Eds.)...

    doi:10.1007/978-3-030- 2020

Show all 111 references
  1. [9]

    Boulton, Andrew D

    Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, and John Van Tassel. 1992. Experience with Embedding Hardware Description Languages in HOL. In Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 In- ternational Confe...

    1992

  2. [10]

    Cohen, and Stephanie Weirich

    Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, and Stephanie Weirich. 2021. Ready, Set, Verify! Applying hs-to-coqm to real-world Haskell code. J. Funct. Program. 31 (2021), e5. https://doi.org/10.1017/ S0956796820000283

    2021

  3. [11]

    Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR 2004 - Concurrency Theory, 15th International Con- ference, London, UK, August 31 - September 3, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 3170) , Philippa Gardner and Nobuko Yosh...

    2004 doi

  4. [12]

    CertiCoq Developers. 2024. CertiCoq. https://github.com/CertiCoq/ certicoq. Version v0.9+8.19, released 2024-05-28

    2024

  5. [13]

    Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. 2023. Omnisemantics: Smooth Handling of Nondeter- minism. ACM Trans. Program. Lang. Syst. 45, 1 (2023), 5:1–5:43. https://doi.org/10.1145/3579834

    2023 doi

  6. [14]

    Frans Kaashoek, and Nickolai Zeldovich

    Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, Octo- ber ...

    2015

  7. [15]

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Hee- woo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training Verifiers to Solve Math Word Problems.CoRR abs/2110.14168 (2021). arXiv...

    2021 arXiv

  8. [16]

    Lukasz Czajka, Burak Ekici, and Cezary Kaliszyk. 2018. Concrete Semantics with Coq and CoqHammer. In Intelligent Computer Mathe- matics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 1100...

    2018 doi

  9. [17]

    Lukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automa- tion for Dependent Type Theory. J. Autom. Reason. 61, 1-4 (2018), 423–453. https://doi.org/10.1007/S10817-018-9458-4

    2018 doi

  10. [18]

    Leonardo de Moura and Sebastian Ullrich. 2021. 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 (Lecture Notes in Computer Science, Vol. 126...

    2021 doi

  11. [19]

    Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods - 9th International Con- ference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Pro- ceedings (Lecture Notes in Computer Science, Vol. 7041) , Gilles Barthe, Al...

    2011 doi

  12. [20]

    DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhi- hong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei...

    2025 arXiv

  13. [21]

    Veneris, Fan Long, and Xujie Si

    Xun Deng, Sicheng Zhong, Andreas G. Veneris, Fan Long, and Xujie Si

  14. [22]

    Quinn Dougherty and Ronak Mehta. 2025. Proving the Coding In- terview: A Benchmark for Formally Verified Code Generation. In IEEE/ACM International Workshop on Large Language Models for Code, LLM4Code@ICSE 2025, Ottawa, ON, Canada, May 3, 2025 . IEEE, 72–79. https://doi.org/10...

    2025

  15. [23]

    Sahibsingh A. Dudani. 1976. The Distance-Weighted k-Nearest- Neighbor Rule. IEEE Trans. Syst. Man Cybern. 6, 4 (1976), 325–327. https://doi.org/10.1109/TSMC.1976.5408784

    1976

  16. [24]

    Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2020. Simple High-Level Code For Cryptographic Arith- metic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54, 1 (2020), 23–30. https://doi.org/10.1145/3421473.3421477

    2020

  17. [25]

    Emily First and Yuriy Brun. 2022. Diversity-Driven Automated For- mal Verification. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022 . ACM, 1–13. https://doi.org/10.1145/3510003.3510138

    2022

  18. [26]

    Emily First, Yuriy Brun, and Arjun Guha. 2020. TacTok: semantics- aware proof synthesis. Proc. ACM Program. Lang. 4, OOPSLA (2020), 231:1–231:31. https://doi.org/10.1145/3428299

    2020 doi

  19. [27]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software En- gineering Conference and Symposium on the Foundations of Software Engineering, ESEC...

    2023

  20. [28]

    Emilio Jesús Gallego Arias. 2016. SerAPI: Machine-Friendly, Data- Centric Serialization for Coq . Technical Report. MINES ParisTech. https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408

    2016

  21. [29]

    GHC Developers. 2025. Haskell base library: GHC/List.lhs, lines 363–365 (commit 52c0b09036c36f1ed928663abb2f295fd36a88bb). https://github.com/ghc/packages-base/blob/ 52c0b09036c36f1ed928663abb2f295fd36a88bb/GHC/List.lhs#L363- L365. Accessed: 2025-08-25

    2025

  22. [30]

    Goguen and Luqi

    Joseph A. Goguen and Luqi. 1995. Formal Methods and Social Con- text in Software Development. In TAPSOFT’95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/- FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings (Lecture Notes in Computer Sc...

    1995

  23. [31]

    Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Mostly Automated Proof Repair for Verified Libraries. Proc. ACM Program. Lang. 7, PLDI (2023), 25–49. https://doi.org/10.1145/3591221

    2023 doi

  24. [32]

    Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming...

    2015

  25. [33]

    Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jie- ung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 201...

    2016

  26. [34]

    Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Imp...

    2018

  27. [35]

    Jilin Hu, Jianyu Zhang, Yongwang Zhao, and Talia Ringer. 2025. Hy- bridProver: Augmenting Theorem Proving with LLM-Driven Proof A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants LMPL ’25, October 12–18, 2025, Singapore, Singapore Synthesis and Ref...

    2025 doi arXiv

  28. [36]

    Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, and Ting Liu. 2025. A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions. ACM Trans. Inf. S...

    2025 doi

  29. [37]

    Guzmán, Kevin Hammond, John Hughes, Thomas Johnsson, Dick Kieburtz, Rishiyur Nikhil, Will Par- tain, and John Peterson

    Paul Hudak, Simon Peyton Jones, Philip Wadler, Brian Boutel, Jon Fairbairn, Joseph Fasel, María M. Guzmán, Kevin Hammond, John Hughes, Thomas Johnsson, Dick Kieburtz, Rishiyur Nikhil, Will Par- tain, and John Peterson. 1992. Report on the programming language Haskell: a non-st...

    1992

  30. [38]

    Alemi, Niklas Eén, François Chollet, and Josef Urban

    Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Pro- cessing Sys...

    2016

  31. [39]

    Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu

  32. [40]

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. InThe Eleventh International Conference on Learning...

    2023

  33. [41]

    Juyong Jiang, Fan Wang, Jiasi Shen, Sungju Kim, and Sunghun Kim

  34. [42]

    Karen Spärck Jones. 2004. A statistical interpretation of term speci- ficity and its application in retrieval. J. Documentation 60, 5 (2004), 493–502. https://doi.org/10.1108/00220410410560573

    2004 doi

  35. [43]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. https://doi.org/10.1017/S0956796818000151

    2018 doi

  36. [44]

    Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. 2024. Cobblestone: Iterative Automation for Formal Verification. CoRR abs/2410.19940 (2024). https://doi.org/10. 48550/ARXIV.2410.19940 arXiv:2410.19940

    2024 doi arXiv

  37. [45]

    Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel.. In Proceedings of ...

    2009

  38. [46]

    Pierce, and Steve Zdancewic

    Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic

  39. [47]

    Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev

  40. [48]

    Xavier Leroy. 2009. Formal verification of a realistic compiler. Com- mun. ACM 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788. 1538814

    2009 doi

  41. [49]

    Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, and Xiaoxing Ma. 2025. Proving Olympiad Inequal- ities by Synergizing LLMs and Symbolic Reasoning. InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Sin- gapore...

    2025

  42. [50]

    Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. 2024. Autoformalize Mathemat- ical Statements by Symbolic Equivalence and Semantic Con- sistency. In Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information...

    2024

  43. [51]

    Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jian- qiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. 2024. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. In Advances in Neural Information Processing Systems 38: A...

    2024

  44. [52]

    CoqPilot, a plugin for LLM-based generation of proofs. In Pro- ceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, Vladimir Filkov, Baishakhi Ray, and Minghui Zhou (Eds.). ACM, ...

    2024

  45. [53]

    Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2025. DafnyBench: A Benchmark for Formal Software Verification. Trans. Mach. Learn. Res. 2025 (2025). https://openreview.net/...

    2025

  46. [54]

    Minghai Lu, Benjamin Delaware, and Tianyi Zhang. 2024. Proof Automation with Large Language Models. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineer- ing, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024 , Vladimir Filkov,...

    2024

  47. [55]

    Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. Zenodo. https://doi.org/10.5281/zenodo.7118596

    2022 doi

  48. [56]

    Conor McBride and Ross Paterson. 2008. Applicative programming with effects. J. Funct. Program. 18, 1 (2008), 1–13. https://doi.org/10. 1017/S0956796807006326

    2008

  49. [57]

    Evan Lohn and Sean Welleck. 2024. miniCodeProps: a Minimal Benchmark for Proving Code Properties. CoRR abs/2406.11915 (2024). https://doi.org/10.48550/ARXIV.2406.11915 arXiv:2406.11915

    2024 doi arXiv

  50. [58]

    Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput. 93, 1 (1991), 55–92. https://doi.org/10.1016/0890-5401(91) 90052-4

    1991 doi

  51. [59]

    Morrison

    Donald R. Morrison. 1968. PATRICIA - Practical Algorithm To Re- trieve Information Coded in Alphanumeric. J. ACM 15, 4 (1968), 514–534. https://doi.org/10.1145/321479.321481

    1968

  52. [60]

    Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anand- kumar, and Xujie Si. 2024. Autoformalizing Euclidean Geometry. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024 . OpenReview.net. https: LMPL ’25, October 1...

    2024

  53. [61]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science, Vol. 2283. Springer. https://doi.org/10.1007/3- 540-45949-9

    2002 doi

  54. [62]

    Peter W. O’Hearn. 2007. Separation logic and concurrent resource management. In Proceedings of the 6th International Symposium on Memory Management, ISMM 2007, Montreal, Quebec, Canada, October 21-22, 2007, Greg Morrisett and Mooly Sagiv (Eds.). ACM, 1. https: //doi.org/10.114...

    2007

  55. [63]

    Microsoft Azure AI Foundry Documentation. 2025. Azure Ope- nAI Reasoning Models. https://learn.microsoft.com/en-us/azure/ai- foundry/openai/how-to/reasoning. Accessed: 2025-07-02

    2025

  56. [64]

    Chris Okasaki and Andy Gill. 1998. Fast mergeable integer maps. In ACM SIGPLAN Workshop on ML. 77–86

    1998

  57. [65]

    OpenAI. 2024. GPT-4o. https://platform.openai.com/docs/models/gpt- 4o. Accessed: 2025-07-08

    2024

  58. [66]

    OpenAI. 2024. GPT-4o Mini. https://platform.openai.com/docs/models/gpt-4o-mini. Accessed: 2025-07-08

    2024

  59. [67]

    OpenAI. 2025. o4-mini. https://platform.openai.com/docs/models/o4- mini. Accessed: 2025-07-08

    2025

  60. [68]

    OpenAI. 2025. tiktoken. https://github.com/openai/tiktoken. Ac- cessed: 2025-07-08

    2025

  61. [69]

    Peter W. O’Hearn. 2020. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL (2020), 10:1–10:32. https://doi.org/10.1145/3371078

    2020 doi

  62. [70]

    Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. 2025. Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark. In Proceedings of the 2025 Workshop on Hot Topics in Operating Systems, HotOS 2025, Banff, AB, Canada, Ma...

    2025

  63. [71]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. DeepSeek-Prover- V2: Advancing Formal Mathemati...

    2025 arXiv

  64. [72]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings . IEEE Computer Society, 55–74. https://doi.org/10.1109/LICS.2002.1029817

    2002 arXiv

  65. [73]

    Talia Ringer. 2021. Proof Repair. Ph. D. Dissertation. University of Washington, USA. https://hdl.handle.net/1773/47429

    2021

  66. [74]

    Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019. QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. 5, 2-3 (2019), 102–281. https://doi.org/10.1561/2500000045

    2019 doi

  67. [75]

    Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey

    Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. 2025. Logical Foundations. Electronic textbook. Version 6.7.1 https://softwarefoundations.cis.upenn.edu/lf-6.7.1/

    2025

  68. [76]

    Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. 2023. Passport: Improving Automated Formal Verification Using Identifiers. ACM Trans. Program. Lang. Syst. 45, 2 (2023), 12:1–12:30. https://doi.org/10.1145/3593374

    2023 doi

  69. [77]

    Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Shizhuo Dylan Zhang, Talia Ringer, and Yuriy Brun. 2025. QEDCar- tographer: Automating Formal Verification Using Reward-Free Rein- forcement Learning. In 47th IEEE/ACM International Conference on Software Engineering, ICSE...

    2025

  70. [78]

    Lucas Silver and Steve Zdancewic. 2021. Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang. 5, POPL (2021), 1–28. https://doi.org/10.1145/3434307

    2021 doi

  71. [79]

    Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics , Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278–293

    2008

  72. [80]

    Antal Spector-Zabusky, Joachim Breitner, Yao Li, and Stephanie Weirich. 2019. Embracing a mechanized formalization gap. CoRR abs/1910.11724 (2019). arXiv:1910.11724 http://arxiv.org/abs/1910. 11724

    2019 arXiv

  73. [81]

    Saul, and Sorin Lerner

    Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 2020, London, UK, June 15, 20...

    2020

  74. [82]

    Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2022. Later credits: re- sourceful reasoning for the later modality. Proc. ACM Program. Lang. 6, ICFP (2022), 283–311. https://doi.org/10.1145/3547631

    2022 doi

  75. [83]

    Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2013. Secure distributed programming with value-dependent types. J. Funct. Program. 23, 4 (2013), 402–451. https://doi.org/10.1017/S0956796813000142

    2013 doi

  76. [84]

    The Rocq Development Team. 2025. The Rocq Prover. https://doi.org/ 10.5281/zenodo.15149629

    2025 doi

  77. [85]

    Ferreira, Sorin Lerner, and Emily First

    Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, and Emily First. 2025. Rango: Adaptive Retrieval-Augmented Proving for Auto- mated Software Verification. In 47th IEEE/ACM International Confer- ence on S...

    2025

  78. [86]

    Trinh, Yuhuai Wu, Quoc V

    Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. 2024. Solving olympiad geometry without human demonstrations.Nat. 625, 7995 (2024), 476–482. https://doi.org/10.1038/S41586-023-06747-5

    2024 doi

  79. [87]

    Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. 2018. Total Haskell is reasonable Coq. In Pro- ceedings of the 7th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, Janu- ary 8-9, 2018,...

    2018 doi

  80. [88]

    Philip Wadler and Stephen Blott. 1989. How to make ad-hoc polymor- phism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Austin, Texas, USA) (POPL ’89). Association for Computing Machinery, New York, NY, USA, 60–76. ...

    1989

  81. [89]

    Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D

    James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. SIGPLAN Not. 50, 6 (June 2015), 357–368. https://doi.org/ 10.1145/2813885.2737958

    2015

  82. [90]

    Wilcox, Steve Anton, Zachary Tatlock, Michael D

    Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. 2016. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Pro- grams and Proofs, Saint Pet...

    2016

  83. [91]

    Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Aut- oformalization with Large Language Models. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Sy...

    2022

  84. [92]

    Pierce, and Steve Zdancewic

    Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq.Proc. ACM Program. Lang. 4, POPL (2020), 51:1–51:32. https://doi.org/10.1145/ 3371119

    2020

  85. [93]

    Philip Wadler. 1992. Comprehending Monads. Math. Struct. Comput. Sci. 2, 4 (1992), 461–493. https://doi.org/10.1017/S0960129500001560

    1992 doi

  86. [94]

    Xinference. 2025. deepseek-r1. https://inference.readthedocs.io/en/ latest/models/builtin/llm/deepseek-r1.html Accessed: 2025-07-08

    2025

  87. [95]

    Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Inter- acting with Proof Assistants. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97...

    2019

  88. [96]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval- Augmented Language Models. In Advances in Neural Information Processing Systems 36: Annual Co...

    2023

  89. [97]

    Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. 2025. VERINA: Benchmarking Verifiable Code Generation. CoRR abs/2505.23135 (2025). https://doi.org/10.48550/ ARXIV.2505.23135 arXiv:2505.23135

    2025 doi

  90. [98]

    Irene Yoon, Yannick Zakowski, and Steve Zdancewic. 2022. Formal reasoning about layered monadic interpreters. Proc. ACM Program. Lang. 6, ICFP (2022), 254–282. https://doi.org/10.1145/3547630

    2022 doi

  91. [99]

    Xinference. 2025. deepseek-prover-v2. https://inference.readthedocs. io/en/latest/models/builtin/llm/deepseek-prover-v2.html Accessed: 2025-07-08

    2025

  92. [100]

    Pierce, and Steve Zdancewic

    Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li- yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2021. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem...

    2021

  93. [101]

    Lichen Zhang, Shuai Lu, and Nan Duan. 2024. Selene: Pioneer- ing Automated Proof in Software Verification. In Proceedings of the 62nd Annual Meeting of the Association for Computational Lin- guistics (Volume 1: Long Papers), ACL 2024, Bangkok, Thailand, Au- gust 11-16, 2024 , ...

    2024 doi

  94. [102]

    Shizhuo Dylan Zhang, Talia Ringer, and Emily First. 2023. Getting More out of Large Language Models for Proofs. CoRR abs/2305.04369 (2023). https://doi.org/10.48550/ARXIV.2305.04369 arXiv:2305.04369

    2023 doi arXiv

  95. [103]

    Haiyan Zhao, Hanjie Chen, Fan Yang, Ninghao Liu, Huiqi Deng, Hengyi Cai, Shuaiqiang Wang, Dawei Yin, and Mengnan Du. 2024. Explainability for Large Language Models: A Survey. ACM Trans. Intell. Syst. Technol. 15, 2 (2024), 20:1–20:38. https://doi.org/10.1145/ 3639372

    2024

  96. [104]

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022 . OpenReview.net. https: //openrev...

    2022

  97. [105]

    Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, and executable formal semantics for LLVM IR. Proc. ACM Program. Lang. 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473572

    2021 doi

  98. [111]

    Zihan Zhou, Minfeng Zhu, and Wei Chen. 2025. A human-centric per- spective on interpretability in large language models. Vis. Informatics 9, 1 (2025), 1. https://doi.org/10.1016/J.VISINF.2025.03.001 Received 2025-07-07; accepted 2025-08-08

    2025 doi

  99. [1520]

    https://doi.org/10.1145/3691620.3695521

  100. [2019]

    In Proceedings of the 8th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, Assia Mahboubi and Magnus O

    From C to interaction trees: specifying, verifying, and testing a networked server. In Proceedings of the 8th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, Assia Mahboubi and Magnus O. Myreen (Eds.). ...

    2019

  101. [2021]

    In 6th Conference on Artificial Intelligence and Theorem Proving

    LISA: Language models of ISAbelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving . 378–392

  102. [2024]

    https://doi.org/10.48550/ARXIV.2406.00515 arXiv:2406.00515

    A Survey on Large Language Models for Code Generation.CoRR abs/2406.00515 (2024). https://doi.org/10.48550/ARXIV.2406.00515 arXiv:2406.00515

    2024 doi arXiv

  103. [2025]

    CoRR abs/2505.19271 (2025)

    VerifyThisBench: Generating Code, Specifications, and Proofs All at Once. CoRR abs/2505.19271 (2025). https://doi.org/10.48550/ ARXIV.2505.19271 arXiv:2505.19271

    2025 doi

Pith tools

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