{"id":"a46b0278-e10a-4182-9e71-b44603a5de0f","arxiv_id":"2502.05714","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"FVAPPS converts 4,715 APPS coding puzzles into Lean 4 'prove your program correct' tasks and reports that frontier LLMs prove roughly 30% of sampled theorems.","lead":"The authors built FVAPPS, a benchmark that turns 4,715 coding interview problems from APPS into Lean 4 tasks where AI must both write a program and prove it correct. It is meant to push AI beyond passing hidden unit tests, toward code that carries a mathematical proof of correctness.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The curated subset is only Plausible-tested, not proof-checked; Section V concedes statements may be vacuous or inapplicable, so benchmark validity and the 30%/18% baselines are not yet established.","rationale":"The reader's weakest assumption—that LLM-generated theorem statements are true, non-vacuous formalizations of intended correctness properties—is exactly the load-bearing point. If this fails, the benchmark does not measure verified coding ability and the baseline percentages lose their meaning. The paper is transparent about the limitation in Section V, but transparency does not supply the missing support. The pipeline's Plausible step is genuine empirical evidence, yet finite random sampling cannot establish truth, and the paper's own admission of possible vacuity is not accompanied by any quantified audit. Baseline successes are also not cleanly separated from the 'Bug' and 'Too trivial' categories in Table III and Figure 6, so even the reported 30%/18% may not reflect correct proofs of intended theorems. I do not see evidence of fraud or carelessness; the public dataset and repository are a useful contribution, and the right fix is a validation audit rather than rejection. Since the reader's conditional verdict already identifies this concern and my check would make the required condition explicit, the verdict remains conditional: adopt the benchmark but insist on an independent audit before relying on the headline numbers.","tokens_in":9681,"tokens_out":8759,"duration_ms":100384,"concrete_test":"Run an independent audit on a random sample of 100 Guarded and Plausible samples: have two Lean-competent annotators, neither an author, formalize a reference solution to the original APPS problem and try to prove or refute every theorem statement in Lean, classifying each as true-and-substantive, vacuous/trivial, or false/mistranslated, with pre-registered thresholds. Report the counts and inter-annotator agreement; if more than 5% of curated statements are false or more than 20% are vacuous, the quality-control claim and the headline 30%/18% numbers require revision.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section V explicitly concedes that 'particular theorems are not applicable or vacuous in some form.' The central claims—that FVAPPS is the largest formal verification benchmark and that frontier LLMs correctly prove only 30%/18% of theorems—require the 1,083 curated theorem statements to be true, non-vacuous, and faithful to the intended correctness properties of each APPS problem. Stage 5 filters by Plausible, a finite random-sampling property tester, not by proof, so false statements can pass and vacuous statements (e.g., a nonnegativity theorem for a Nat-valued output) are not systematically excluded. The papers own qualitative tables also label some completed theorems as 'too trivial' or 'Bug,' implying that the reported success counts mix genuine proofs of intended properties with easy or spurious ones. No independent validation of the generated statements is reported; the manual spot-check is not quantified, and no inter-annotator or pre-registered criterion is given. If the statements are false, model failures are benchmark artifacts; if they are vacuous or trivial, success rates overstate verified coding ability.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":9822,"tokens_out":4721,"duration_ms":50391,"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":[{"comment":"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":"Section V; Section II-B, Stage 5; Figure 2"},{"comment":"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":"Section III-D; Figure 6; Table III"},{"comment":"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.","section":"Section II-B; Section III-A"},{"comment":"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.","section":"Abstract; Section IV-A"}],"minor_comments":[{"comment":"The word \"nontheless\" appears twice in the discussion; it should be \"nonetheless.\"","section":"Section V"},{"comment":"\"withing\" and \"falling withing the scope\" should be \"within\" and \"falling within the scope.\"","section":"Section II-B"},{"comment":"\"FILTERED TO THOSE THAT MADE IT PASSED STAGE 3\" should read \"made it past Stage 3.\"","section":"Table I caption"},{"comment":"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.\"","section":"Appendix, Figure 10"},{"comment":"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.","section":"Figure 6 and Table III"}],"recommendation":"major_revision","confidential_remarks":"The authors are unusually transparent about the limitations of their own benchmark, and the resource has clear potential value. However, the load-bearing claims—dataset quality and baseline success rates—need substantially more validation or a careful restatement before publication. I recommend major revision rather than rejection because the issues are fixable within the manuscript's scope, and the benchmark itself is a meaningful contribution to the community."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat'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.\n\nThe 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.\n\nThe 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.\n\nBottom 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.","headline":"A large new benchmark that is honestly presented but not yet validated; send to review with major revisions.","tokens_in":10393,"tokens_out":2888,"would_cite":false,"duration_ms":25176,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["formal verification","benchmark","Lean 4","program synthesis","LLM code generation","theorem proving","property-based testing","APPS dataset"],"falsifier":"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.","tokens_in":9422,"feed_emoji":"✅","tokens_out":11777,"duration_ms":107346,"temperature":0.7,"pith_summary":"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.","feed_headline":"LLMs prove just 30% of a new verified-coding benchmark","feed_subtitle":"FVAPPS ships 4,715 Lean formalizations of coding-interview problems; frontier models solve only a minority of the proofs.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the APPS coding problems, Python solutions, and unit tests that FVAPPS is built from.","marker":"[Hen+21]"},{"why":"Describes the Lean theorem prover that typechecks the benchmark's 'sorry'-ed statements and proofs.","marker":"[Mou+15]"},{"why":"Supplies the property-based testing methodology used in stage two of the generation pipeline.","marker":"[MHC19]"},{"why":"Defines DafnyBench, the closest prior formal verification benchmark whose scale the FVAPPS 'largest' claim is set against.","marker":"[Lou+24]"},{"why":"Documents Clover, a closed-loop verifiable code generation benchmark an order of magnitude smaller, used as scale context.","marker":"[Sun+24]"},{"why":"Documents dafny-synthesis, another prior verified program synthesis benchmark with roughly a hundred programs.","marker":"[Mis+24]"},{"why":"Supports the paper's choice of Lean 4 for expressing general-purpose programs beyond pure mathematics.","marker":"[Chr23]"},{"why":"Reports the open-source DeepSeek-Prover model that the authors tried and found insufficient, motivating their scaffolded baseline setup.","marker":"[Xin+24a]"}],"fun_headline_variants":["New verified coding benchmark stumps LLMs at 30%","FVAPPS: 4,715 Lean proofs, LLMs solve under a third","Coding interviews meet formal proof: benchmark shows LLM limits","Formal verification benchmark: LLMs prove only 30% of tasks","Largest verified coding benchmark challenges LLMs to prove code"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["New verified coding benchmark stumps LLMs at 30%","FVAPPS: 4,715 Lean proofs, LLMs solve under a third","Coding interviews meet formal proof: benchmark shows LLM limits","Formal verification benchmark: LLMs prove only 30% of tasks","Largest verified coding benchmark challenges LLMs to prove code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000164,"raw_usage":{"total_tokens":1210,"prompt_tokens":869,"completion_tokens":341,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":485,"completion_tokens_details":{"reasoning_tokens":249}},"tokens_in":485,"tokens_out":341,"duration_ms":3876,"temperature":1.0,"reasoning_tokens":249,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T18:14:40.203116+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}