{"id":"0209748a-ed9b-4a99-97af-5e8681355b0b","arxiv_id":"2608.13077","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"COINS, a test-case-based Rocq evaluation framework, shows frontier LLMs generate few candidate formal specifications on HumanEval, with rates between 1.22% and 28.05%.","lead":"This paper introduces COINS, a Rocq-based framework that evaluates LLM-written program specifications by checking whether they accept trusted positive tests and reject mutated negative ones. It reports that even frontier LLMs produce few candidate specifications for HumanEval, and argues test-case-based checks are more discriminative than full equivalence proofs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"REJECT all appears empirically vacuous: in Table 2 every row shows PASS all = REJECT all, so no specification was ever eliminated by the negative stage; headline candidate rates are therefore indistinguishable from positive-case acceptance, and the machine-unchecked negative direction (Sec.","rationale":"Good-faith reading: COINS is a well-motivated attempt to make specification evaluation tractable and interpretable. The positive direction is genuinely sound—every PASS all result is a machine-checked Rocq proof of acceptance on a trusted positive case—and the paper leverages the correct asymmetry (proof success is reliable; failure is ambiguous). The RQ3 ablation, the CLEVER comparison, the Fixpoint analysis, and the error taxonomy are useful, and Appendix B.4 is honest about the negative direction's limitation, which counts in the authors' favor. What would have to be true for the central claim to hold is that the negative stage has real discriminating power, so that an over-permissive specification is likely to be caught rather than waved through by an LLM judgment. The paper's own numbers do not demonstrate this and are fully consistent with the opposite: PASS all and REJECT all are numerically identical in every row of Table 2 for six models and the human anchor across 1,640 negative cases; no specification is reported as eliminated by REJECT all; and the intermediate counts do not reconcile across Figure 1, Section 4.2, Table 2, and Appendix E. If REJECT all never fires, the candidate rate equals the PASS all rate, and PASS all is precisely the quantity that RQ3 shows to be verifier-sensitive (+3.05%), so the headline spread (1.22% to 28.05%) cannot be attributed to generation capability until the negative stage demonstrably contributes. The planted-specification calibration test proposed above settles which reading is correct: if deliberately weakened specifications are eliminated and judgment/proof-success rates are reported, the benchmark stands as a faithful measure; if planted over-permissive specs survive REJECT all, the candidate rates are upper bounds and the 'sound, faithful' wording must be revised. This is a strengthening of the reader's condition, not a rejection: the positive findings are real, the limitations section anticipates part of this concern, and the appropriate disposition remains conditional acceptance pending the calibration evidence and the reconciliation of the reported counts. The reader's weakest assumption identified the same mechanism (the unreliability of the LLM's skip decision as rejection evidence); this review adds that Table 2's column equality makes the vacuous-filter failure mode the default reading of the data, not a corner case.","tokens_in":24624,"tokens_out":18283,"duration_ms":186466,"concrete_test":"Calibrate the negative stage with planted over-permissive specifications. Take 20 human-written reference specifications that pass PASS all; weaken each by deleting one conjunct or relaxing one bound, and confirm, by constructing the acceptance proof with a generous budget, that each weakened spec accepts at least one of the existing 1,640 negative cases. Then run the full COINS pipeline (Gemini 3 Pro Preview prover, identical prompts) on these 20 planted specs and measure how many are eliminated at REJECT all, reporting the LLM's accept/reject judgment rate and negative-case proof-success rate. If any planted spec survives, the negative direction is unreliable and candidate rates are upper bounds rather than faithful measures; if all are eliminated, re-run PASS all to confirm the planted flaws are not already caught there, thereby isolating REJECT all's marginal contribution.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires REJECT all to supply reliable, machine-unchecked-in-theory but effective-in-practice evidence that candidate specifications reject incorrect behaviors. Section 3.2 explicitly skips the formal proof whenever the LLM prover judges rejection ('proving rejection can be harder'), and Appendix B.4 concedes R_all(S)=top does not guarantee rejection. What is new here is that the paper's own data are consistent with the stage being vacuous: in Table 2, PASS all and REJECT all are numerically identical in every row (GPT-4o 4.27/4.27, DeepSeek-V3.1 1.22/1.22, Claude 3.7 Sonnet 1.83/1.83, Claude 4.5 Opus 14.63/14.63, GPT-5 15.24/15.24, Gemini 3 Pro Preview 28.05/28.05). Across 164 problems and 1,640 negative cases, no specification that passed all positive cases is reported to be eliminated at the negative stage for any model. The human anchor shows the same pattern: Table 1 gives Gemini PASS all 29.88% (49) while Appendix E reports 50 human REJECT all candidates, an impossible combination under the paper's candidate definition (PASS all and REJECT all). The advertised intermediate counts also do not reconcile: Figure 1's annotation says Gemini goes 164 to 43 candidates, Section 4.2's text says 26.22%, and Table 2 says 28.05% (46). Two readings fit the column equality: either the ~756-case positive suite is so constraining that over-approximation is impossible (the paper's 'Precision Emerges from Coverage' claim), or the negative judge routinely answers 'not accepted' and the prover rarely finds acceptance proofs, making REJECT all an expensive no-op. The paper reports no intermediate attrition, no accept/reject judgment rates, and no negative-case proof-success rates, so the reader cannot distinguish these.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript introduces COINS, a Rocq-based evaluation framework for LLM-generated formal program specifications. Instead of proving full semantic equivalence, COINS instantiates each candidate specification on positive and negative test cases and asks an LLM prover to discharge the resulting proof obligations; a specification becomes a 'candidate' when it passes both the positive-acceptance stage and the negative-rejection stage. The authors contribute a manually written Rocq specification for each of the 164 HumanEval problems, generate 1,640 mutated negative cases, and evaluate six LLMs. They report large gaps in specification-generation ability, with REJECT all rates from 1.22% to 28.05%, and argue that test-case-based formal reasoning is more faithful and discriminative than full equivalence proving. The paper also presents an equivalence analysis between human and LLM candidates, an ablation study separating specification quality from prover strength, and secondary analyses of syntax errors, Fixpoint usage, and input-type difficulty.","tokens_in":25047,"tokens_out":7707,"duration_ms":76145,"significance":"The curated human-written Rocq specification suite for all 164 HumanEval problems is a genuinely useful resource, and the positive-case proof obligations are machine-checked, giving the PASS all results a sound core. The framework's goal of separating specification quality from prover capability is timely, and the reported model ordering is a falsifiable empirical claim. However, the headline REJECT all metric currently rests on unverified LLM judgments for negative cases and is numerically identical to PASS all in every reported row; the equivalence-based faithfulness validation is also too thin (9 proven equivalents and 3 manual inspections) to carry the 'faithful and discriminative' conclusion. The contribution is therefore conditional: the benchmark and dataset are valuable, but the central evidential claim about rejecting over-permissive specifications is not yet supported.","major_comments":[{"comment":"The REJECT all stage does not provide the sound negative evidence that the abstract and conclusion claim. Section 3.2 states that if the LLM judges a negative case as rejected, the formal proof is skipped because 'proving rejection can be harder,' and Appendix B.4 explicitly concedes that R_all(S)=top does not guarantee that S rejects all negative cases. This would be acceptable as a heuristic if the stage were shown to be informative, but Table 2 shows that REJECT all equals PASS all in every row (e.g., GPT-4o 4.27%/4.27%, DeepSeek-V3.1 1.22%/1.22%, Gemini 3 Pro Preview 28.05%/28.05%), so no specification was ever eliminated by the negative stage across 164 problems and 1,640 negative cases. The headline candidate rates are therefore indistinguishable from positive-case acceptance rates, and the interpretation 'Precision Emerges from Coverage' is only one of two readings; the other is that the negative judge rarely or never attempts acceptance proofs. To support the central claim, the authors should either machine-check rejection (for example, prove False from the specification and the negative input-output pair), or report per-negative-case LLM judgment statistics and demonstrate, on a known over-permissive specification, that the REJECT all stage can actually fail a candidate.","section":"§3.2, Table 2, Appendix B.4"},{"comment":"The faithfulness evidence is too thin to support the claim that COINS provides a 'faithful and discriminative measure of progress.' Only 29 of 80 unique problems have both a human and an LLM candidate; of those, only 9 have provable equivalence in both directions, 3 are manually judged equivalent, and 17 fail in both directions. Manual inspection of the 3 single-direction cases does not rule out genuine semantic divergence in the 17 bidirectional failures, so the aggregate numbers do not establish that candidates passing COINS are semantically equivalent to the curated human intent. The authors should either provide a much larger equivalence-validation sample with error analysis of the failures, or explicitly restrict the faithfulness claim to 'consistent with all tested positive and negative cases.'","section":"Appendix E, Table 1, §4.2"},{"comment":"The headline numbers are internally inconsistent. Table 2 reports Gemini 3 Pro Preview REJECT all as 28.05% (46), while Figure 1 annotates the pipeline as 164 to 43 candidates and Section 4.2 gives 26.22% for Gemini; Appendix E reports 50 validated human candidates even though Table 1 lists only 49 human specifications passing PASS all. Under the paper's own candidate definition (PASS all plus REJECT all), these counts cannot all be correct, and they prevent a reader from reproducing the main result. Please reconcile the numbers and report the exact per-stage filtering counts for every model.","section":"Table 2 vs Figure 1, §4.2, Appendix E"},{"comment":"The statement that only 31.0% of test-based candidates yield 'provably isomorphic specifications' is used to conclude that equivalence proving systematically underestimates specification quality. The 31.0% figure is 9 out of 29 overlapping problems, not a rate over all candidates, and the 17 bidirectional failures are not analyzed to distinguish prover failure from semantic difference. Without a control (for example, known-equivalent specification pairs discharged by the same prover), the conclusion that equivalence-based evaluation is unreliable because of proof complexity is not established; it may instead reflect that many candidate specifications are not actually equivalent to the human intent.","section":"§4.3, Appendix B.5, Appendix E"}],"minor_comments":[{"comment":"The claim that 'syntactically valid Rocq specifications are often semantically precise under our test-based evaluation' is difficult to reconcile with Appendix J's example of a syntactically valid but contradictory specification; please qualify the claim with the observed failure rates.","section":"§4.2"},{"comment":"The row for Gemini 3 Pro Preview ('17 8 5 636') appears to be a rendering error; the counts should sum to 36.","section":"Table 4"},{"comment":"The probability statement Pr[VERIFY_M(S,i,o)=proof]=0 when S(i,o)=⊥ should state that 'proof' means a type-checked proof, since an LLM can emit invalid proof scripts that the Rocq kernel rejects.","section":"Appendix B.1, Definition B.1"}],"recommendation":"major_revision","confidential_remarks":"The paper has a promising benchmark and a valuable human-curated specification suite, but the main metric needs to be either made machine-checked or honestly relabeled as positive-case acceptance; otherwise the empirical claims will not withstand scrutiny."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a read, and worth sending to referees, but the headline metric needs a hard look. What is new and useful: COINS, a test-case instantiation framework for evaluating LLM-written Rocq specifications, and the first complete human-written Rocq specification suite for HumanEval. The positive evidence is real—every accepted test case is backed by a Rocq-checked proof. The mutation-derived negative suite is a sensible idea, and the ranking of models from 1.22% to 28.05% is at least a plausible ordering of specification-generation ability. The RQ4 result on Fixpoint versus relational style is also a solid, practical observation.\n\nThe problem is REJECT all. In Table 2, PASS all and REJECT all are numerically identical in every row, for every model. No specification was ever eliminated by the negative stage. The paper calls this \"Precision Emerges from Coverage\" and argues the positive suite is strong enough to enforce precision. That is possible, but it is also possible that the negative stage is an expensive no-op: the LLM judge says \"not accepted,\" the prover never attempts a formal rejection proof, and the specification is never actually shown to reject anything. Appendix B.4 concedes R_all(S)=top does not guarantee rejection, yet the abstract and conclusion describe the evidence as \"sound\" and \"faithful.\" The sound part only covers the positive direction.\n\nThe paper is transparent about some of this in the appendix, but the main text does not report per-stage attrition, accept/reject judgment rates, or negative-case proof success rates. Without those numbers, a reader cannot distinguish the paper's favorable interpretation from a vacuous filter.\n\nThere are also small internal inconsistencies that a referee should not have to hunt for: Appendix E reports 50 human REJECT-all candidates, which is impossible under the paper's own candidate definition when Table 1 gives Gemini PASS all = 49. Figure 1 shows 164→43, Section 4.2 says 26.22%, and Table 2 says 28.05% (46). Not fatal, but sloppy.\n\nThe \"faithful\" claim rests on a small equivalence analysis—9 proven equivalents plus 3 inspected by hand—so that word should be toned down.\n\nBottom line: the artifact and positive-side methodology are worth engaging seriously. The negative-side metric, as reported, is not doing empirical work, and the paper should be revised to say so plainly and to provide the missing attrition data. I would send this to reviewers; it deserves a serious referee, but with a clear request to reconcile the numbers and reframe the REJECT-all claim.","headline":"The paper ships a genuinely useful artifact—the first full HumanEval Rocq specification suite—but the headline REJECT-all metric is empirically indistinguishable from PASS-all in every reported row, so the paper's central methodological claim is softer than the abstract suggests.","tokens_in":25601,"tokens_out":2833,"would_cite":true,"duration_ms":31765,"reading_group":"yes","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 tries to establish that formal specs can be judged by test-case proofs, which exposes real model differences hidden by equivalence-based benchmarks.","keywords":["COINS","formal specification generation","LLM evaluation","Rocq proof assistant","HumanEval","test-case-based verification","mutation testing","specification quality"],"falsifier":"Take any candidate specification from Table 2 and run a second prover or an exhaustive tactic search on its ten negative cases; if a negative case is shown in Rocq to satisfy the specification, REJECT all has passed an over-permissive spec and the candidate rates mix quality with missed proofs.","tokens_in":24429,"feed_emoji":"🧪","tokens_out":15063,"duration_ms":144722,"temperature":0.7,"pith_summary":"The paper tries to establish that LLM-written formal program specifications are best evaluated by instantiating them on trusted positive and negative test cases and proving the resulting obligations in the Rocq proof assistant, rather than by proving semantic equivalence to a ground-truth specification. It argues that this design matches the asymmetry of formal reasoning: a successfully checked proof is sound positive evidence, while a failed proof is ambiguous and can reflect proof difficulty instead of a bad specification. On a new suite of 164 human-written Rocq specifications for HumanEval, the proposed COINS framework scores six LLMs between 1.22% and 28.05% candidate specifications, separating models where an equivalence-based benchmark produced almost no discriminative signal. If the paper is right, accurate evaluation, not model scaling alone, is what will reveal progress in specification synthesis, and test-case-based formal reasoning is the practical way to get that signal.","feed_headline":"Even the best LLM's formal spec passes tests only 28% of the time","feed_subtitle":"It separates proof difficulty from specification quality, so the 1.22% to 28.05% model spread is meaningful.","key_machinery":"The central mechanism is the COINS pipeline: each generated specification is a Rocq proposition spec(input, output) that gets instantiated on concrete input-output pairs, producing proof obligations the model must discharge with Rocq-checked proofs. Positive cases test coverage; negative cases, produced by mutating canonical implementations, test whether the specification is too permissive; a candidate specification must pass all positive proof obligations and have no negative case for which an acceptance proof is found. The design leans on an asymmetry principle the paper formalizes: a constructed proof is reliable evidence by the soundness of the Rocq type checker, while a failed proof is inherently ambiguous, so the benchmark maximizes successful proofs rather than treating failures as verdicts. An optional final stage attempts equivalence to human-written reference specifications, but the paper keeps that stage secondary because it reintroduces the proof burden that hides quality.","core_discovery":"COINS's claim is that specification quality can be read off from how a specification behaves on concrete, trusted test cases: a candidate specification must provably accept all positive cases and must not be provably over-permissive on mutated negative cases. The paper reports candidate rates from 1.22% for the weakest model to 28.05% for the strongest, and an ablation that improves specification quality by +5.01% versus +3.05% for a stronger verifier. The paper's conclusion is that specification generation remains a hard open problem, that full equivalence proofs systematically underestimate quality because verification complexity obscures real differences, and that test-case-based formal reasoning is a faithful, discriminative middle ground for future benchmarks.","pith_inferences":["Editorial: the asymmetry principle—proofs are reliable, failed proofs are not—should transfer to other formal artifacts, so benchmarks for invariants, contracts, and autoformalization that treat failed proof attempts as verdicts will systematically underestimate model ability.","Editorial: a concrete follow-up test is to rerun COINS on the 46 strongest-model candidates with a second independent prover or a stronger tactic search and measure how many unseen acceptance proofs appear among the skipped negative cases.","Editorial: the mutated negative cases come from a fixed budget around canonical implementations, so over-permissive specifications whose bad outputs lie outside that neighborhood can pass; adding property-based random negative cases would make REJECT all harder to fool."],"forward_implications":["Candidate rates from 1.22% to 28.05% reflect genuine differences in specification-writing ability rather than prover skill, because test-case proof obligations are small enough for the chosen verifier to mostly discharge.","Equivalence-based metrics understate LLM specification quality: only 31.0% of test-case-passing specs were provably isomorphic to human references, so full equivalence proofs should not be the primary evaluation target.","Specification quality is a distinct capability from code generation: even where HumanEval coding is saturated, model gaps on specifications remain wide, so specification synthesis deserves separate and more discriminative benchmarks.","Ablation results imply that both generation quality and verifier power matter, with specification quality contributing +5.01% and a stronger verifier +3.05%, so benchmark protocols must control both factors."],"supporting_citations":[{"why":"Supplies the 164 HumanEval problems whose reference implementations feed both the human specifications and the positive and negative test cases.","marker":"Chen et al., 2021"},{"why":"Defines the equivalence-based CLEVER benchmark that COINS contrasts with; its 0.621% correctness illustrates how full equivalence proofs destroy discriminative signal.","marker":"Thakur et al., 2025"},{"why":"Grounds the Rocq proof assistant whose type-checker soundness makes constructed acceptance proofs reliable positive evidence.","marker":"Huet et al., 1997"},{"why":"Marks the property-based testing contrast: QuickChick checks executable properties while COINS evaluates potentially non-executable specifications through proof obligations.","marker":"Paraskevopoulou et al., 2015"},{"why":"Supports the paper's claim that for simple programs a diverse test suite leaves little room for over-approximation, explaining the close alignment of PASS all and REJECT all.","marker":"Le-Cong et al., 2025"}],"fun_headline_variants":["LLM specs pass tests at best 28% -- COINS eval","Formal spec generation: top LLM only 28% on tests","COINS: test-based spec eval reveals LLM gap","Spec quality vs proof difficulty: COINS separates","LLMs write specs, but quality hits 28% ceiling"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"REJECT all assumes that an LLM prover's failure to construct an acceptance proof for a negative case counts as the specification rejecting that case, but the pipeline never checks a formal proof of rejection.","fun_headline_variants_meta":{"raw":{"variants":["LLM specs pass tests at best 28% -- COINS eval","Formal spec generation: top LLM only 28% on tests","COINS: test-based spec eval reveals LLM gap","Spec quality vs proof difficulty: COINS separates","LLMs write specs, but quality hits 28% ceiling"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000161,"raw_usage":{"total_tokens":1216,"prompt_tokens":907,"completion_tokens":309,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":523,"completion_tokens_details":{"reasoning_tokens":223}},"tokens_in":523,"tokens_out":309,"duration_ms":3852,"temperature":1.0,"reasoning_tokens":223,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T17:16:55.925177+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any candidate specification from Table 2 and run a second prover or an exhaustive tactic search on its ten negative cases; if a negative case is shown in Rocq to satisfy the specification, REJECT all has passed an over-permissive spec and the candidate rates mix quality with missed proofs.","supporting_citations":[],"review_version":1}