Proving the Coding Interview: A Benchmark for Formally Verified Code Generation

Quinn Dougherty; Ronak Mehta

REVIEW 4 major objections 5 minor 15 references

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation

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

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

Pith's one-line read The paper claims FVAPPS is the largest formal verification benchmark, with 4,715 Lean 4 samples and 1,083 quality-controlled ones, and that frontier LLMs prove only a minority of the sampled theorems.

desk verdict A large new benchmark that is honestly presented but not yet validated; send to review with major revisions. read the letter →

arxiv 2502.05714 v1 pith:SMMZFC5Z submitted 2025-02-08 cs.SE cs.AIcs.LGcs.LO

Quinn Dougherty , Ronak Mehta This is my paper · ORCID

classification cs.SEcs.AIcs.LGcs.LO

keywords formalverificationbenchmarkLean4programsynthesisLLMcodegenerationtheoremprovingproperty-basedtestingAPPSdataset

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 introduces FVAPPS, a benchmark that converts 4,715 coding-interview problems from the APPS dataset into Lean 4 files, each containing a solution function signature plus correctness theorems left as unproved 'sorry' obligations. The authors claim this is the largest formal verification benchmark to date, with 1,083 samples passing a stricter quality-controlled filter. On 100 randomly selected samples, two frontier models prove only a minority of the 406 theorem obligations: 30% for Sonnet and 18% for Gemini. A human baseline on one sample spent ten hours and completed the function but none of the proofs, which the paper offers as evidence that the task is genuinely hard. The benchmark's purpose is to give the field a concrete, shared measure of progress toward language models that can write code and prove it correct.

What carries the argument

The load-bearing machinery is a five-stage, LLM-in-the-loop pipeline that starts from APPS problems and their Python solutions. Stage two uses procedurally generated property-based tests to create unit tests; stage three asks a language model to convert those tests into Lean 4 theorem statements that typecheck with 'sorry'; stage four adds inline unit tests and translated Lean definitions; stage five filters theorems through a property-based testing framework in Lean. The result is a 'def plus multiple theorems' file structure whose sorry obligations define the task, with three quality tiers (unguarded, guarded, guarded and plausible) that let users trade size against statement reliability.

What would settle it

Independently hand-formalize a random sample of FVAPPS problems and compare the benchmark's theorems against the original APPS unit tests and natural-language descriptions; if a substantial fraction of the theorems are vacuously true, unsatisfiable, or assert properties the problem does not require, the 4,715-sample count and the baseline percentages would overstate measured verified coding ability.

Watch

Extended reading notes

Core claim

The central claim is that APPS-style unit tests and natural-language specifications can be systematically lifted into Lean 4 theorem statements, producing a benchmark where success means both implementing a function and proving its correctness properties. The paper claims that FVAPPS is the largest formal verification benchmark, with 4,715 samples, 2,089 samples passing inline unit-test guards, and 1,083 samples passing an additional property-based check. Its baseline experiments report that Sonnet completes 121 of 406 sampled theorem obligations (30%) and Gemini completes 74 (18%), while a human baseline on sample 23 needed ten hours just to implement the function. The authors present these numbers as a challenge: the field should aim to solve each general-purpose programming problem and its associated correctness specifications together.

Load-bearing premise

The benchmark's value rests on the assumption that the Lean theorem statements generated from APPS problems are true, non-vacuous formalizations of each problem's intended correctness properties, which the paper itself flags as a residual risk.

Editorial extensions

If this is right

If FVAPPS is a valid measure, frontier LLMs are currently far from verified code generation: on the sampled problems they prove fewer than a third of the proof obligations.
The benchmark gives the community a fixed, public target, so improvements from fine-tuning, scaffolding loops, and proof search can be tracked sample-by-sample rather than anecdotally.
The guarded-and-plausible subset isolates solvable, property-checked problems, giving training and evaluation a cleaner signal than the full unguarded set.
Because APPS draws on coding interview problems, the benchmark ties formal verification research to the same tasks used to assess human software engineering skill.

Reading between the lines

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

