{"id":"e34a6925-03b8-4297-bc59-18a25690fff2","arxiv_id":"2607.23425","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":4,"one_line_summary":"An exact model-checker oracle for NL-to-TLA+ still yields an elevenfold “correctness envelope” (18.7%–1.7%) once interface supply and vacuity screens are made explicit.","lead":"TLA+-Bench grades LLM-written TLA+ specs by running the real model checker, not by parse rate or text similarity. The headline result is that even an exact oracle still leaves grading choices that swing the reported correct rate elevenfold, from 18.7% down to 1.7%.","discovery_kind":"new_method","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"The envelope's floor (1.7% mutation-surviving, hence the \"elevenfold\" headline) is set largely by scoring convention, not by measured vacuity: 12 of 30 passes are declared non-surviving untested because their configs name temporal properties, and only 5 of the 18 actually-tested passes survive.","rationale":"I verified the internal arithmetic of the envelope before attacking it, and it reconciles: default 30/300 (Table A4: 4+10+16), substantive 12/300, mutation 5/300, config-aware 56/300 (Table A7: 26+19+11), difficulty cliff 26/105→2/102→2/93. The pipeline is unusually transparent — outputs released, counts recomputed from released data, conventions disclosed. So this is not an inconsistency complaint. My concern is that the headline's most quoted numbers (1.7%, elevenfold) sit on the envelope's weakest-constructed bound: a floor where 12 of 30 passes are classified by test inapplicability rather than by any vacuity evidence, on top of an n=5 survivor count. The reader identified the property-scoped oracle as the weakest assumption; my concern is adjacent but distinct — it is about how the paper's own lower bound is manufactured within that oracle, not about whether the oracle is the right operationalization. Hence \"partial\" agreement. I do not move the verdict off CONDITIONAL: the paper hedges the bound explicitly (\"conservative lower bound\"), releases everything needed to run my proposed check without re-querying models, and the central methodological claim (unstated grading choices move measured correctness by a large factor) is robust to any plausible reclassification — even a fully charitable floor of 17/300 still leaves a fourfold-plus range. The appropriate response is a restatement of the headline ratio as convention-sensitive, plus running the temporal-vacuity check on the 12 untested passes, both of which fit within the existing CONDITIONAL framing rather than warranting REJECT or a stronger verdict.","tokens_in":24246,"tokens_out":3254,"duration_ms":104866,"concrete_test":"For the 12 temporal-only passes scored non-surviving in §8.7, run an actual temporal vacuity check from the released outputs: e.g., for each, ask TLC whether the property's enabling condition is ever reached (model-check the negated antecedent or a weakened/antecedent-TRUE variant of the formula, per Beer et al. [4] cited by the paper), classifying each pass as vacuous or load-bearing. Recompute the envelope floor as (5 + non-vacuous-of-12)/300. If the floor rises above ~2.5%, the \"elevenfold\" headline should be restated as a range-of-ranges. Simultaneously, for the 5 surviving safety-invariant passes, inspect the mutated run logs to confirm each failure is attributable to the mutated invariant's removal rather than an unrelated deadlock or secondary temporal check.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest claim's quantitative punch — \"correct rate moves elevenfold, 18.7% to 1.7%\" — rests on the mutation-surviving bound of §8.7. That bound is computed as follows: of the 30 default-regime passes, 12 check a temporal property with no mutable safety invariant and are \"scored as non-surviving on that ground,\" i.e., counted as vacuous-adjacent without any test being run on them. The mutation test only acts on the remaining 18, of which 5 survive. So the 1.7% floor is really \"5 of 300 demonstrably load-bearing,\" while the true floor lies somewhere in [5/300, 17/300] depending on how many of the 12 untested temporal passes are genuinely constraining. If, say, half of those 12 are non-vacuous, the floor is ~3.7% and the headline range shrinks from elevenfold to roughly fivefold. The paper does disclose this (\"the test is a lower bound\"), and the qualitative claim — grading choices move the number a lot — survives any reclassification. But the abstract and §8.2 present 1.7% and \"elevenfold\" as measured envelope bounds, when the lower bound is 40% convention (12 of 30 passes classified by inapplicability rather than evidence) and the survivor count itself is n=5, so a handful of reclassifications move the headline ratio materially. A secondary murkiness: the stated survival criterion — \"a pass survives when the mutated run still fails\" after replacing every checked safety invariant with TRUE — is under-specified for multi-property configurations (a mutated run can only fail via deadlock or a temporal check, which does not by itself show the mutated invariant was load-bearing). The released code presumably fixes this, but the paper's description does not let the reader verify that the 5 survivors fail for the right reason. This is distinct from the reader's flagged concern (property-scoped oracle vs. behavioral equivalence): even accepting the property-scoped oracle, the lower envelope bound's construction overstates how much of the range is empirically measured.","agreement_with_reader":"partial"},"referee_report":{"model":"moonshotai/kimi-k3","summary":"The paper introduces TLA+-Bench, a corpus of 1,300 TLA+ specifications (403 model-checked gold, 897 parse-only silver) from 13 public repositories, each with four model-written descriptions (two styles × two providers), difficulty labels, and runnable TLC configurations for the gold tier. Six LLMs are evaluated on a 100-specification evaluation set (gold system category minus 46 flagged trivial fixtures), graded by SANY parse plus TLC model check against the fixed reference configuration. The central claim is the \"correctness envelope\": on one fixed set of 300 frontier-model outputs, the pooled correct rate moves sixfold under grading-only changes (10.0% default → 4.0% substantive → 1.7% mutation-surviving), and elevenfold (18.7% → 1.7%) when the configuration-aware regime, a separate generation set with interface names supplied, is included. Within the envelope: all models are far more often valid than correct, open models score ≤1% correct, and correctness collapses from 25% (basic) to 2% (intermediate/advanced). Configuration-binding dominates the checker-grounded failure taxonomy. The paper is notably transparent about scope limits: property-scoped oracle, single sample per spec, non-uniform decoding, non-blind author-team audits.","tokens_in":24703,"tokens_out":4050,"duration_ms":136819,"significance":"If the numbers hold, this is a useful datasets-and-benchmarks contribution with an unusual degree of methodological self-awareness. Strengths worth naming: every gold reference is SANY+TLC validated before inclusion; the grader is frozen and deterministic with a stated tie-break; model outputs are released so the default/substantive/mutation rows of Table 5 can be recomputed without re-querying any model; the configuration-aware bound is generated from released runnable configurations; trivial fixtures are flagged rather than silently dropped; and failure categories come from checker output, not inferred labels. The correctness-envelope framing — that an exact oracle yields a range of defensible rates, not one number — is a genuinely transferable point for execution-graded benchmarks. The internal findings (valid ≫ correct; difficulty cliff backed by κ≈0.8 IAA plus a construct-derived robustness check) are stable and appropriately hedged for n=100.","major_comments":[{"comment":"The envelope floor of 1.7% (5/300) is constructed by counting 12 of the 30 default-regime passes as non-surviving without any test, because their configurations name temporal properties with no mutable safety invariant. Only 18 passes were actually mutated, of which 5 survive. The true mutation floor therefore lies in [5/300, 17/300] = [1.7%, 5.7%], and if half the untested temporal passes are non-vacuous the headline range shrinks from elevenfold to roughly fivefold. §8.7 does disclose this ('scored against the rate rather than excluded... a conservative lower bound'), but the abstract, §1 contribution ❹, and Table 5 present 1.7% and 'elevenfold' as measured bounds on the same footing as the other rows. Request: add an upper-bound row or explicit range to Table 5, hedge the abstract/intro phrasing, or extend the probe to temporal properties so the floor is measured rather than assigned","section":"§8.7 / §8.2 / Abstract"},{"comment":"The survival criterion — 'replace every checked safety invariant named by the configuration with TRUE and re-run TLC; a pass survives when the mutated run still fails' — is under-specified for multi-property configurations. When a configuration names several invariants plus a temporal property, mutating all invariants at once means the mutated run can still fail only via another property (e.g., the temporal one), so 'survival' re-tests that property rather than establishing that the mutated invariant was load-bearing. Please state whether mutation is joint or per-invariant, and which property's failure counts as survival; per-invariant single mutations would give a cleaner attribution and are cheap at n=18.","section":"§8.7"}],"minor_comments":[{"comment":"Table 2 legend renders as glyph soup ('/check-circleYes,/adjus◎Partial,/times-circleNo'); check the macro definitions before camera-ready.","section":"Table 2"},{"comment":"§5 says the mutation bound 'acts on the safety-invariant subset of these 291', while §8.7 says temporal-only passes are counted as non-surviving rather than excluded. These phrasings describe the same rule differently; align them.","section":"§5 vs §8.7"},{"comment":"The substantive and mutation rows reclassify the same 30 passes, so the envelope rates are paired, not independent. A paired (McNemar-style) comparison would be more informative than the per-row binomial intervals quoted in §8.3/§9, particularly for the 4.0% vs 1.7% gap (12 vs 5 passes).","section":"§8.2 / Table 5"},{"comment":"Table 6 reports only percentages; the underlying counts (4, 10, 16 correct) appear only in Table A4. Add counts to Table 6 or cross-reference, since small-count rows (e.g., GPT-5 4%) deserve visible denominators.","section":"Table 6"},{"comment":"Appendix A11 discloses that the exact GPT-5 description prompts were not recorded and are reconstructed. Since GPT-5 declarative descriptions are the evaluation input, consider archiving the release scripts' prompt templates verbatim going forward; the archived descriptions themselves make the current evaluation reproducible, so this is process feedback only.","section":"Appendix A11"}],"recommendation":"minor_revision","confidential_remarks":"FormalLM [5] is the authors' own prior benchmark; the manuscript states the delta explicitly and does not lean on the overlap, which I take to be handled appropriately. Both annotation studies (faithfulness, difficulty) use author-team annotators and are non-blind; this is disclosed in both places and in the ethics statement, but the editor may want to note that neither audit is independent of authorship. Fit with the datasets-and-benchmarks track is good."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing worth knowing is the correctness envelope. On one fixed set of 300 frontier outputs they show that unstated grading choices (interface supply, behavioral screen, vacuity screen) move the pooled correct rate from 18.7% down to 1.7%. That is the paper’s actual result, and it is transferable beyond TLA+. Inside the envelope the findings are stable and unsurprising: parse >> correct, open models near floor, sharp difficulty cliff.\n\nWhat is new is the resource plus the measurement. First large NL-to-TLA+ set graded by full-state-space TLC rather than parse or resemblance; 403 gold + 897 silver from 13 repos; subsumes FormalLM; ships dual styles/providers, difficulty/category labels, fixture flags, checker-grounded failure taxonomy, and the released outputs so the default/substantive/mutation rows recomputed without re-querying. Construction is audited, gold refs are SANY+TLC validated, IAA on difficulty is κ≈0.8 with a construct-derived robustness check, and circularity is low—third-party specs, fixed configs, external oracle. Reproducibility artifacts are strong.\n\nSoft spots in proportion. The stress-test note is right on the numbers: of the 30 default passes, 12 temporal-only are scored non-surviving by inapplicability, not by a run, so the 1.7% floor and the “elevenfold” headline are partly convention. The paper does say “lower bound,” and the qualitative claim (grading choices move the number a lot; sixfold on fixed outputs alone) survives any reasonable reclassification of those 12. Still, the abstract sells 1.7% harder than the method section supports. Second, the oracle is property-scoped and harness-coupled, not behavioral equivalence—they state this clearly and leave reference-varying gates to future work. Third, descriptions are model-written (faithfulness audit is decent but not blind), and the intent style plus second provider are shipped unexercised, so capability claims stay envelope-relative. Model rankings are n=100, one sample, mixed decoding—indicative only, which they mostly treat as such.\n\nThis is for people who build or consume execution-graded benchmarks for code/spec generation, and for anyone tired of single silent pass rates. It deserves a serious referee. I would engage, cite the envelope framing and the resource, and bring it to reading group. Not a takedown candidate; a careful datasets paper with one over-sharp headline number.","headline":"Real methodological contribution on how exact oracles still leave a wide correctness range; the 1.7%/elevenfold floor is partly scoring convention, but the qualitative claim and the resource hold up.","tokens_in":25925,"tokens_out":627,"would_cite":true,"duration_ms":20051,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"An exact model-checker oracle for natural-language to TLA+ generation does not yield one correctness number but a range spanning elevenfold, from 18.7% down to 1.7%.","keywords":["benchmark","dataset","formal specification","TLA+","model checking","large language models","execution-grounded evaluation","code generation"],"falsifier":"Re-grade the released 300 frontier outputs under a reference-varying behavioral gate (perturb the gold properties or constants and demand the checker detect the change); if the envelope collapses to a single stable rate near the default figure, the measurement claim fails.","tokens_in":25553,"feed_emoji":"📐","tokens_out":915,"duration_ms":17139,"temperature":0.7,"pith_summary":"Large language models are being asked to write TLA+ formal specifications from plain-language descriptions, but prior benchmarks score them by surface resemblance or by whether the output merely parses. This paper releases TLA+-Bench: hundreds of real specifications paired with runnable model-checking configurations so that a generated module is graded by walking its full reachable state space. The central result is about measurement itself. On one fixed set of model outputs, the three grading choices earlier work leaves unstated move the pooled correct rate sixfold; telling the model the interface names widens the span to elevenfold. Inside that range the picture is stable: every model produces valid TLA+ far more often than correct TLA+, open models stay near zero, and correctness collapses once problems leave the easiest tier.","feed_headline":"Exact oracle, elevenfold swing in “correct” TLA+","feed_subtitle":"Same model outputs score 18.7% or 1.7% once grading choices left silent by prior benches are made explicit.","key_machinery":"The correctness envelope: the measured span of defensible correct rates obtained by making explicit the interface-supply choice and the two vacuity screens (substantive multi-state behavioral pass; mutation of named safety invariants to TRUE) that prior single-number benchmarks leave silent.","core_discovery":"An exact oracle does not settle correctness on its own. The same frontier-model outputs admit a correctness envelope from 18.7% (interface names supplied) through 10.0% (default recovery) and 4.0% (behavior must be exercised) down to 1.7% (named property must be load-bearing). Inside the envelope every model is far better at valid than correct TLA+: the strongest reaches 16% by default and 26% with names given, open models at most 1%, and correctness falls from roughly 25% on basic specs to 2% on harder ones.","pith_inferences":["The same three silent choices (which instances count, how much interface must be recovered, whether a pass must check anything) likely inflate reported rates in NL-to-SQL and code-generation benches that use fixed harnesses.","Configuration-binding as the dominant failure mode suggests future generators may gain more from interface-aligned decoding or two-stage name binding than from raw scale alone.","Shipping paired name-revealing and name-hidden descriptions turns identifier leakage into a controllable experimental axis for any public-code corpus evaluation."],"forward_implications":["A parse-only or resemblance-only benchmark for NL-to-TLA+ will badly overstate capability relative to full-state-space checking.","Resource builders who grade executable artifacts should report a range over interface and vacuity choices rather than one silent number.","Frontier models still top out near 26% even when interface names are handed to them, so interface recovery is only part of the gap.","Difficulty stratification is essential: pooled rates hide a cliff from basic to intermediate/advanced specs.","The released gold configurations, fixture flags, and model outputs let others recompute every envelope bound without re-querying models."],"fun_headline_variants":["Exact oracle swings TLA+ correctness elevenfold","Same outputs: 18.7% to 1.7% correct TLA+","Correctness envelope exposes grading gaps in TLA+","Valid TLA+ far outruns correct: 26% peak with names","TLA+-Bench: difficulty drops correct specs to 2%"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"That satisfying the properties named by a fixed reference configuration the model did not write is the right operational meaning of “correct” for this generation task.","fun_headline_variants_meta":{"raw":{"variants":["Exact oracle swings TLA+ correctness elevenfold","Same outputs: 18.7% to 1.7% correct TLA+","Correctness envelope exposes grading gaps in TLA+","Valid TLA+ far outruns correct: 26% peak with names","TLA+-Bench: difficulty drops correct specs to 2%"]},"model":"grok-4.5","effort":"low","cost_usd":0.004945,"raw_usage":{"total_tokens":1508,"prompt_tokens":917,"num_sources_used":0,"completion_tokens":74,"cost_in_usd_ticks":49448000,"prompt_tokens_details":{"text_tokens":917,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":517,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":917,"tokens_out":74,"duration_ms":7684,"temperature":1.0,"reasoning_tokens":517,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T22:34:21.410999+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Re-grade the released 300 frontier outputs under a reference-varying behavioral gate (perturb the gold properties or constants and demand the checker detect the change); if the envelope collapses to a single stable rate near the default figure, the measurement claim fails.","supporting_citations":[],"review_version":1}