A natural separation test would be to have a different model family generate the theorem statements and then evaluate all models on them; since the same model family that wrote the statements was also one of the baselines, generator-evaluator overlap could bias the reported percentages.
The paper's own vacuity caveat suggests a concrete audit: independently hand-formalize a random sample of the problems and compare the benchmark theorems; if many are trivially true or unsatisfiable, the headline numbers would overstate difficulty.
One could test whether proof performance is measuring proving ability or statement quality by replacing the LLM-generated theorems with human-written ones for the same problems and re-running the baselines.
A complementary check would combine proof completion with execution: for every proved theorem, run the extracted function against the original APPS unit tests to catch proofs of subtly wrong implementations.

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.

Desk Editor's Note

read the letter

Quick take: FVAPPS is a genuinely new resource—the largest attempt I've seen to turn APPS-style coding problems into Lean 4 verification tasks—but the central claims about size and model performance are still conditional on validation the authors haven't done yet.

What's good: The pipeline is explicit, the dataset and code are public, and the authors are refreshingly candid about the risk that their auto-generated theorem statements are vacuous or off-target. The Section V admission is not buried; it's in the discussion. The human baseline (10 hours for one definition, no proofs) gives a sense of difficulty. These things help the reader calibrate.

The soft spots are real and, in my view, load-bearing for the headline numbers. First, the 4715 count mixes files, defs, and theorems in ways that aren't fully reconciled; the 'largest' claim needs a precise counting methodology. Second, the curated 'Guarded and Plausible' subset is filtered by Plausible, a random testing tool, not by proof. That can pass false statements and skip vacuous ones. The authors note this, but they don't quantify the risk—no random sample of statements has been checked by independent proof. Third, the baseline evaluation is thin: 101 samples, no variance, inconsistent sample counts between abstract and tables, and Figure 6 explicitly labels some successes as 'completely spurious' or 'bugs.' So the 30%/18% figures are not yet reliable measures of verified coding ability.

The circularity concern—using Claude Sonnet both to generate the benchmark and to evaluate it—is worth noting, but it's not fatal. The benchmark is grounded in external APPS problems, and the issue is more about generalizability than about contamination. Still, the Guarded and Plausible subsets are defined by Sonnet's ability to produce working definitions, so they may be easier for Sonnet-class models by construction.

Bottom line: this is a useful contribution that deserves peer review. The authors have done the hard work of building a large dataset and being honest about its limitations. What's missing is a validation study—prove a random sample of the curated theorems, report per-sample counting, and give confidence intervals on the baselines. I'd send it to review with the expectation of major revisions, not desk reject it. I wouldn't cite the numbers yet, but I'd keep an eye on the dataset and would probably use it once validated.

Referee Report

4 major / 5 minor

Summary. The paper introduces FVAPPS, a benchmark that extends the APPS coding-challenge dataset into Lean 4 by converting each problem's Python solution and unit tests into a function signature and theorem statements left unproved with "sorry." The generation pipeline uses Claude Sonnet 3.5 in five stages: preprocessing APPS, property-test generation, Lean typechecking, guarded unit-test filtering, and Plausible property-based filtering. The released dataset contains 4,715 samples, 2,089 guarded samples, and 1,083 guarded-and-plausible samples. Baseline evaluations on 100 randomly sampled problems report that Claude Sonnet proves 121 of 406 theorem attempts (30%) and Gemini proves 74 (18.5%), with a ten-hour human baseline completing only a definition on one sample. The authors claim FVAPPS is the largest formal verification benchmark and challenge the community to solve both the programming and the correctness-specification tasks.

Significance. If the theorem statements in FVAPPS are faithful, true, and non-vacuous, the benchmark would be a valuable community resource: it is open-source, builds on a widely used coding benchmark, and directly targets the joint problem of program synthesis and formal verification. The paper is commendably transparent about its limitations and provides substantial engineering detail, including pinned Lean/Mathlib versions, scaffolding loops, and a human baseline. The pipeline's machine-checked typechecking ensures that statements are syntactically well-formed, and the Plausible filter is a reasonable first-line sanity check. However, the central claims—the size of the quality-controlled set and the 30%/18% baseline success rates—depend on theorem statements being true and meaningful, and that validity is not established. The paper's own examples and qualitative tables show that many completed theorems are vacuous, trivial, or spurious, so the headline numbers cannot currently be read as measures of verified coding ability.

major comments (4)

[Section V; Section II-B, Stage 5; Figure 2] The authors concede in Section V that "particular theorems are not applicable or vacuous in some form," and the Stage 5 filter uses Plausible, a finite random-sampling property tester, not a proof checker. False statements can therefore pass, and vacuous statements are not systematically excluded. This is not hypothetical: Figure 2 contains solve_elections_nonnegative, which is trivially true because the function returns Nat, and Figure 6 has an entire bucket called "Non-negativity of Nat." Since the headline success rates count all completed theorems, including these, the benchmark's validity is not yet established. Please provide a quantified manual review or a formal statement-validity check, and report success rates with vacuous and spurious theorems excluded.
[Section III-D; Figure 6; Table III] The baseline results count 121/406 and 74/406 as "correctly proves," but Figure 6 explicitly labels a red box of "completely spurious results, either bugs or a substitution of a quantified variable with a single value," and Table III lists many theorems under "Too trivial" and "Bug." The acceptance criterion for a successful proof is therefore not objective: a generated file that typechecks and resolves all sorrys is counted even when the proof is not a genuine proof of the intended property. The paper should define a stricter criterion (e.g., no sorry, compilation success, and an independent judgment that the theorem is non-vacuous and faithful to the APPS problem) and recompute the 30% and 18.5% figures under that criterion.
[Section II-B; Section III-A] The benchmark generation pipeline and the Sonnet baseline both use claude-3-5-sonnet-20241022, and the Guarded and Guarded-and-Plausible subsets are defined by whether that same model class can produce working definitions. This creates a circularity: the "quality controlled" subsamples are selected for tractability by the evaluated model, so the baseline comparison is in part a measure of a model performing on tasks generated by itself. The resource remains useful, but the independence of the evaluation should be demonstrated by using a different generator for at least a subset, or by reporting a contamination/independence analysis and qualifying the claims accordingly.
[Abstract; Section IV-A] The "largest formal verification benchmark" claim is based on 4,715 samples, but this total includes unguarded files whose theorem statements are not proof-checked and may be vacuous, while the quality-controlled set is 1,083. Comparable benchmarks such as DafnyBench and Clover count different units (programs, proof tasks, or benchmark instances), so it is unclear whether the comparison is apples-to-apples. Please state the unit of comparison explicitly (files vs. theorems vs. problem instances) and, if the claim is meant for the curated subset, provide a direct comparison on the same unit.

minor comments (5)

[Section V] The word "nontheless" appears twice in the discussion; it should be "nonetheless."
[Section II-B] "withing" and "falling withing the scope" should be "within" and "falling within the scope."
[Table I caption] "FILTERED TO THOSE THAT MADE IT PASSED STAGE 3" should read "made it past Stage 3."
[Appendix, Figure 10] The code sample contains stray spaces in variable names such as "v 1.fst" and "v 2.fst"; these should be "v1.fst" and "v2.fst."
[Figure 6 and Table III] The qualitative categories in Figure 6 are not accompanied by a rubric or raw classification counts; a codebook would allow readers to reproduce the "spurious" and "too trivial" labels.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the benchmark is grounded in external APPS data, the baseline results are genuine executable-checked measurements, and the acknowledged vacuity risk is a validity concern rather than a circular derivation.

full rationale

The paper's central claims rest on a new dataset derived from the external APPS benchmark and on baseline measurements obtained by running lean/lake build over sorry-filled files. The generation pipeline uses executable feedback (pytest exit codes, Lean typechecking, and Plausible property checks) to filter outputs, and the final benchmark artifacts are new theorem statements rather than restatements of the pipeline's own acceptance criteria. No equation, parameter, or fitted quantity is renamed as a prediction: the 30% and 18% success rates are empirical counts of proofs that compile, not quantities forced by the construction of the benchmark. The overlap between the model used for generation (Claude Sonnet) and the model evaluated is a real contamination/selection concern, but it does not make the reported success rates true by construction, since the baseline model is not given the generation transcripts and must produce proofs for statements it has not necessarily seen. The paper's Section V admission that 'particular theorems are not applicable or vacuous in some form' is a serious validity risk for the benchmark's soundness, but it is a limitation of the data quality, not a circular step in the derivation of the benchmark or its baseline numbers. The only self-citation in the paper, Dafny Copilot [Fou24], appears in related work and is not load-bearing for any central claim. Under the hard rule that circularity requires a specific reduction of a claimed result to its own inputs by construction, no such reduction is present.

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

This is a dataset paper, so there are no fitted constants in the mathematical sense. The main unexamined inputs are the APPS source data, the LLM's translation to Lean, and the property-testing filter.

assumptions (4)

domain assumption APPS problem statements, solutions, and unit tests are correct and cover each problem's intended behavior.
The entire pipeline builds on APPS data without independent verification of every sample.
domain assumption Claude Sonnet 3.5's conversion of Python solutions and property tests into Lean 4 theorem statements is faithful.
The theorem statements are generated by an LLM and only checked by typechecking and random property testing, not by proof. Section II-B.
domain assumption Plausible property-based testing is sufficient to establish that a theorem is 'probably true'.
Stage five filters theorems only by random testing, not by proof, so a theorem could be false yet pass all tests. Section II-B.
standard math Lean 4, Mathlib, and the pinned versions behave correctly.
The construction and baseline rely on Lean 4.12.0 and Mathlib commit 809c3fb3b5c8f5d7dace56e200b426187516535a. Section III-A.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Proving the Coding Interview: A Benchmark for Formally Verified Code Generation." pith.science (2026). https://pith.science/paper/SMMZFC5Z

@misc{pith2026250205714,
  author       = {Pith},
  title        = {Pith review of: Proving the Coding Interview: A Benchmark for Formally Verified Code Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SMMZFC5Z}},
  note         = {Machine review of arXiv:2502.05714}
}

read the original abstract

We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness, the largest formal verification benchmark, including 1083 curated and quality controlled samples. Previously, APPS provided a benchmark and dataset for programming puzzles to be completed in Python and checked against unit tests, of the kind seen in technical assessments in the software engineering industry. Building upon recent approaches for benchmarks in interactive theorem proving, we generalize the unit tests to Lean 4 theorems given without proof (i.e., using Lean's "sorry" keyword). On the 406 theorems of 100 randomly selected samples, Sonnet correctly proves 30% and Gemini correctly proves 18%. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and its associated correctness specifications. The benchmark is available at https://huggingface.co/datasets/quinn-dougherty/fvapps.

Figures

Figures reproduced from arXiv: 2502.05714 by the authors.

**Figure 1.** Benchmark generation pipeline for creating coding interview theorem statements in Lean from APPS questions and solutions. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗

**Figure 2.** FVAPPS sample 23, derived from train sample 23 of APPS source. The [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

**Figure 3.** Our generic scaffolding loop used at various stages of our pipeline. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗

Figures from the paper (6 more)

**Figure 4.** Figure 4: Total number of defs and theorems across FVAPPS samples. [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]

**Figure 7.** Figure 7: Number of theorem attempts it took to solve a theorem, conditional [PITH_FULL_IMAGE:figures/full_fig_p005_7.png]

**Figure 6.** Figure 6: Qualitative categories of theorem solutions in the 100 samples, first [PITH_FULL_IMAGE:figures/full_fig_p005_6.png]

**Figure 8.** Figure 8: Definition attempts needed to solve a function, conditional on success. [PITH_FULL_IMAGE:figures/full_fig_p007_8.png]

**Figure 9.** Figure 9: claude-3-5-sonnet-20241022’s attempt at the definition for sample 23 [PITH_FULL_IMAGE:figures/full_fig_p007_9.png]

**Figure 10.** Figure 10: gemini-1.5-pro’s solution to the definition for sample 23 of FVAPPS [PITH_FULL_IMAGE:figures/full_fig_p008_10.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 2 canonical work pages

[6]

Code Llama: Open Foundation Models for Code

[Roz+23] Baptiste Rozière et al. “Code Llama: Open Foundation Models for Code”. In: ArXiv abs/2308.12950 (2023). URL: https : / / api . semanticscholar.org/CorpusID:261100919. [Sin+23] Mukul Singh et al. “CodeFusion: A Pre-trained Diffusion Model for Code Generation”. In: ArXiv abs/2310.17680 (2023). URL: https : / / api . semanticscholar.org/CorpusID:264...

arXiv 2023
[7]

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

arXiv: 2310.00656 [cs.AI]. [Yan+23] Kaiyu Yang et al. “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”. In: arXiv preprint arXiv:2306.15626 (2023). [Alp24] AlphaProof and AlphaGeometry teams. AI achieves silver-medal standard solving Interna- tional Mathematical Olympiad problems . Google DeepMind. July

arXiv 2023
[9]

[Dee+24] DeepSeek-AI et al

arXiv: 2403.04132 [cs.AI]. [Dee+24] DeepSeek-AI et al. DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model

arXiv
[10]

21783 [cs.AI]

arXiv: 2407 . 21783 [cs.AI]. URL: https://arxiv.org/abs/2407.21783. [Fou24] Beneficial AI Foundation. Dafny Copilot

arXiv
[11]

LiveCodeBench: Holistic and Contamination Free Evaluation of Large Lan- guage Models for Code

URL: https : / / github . com / Beneficial - AI - Foundation/dafny-autopilot. [Jai+24] Naman Jain et al. “LiveCodeBench: Holistic and Contamination Free Evaluation of Large Lan- guage Models for Code”. In: arXiv preprint (2024). [Lou+24] Chloe Loughridge et al. “DafnyBench: A Bench- mark for Formal Software Verification”. In: arXiv preprint arXiv:2406.084...

arXiv 2024
[12]

Clover: Closed-loop verifiable code generation

arXiv: 2303.08774 [cs.CL]. URL: https://arxiv. org/abs/2303.08774. [Sun+24] Chuyue Sun et al. “Clover: Closed-loop verifiable code generation”. In: ICLR 2024 Conference

arXiv 2024
[13]

DeepSeek-Prover-V1.5: Har- nessing Proof Assistant Feedback for Reinforce- ment Learning and Monte-Carlo Tree Search

arXiv: 2407 . 16741 [cs.SE]. URL: https://arxiv.org/abs/2407.16741. [Xin+24a] Huajian Xin et al. “DeepSeek-Prover-V1.5: Har- nessing Proof Assistant Feedback for Reinforce- ment Learning and Monte-Carlo Tree Search”. In: arxiv (2024). arXiv: 2408.08152 [cs.CL]. URL: https://arxiv.org/abs/2408.08152. [Xin+24b] Huajian Xin et al. DeepSeek-Prover: Advanc- in...

arXiv 2024
[14]

URL: https : / / arxiv

arXiv: 2405.14333 [cs.AI]. URL: https : / / arxiv. org / abs / 2405 . 14333. [Yan+24] Chenyuan Yang et al. AutoVerus: Automated Proof Generation for Rust Code

arXiv

Show all 15 references

[15]

URL: https://arxiv.org/ abs/2409.13082

arXiv: 2409.13082 [cs.SE]. URL: https://arxiv.org/ abs/2409.13082

arXiv
[1891]

Learning to prove theorems via interacting with proof assistants

ISSN : 2475-9066. DOI: 10 . 21105 / joss . 01891. URL: http://dx.doi.org/10.21105/joss.01891. [YD19] Kaiyu Yang and Jia Deng. “Learning to prove theorems via interacting with proof assistants”. In: arXiv preprint arXiv:1905.09381 (2019). [Ell+20] Kevin Ellis et al. DreamCoder:...

2019 arXiv
[2004]

Mining the Archive of Formal Proofs

URL: https://coq. inria.fr. [Bla+15] Jasmin Christian Blanchette et al. “Mining the Archive of Formal Proofs”. In:International Con- ference on Intelligent Computer Mathematics . Springer. 2015, pp. 3–17. [Mou+15] Leonardo de Moura et al. “The Lean Theorem Prover (System Descr...

2015
[2006]

URL: https : / / arxiv

08381 [cs.AI]. URL: https : / / arxiv. org / abs / 2006.08381. [Aus+21] Jacob Austin et al. Program Synthesis with Large Language Models

2006 arXiv
[2021]

Evaluating large language models trained on code

arXiv: 2108 . 07732 [cs.PL]. URL: https : / / arxiv. org / abs / 2108 . 07732. [Che+21] Mark Chen et al. “Evaluating large language models trained on code”. In: arXiv preprint arXiv:2107.03374 (2021). [Hen+21] Dan Hendrycks et al. “Measuring Coding Chal- lenge Competence With ...

2021 arXiv
[2023]

Swe-bench: Can lan- guage models resolve real-world github issues?

URL: https://lean-lang.org/ functional_programming_in_lean/. [Jim+23] Carlos E Jimenez et al. “Swe-bench: Can lan- guage models resolve real-world github issues?” In: arXiv preprint arXiv:2310.06770 (2023). [Lei23] K Rustan M Leino. Program Proofs. MIT Press,

2023 arXiv
[2024]

google/discover/blog/ai-solves-imo-problems-at- silver-medal-level/ (visited on 10/30/2024)

URL: https : / / deepmind . google/discover/blog/ai-solves-imo-problems-at- silver-medal-level/ (visited on 10/30/2024). [Chi+24] Wei-Lin Chiang et al. Chatbot Arena: An Open Platform for Evaluating LLMs by Human Prefer- ence

2024

Pith tools

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

[1] [6]

Code Llama: Open Foundation Models for Code

[Roz+23] Baptiste Rozière et al. “Code Llama: Open Foundation Models for Code”. In: ArXiv abs/2308.12950 (2023). URL: https : / / api . semanticscholar.org/CorpusID:261100919. [Sin+23] Mukul Singh et al. “CodeFusion: A Pre-trained Diffusion Model for Code Generation”. In: ArXiv abs/2310.17680 (2023). URL: https : / / api . semanticscholar.org/CorpusID:264...

arXiv 2023

[2] [7]

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

arXiv: 2310.00656 [cs.AI]. [Yan+23] Kaiyu Yang et al. “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”. In: arXiv preprint arXiv:2306.15626 (2023). [Alp24] AlphaProof and AlphaGeometry teams. AI achieves silver-medal standard solving Interna- tional Mathematical Olympiad problems . Google DeepMind. July

arXiv 2023

[3] [9]

[Dee+24] DeepSeek-AI et al

arXiv: 2403.04132 [cs.AI]. [Dee+24] DeepSeek-AI et al. DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model

arXiv

[4] [10]

21783 [cs.AI]

arXiv: 2407 . 21783 [cs.AI]. URL: https://arxiv.org/abs/2407.21783. [Fou24] Beneficial AI Foundation. Dafny Copilot

arXiv

[5] [11]

LiveCodeBench: Holistic and Contamination Free Evaluation of Large Lan- guage Models for Code

URL: https : / / github . com / Beneficial - AI - Foundation/dafny-autopilot. [Jai+24] Naman Jain et al. “LiveCodeBench: Holistic and Contamination Free Evaluation of Large Lan- guage Models for Code”. In: arXiv preprint (2024). [Lou+24] Chloe Loughridge et al. “DafnyBench: A Bench- mark for Formal Software Verification”. In: arXiv preprint arXiv:2406.084...

arXiv 2024

[6] [12]

Clover: Closed-loop verifiable code generation

arXiv: 2303.08774 [cs.CL]. URL: https://arxiv. org/abs/2303.08774. [Sun+24] Chuyue Sun et al. “Clover: Closed-loop verifiable code generation”. In: ICLR 2024 Conference

arXiv 2024

[7] [13]

DeepSeek-Prover-V1.5: Har- nessing Proof Assistant Feedback for Reinforce- ment Learning and Monte-Carlo Tree Search

arXiv: 2407 . 16741 [cs.SE]. URL: https://arxiv.org/abs/2407.16741. [Xin+24a] Huajian Xin et al. “DeepSeek-Prover-V1.5: Har- nessing Proof Assistant Feedback for Reinforce- ment Learning and Monte-Carlo Tree Search”. In: arxiv (2024). arXiv: 2408.08152 [cs.CL]. URL: https://arxiv.org/abs/2408.08152. [Xin+24b] Huajian Xin et al. DeepSeek-Prover: Advanc- in...

arXiv 2024

[8] [14]

URL: https : / / arxiv

arXiv: 2405.14333 [cs.AI]. URL: https : / / arxiv. org / abs / 2405 . 14333. [Yan+24] Chenyuan Yang et al. AutoVerus: Automated Proof Generation for Rust Code

arXiv