{"id":"0c0f8872-76fc-4f3d-aeed-d95a273f94f7","arxiv_id":"2607.04631","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":5,"one_line_summary":"A distributed LLM-worker system with entropy-maximizing self-improvement generates large verified-program datasets that train open models to match Claude Opus 4.5 on verification tasks.","lead":"Formal Disco is a multi-agent LLM system that generates large, diverse corpora of formally verified programs in Dafny, Verus, and Frama-C by initiating, repairing, and extending code under verifier feedback, guided by entropy maximization. The resulting synthetic data lets open models match or beat Claude Opus 4.5 on annotation and lemma-proving tasks, offering a scalable path past the data barrier in formal verification.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified; the weakest assumption is real but already bounded by the paper's own ablations and human-benchmark results.","rationale":"The reader's weakest_assumption correctly names the hand-chosen feature set and simple SFT recipe. Those are genuine limitations, but they are already stress-tested inside the paper: rarefaction curves, ablations of READMEs and docs, comparison to SAFE, and direct Pass@k on human benchmarks. Because the transfer claim is empirically supported rather than merely assumed, elevating the limitation into a reason to move the verdict from ACCEPT would over-weight an acknowledged soft spot that does not invalidate the reported results. Code and data are public, so independent re-runs are feasible. Verdict and confidence should remain as the reader stated.","tokens_in":34603,"tokens_out":534,"duration_ms":5012,"concrete_test":"Re-run the VerusBench annotation Pass@k evaluation of Section 4.3 after replacing the four entropy-maximization features with only the two unoptimized features that currently lag human data (annotation templates + language-feature usage); if Pass@1 falls below the SAFE baseline (40.9%) or the gap to Opus widens by more than 10 absolute points, the hand-chosen feature set is load-bearing for transfer. Otherwise the concern is non-critical.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim rests on the transfer story that entropy maximization over four hand-chosen features (annotations-per-method, lemma-body size, loop skeletons, method-body size) plus README/doc seeds yields synthetic programs useful for human-written verification tasks. That transfer is not guaranteed a priori: Section 5 and the rarefaction curves (Fig. 4) explicitly show that on unoptimized features (annotation templates) human DafnyBench remains more diverse, and the SFT recipe strips CoT. Nevertheless this is not a load-bearing failure of the argument. Downstream Pass@k on DafnyBench and VerusBench (Figs. 5–6) already measures transfer to human programs; the SAFE-matched Verus ablation shows FormalDisco data scales better with sampling budget; and the README/docs ablations (Fig. 7) quantify the external-entropy contribution. The paper therefore already supplies the evidence that would be needed to falsify the transfer claim, and that evidence supports rather than undermines it. No hidden inconsistency or untested premise remains that would overturn the strongest claim.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces FormalDisco, a distributed multi-agent system for open-ended synthetic generation of formally verified programs. Three LLM workers (Initiator, Fixer, Extender) collaborate via a shared agenda, seeded by random GitHub READMEs and language-reference snippets. The authors propose a maximum-entropy principle over program features and operationalize it via iterative supervised fine-tuning that retains only the top third of successful traces by minimum surprisal rank. They release large verified corpora in Dafny, Verus, and Frama-C (>100k programs), show that self-improved open models match or exceed the seed Claude workers on generation tasks while increasing feature entropy, and demonstrate that fine-tuning Qwen2.5-Coder-32B on data extracted from these corpora roughly doubles Pass@16 on DafnyBench annotation, matches Claude 4.5 Opus Pass@1 on VerusBench annotation, and yields large gains on Dafny lemma proving.","tokens_in":34980,"tokens_out":1183,"duration_ms":85285,"significance":"Data scarcity has long limited LLM progress on verification-aware languages. FormalDisco supplies a language-agnostic, verifier-grounded pipeline that produces large public datasets and open models competitive with a frontier system on several verification tasks. Strengths include: (i) an external, non-circular success signal from compilers/verifiers; (ii) held-out evaluation on human-written DafnyBench and VerusBench; (iii) rarefaction-curve comparisons and ablations of the multi-worker design, READMEs, and documentation snippets; (iv) released code and datasets. The entropy-maximization framing and the demonstration that self-training need not collapse diversity are methodologically useful beyond this domain. If the transfer results hold under broader scrutiny, the work offers a practical path for new formal languages to bootstrap AI assistance without decades of human corpora.","major_comments":[{"comment":"Abstract and §1 claim that fine-tuned models often match or exceed Claude Opus 4.5. On VerusBench annotation Pass@1 this is accurate (43% = 43%), and on DafnyBench annotation Pass@16 matches Opus Pass@1. On the lemma-proving task (§4.3, Fig. 6), however, Opus remains substantially stronger (61.6% vs 25.5% Pass@1). The fine-tuned models are also trained without chain-of-thought while the Opus baseline uses CoT. The claim should be scoped explicitly to the annotation tasks (or to Pass@k regimes) so that the abstract does not overstate the lemma-proving result.","section":null},{"comment":"§3.3 and §5: entropy maximization is performed over four hand-chosen features (annotations per method, lemma body size, loop skeletons, method body size). Rarefaction curves (Fig. 4) show that on unoptimized features—especially annotation templates—human DafnyBench remains more diverse. The paper already notes this limitation, but the central transfer story would be stronger with either (a) a sensitivity analysis over alternative feature sets or (b) an explicit argument why the four chosen features are the ones most relevant to the downstream annotation and lemma tasks. Without that, it remains possible that gains come mainly from scale and verifier filtering rather than from the entropy objective itself.","section":null}],"minor_comments":[{"comment":"Downstream evaluation (§4.3) covers Dafny and Verus only; Frama-C is used for generation and diversity analysis but not for task transfer. A short note on why Frama-C was omitted from SFT evaluation (or a small pilot) would round out the three-language claim.","section":null},{"comment":"Figure numbering in the manuscript dump is inconsistent: the main rarefaction panel is labeled Figure 4 in the text but later referred to as Figure 8; appendix rarefaction figures are also numbered 8–10. Please renumber for the camera-ready version.","section":null},{"comment":"Table 3 reports that Verus lemma-body median size decreases slightly under Qwen self-improvement (5 → 3) while p90 rises modestly. A one-sentence interpretation in §4.2 would help readers who might otherwise read this as partial diversity collapse on that feature.","section":null},{"comment":"The free parameters of the pipeline (msr top-1/3 fraction, max repair attempts = 3, K = 10k/30k, LoRA r=32) are listed in the appendix but not ablated. Even a brief statement that the top-1/3 threshold was not tuned on the downstream benchmarks would reassure readers about selection bias.","section":null},{"comment":"Related work on synthetic data for Lean/Isabelle (AlphaGeometry, DeepSeek-Prover, Goedel-Prover) is cited; a sentence contrasting open-ended joint generation of specs+impls+proofs with statement-conditioned proof search would sharpen the positioning.","section":null}],"recommendation":"minor_revision","confidential_remarks":"The work is solid and the release of three large verified corpora is a genuine community service. I lean accept-after-minor-revision rather than pure accept only because the abstract’s comparison to Claude Opus 4.5 needs tighter scoping; once that and the feature-selection discussion are clarified, the paper is ready. Fit for a top AI/ML venue is good; for a more formal-methods-centric journal the Frama-C evaluation gap would matter more."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This is the first language-agnostic open-ended generator that jointly produces specs, implementations, and proofs for auto-active verifiers, then turns the traces into public datasets and usable open models. That is the real contribution.\n\nWhat works: the initiator/fixer/extender agenda is simple and scales; README + doc-snippet seeds stop thematic collapse (their ablation is clean); entropy-ranked SFT keeps diversity rising instead of collapsing; and the downstream numbers are honest. Qwen-32B fine-tuned on their extracted diffs matches Claude Opus Pass@1 on VerusBench annotation and roughly doubles base Pass@16 on DafnyBench. They also beat the same pipeline run on SAFE as the sampling budget grows. Code, data, and rarefaction curves against SAFE/VeruSyn/DafnyBench are public. That is more than most synthetic-data papers deliver.\n\nSoft spots, in proportion: the four hand-chosen features are a design choice, not a theorem, and on unoptimized features (annotation templates) human DafnyBench still wins the rarefaction curves. The SFT recipe is deliberately dumb—no CoT—so the lemma-proving gap to Opus is expected and they say so. Neither undercuts the central claim that the corpora transfer to human benchmarks. Free parameters (top-1/3 msr filter, K, LoRA) are ordinary for this genre.\n\nWho it is for: anyone stuck on data scarcity in formal methods or AI-for-code, and anyone building multi-agent synthetic pipelines. It deserves a serious referee. I would bring it to reading group and I would cite the datasets and the worker design. Accept for peer review; the engineering and the released artifacts are the load-bearing parts and they hold.","headline":"Solid systems paper that actually ships the data and shows open models catching Claude on verification tasks; the entropy story is useful but secondary to the engineering.","tokens_in":35567,"tokens_out":453,"would_cite":true,"duration_ms":5851,"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":"Formal Disco uses LLM workers and entropy maximization to generate large synthetic corpora of verified programs, training open models that match frontier systems on verification tasks.","keywords":["formal verification","synthetic data generation","Dafny","Verus","Frama-C","entropy maximization","LLM agents","program synthesis"],"falsifier":"Fine-tune the same open model on a size-matched Formal Disco corpus versus a non-entropy-maximized or randomly varied synthetic corpus and check whether the entropy-maximized model fails to outperform the baseline on DafnyBench and VerusBench annotation and lemma-proving Pass@k.","tokens_in":35532,"feed_emoji":"🔐","tokens_out":948,"duration_ms":16707,"temperature":0.7,"pith_summary":"Formal verification gives the strongest correctness guarantees for code, but verification-aware languages have almost no public training data, so AI models cannot help write or prove them. This paper argues that the data barrier can be broken by open-ended synthetic generation: a distributed system of LLM workers that sketch programs from random open-source READMEs and language documentation, repair them under compiler and verifier feedback, and extend working programs into larger ones. A principle of maximum entropy over program features steers both the system design and iterative fine-tuning so that each round produces not only more successes but more diverse programs, avoiding the usual collapse of self-training. The released datasets in Dafny, Verus, and Frama-C contain over 100,000 verified programs; fine-tuning an open 32B coder on data extracted from them roughly doubles annotation success on human Dafny benchmarks and matches Claude 4.5 Opus Pass@1 on Verus annotation. If the approach holds, new formal languages need not wait decades for human corpora before AI assistance becomes useful.","feed_headline":"Synthetic verified programs train open models to match Claude","feed_subtitle":"Initiator, fixer, and extender agents plus entropy ranking yield Dafny, Verus, and Frama-C corpora that lift annotation performance.","key_machinery":"The principle of maximum entropy for synthetic program generation: Shannon entropy over discrete program features (annotations per method, lemma and method body sizes, loop skeletons) is maximized by ranking successful worker traces by minimum surprisal rank and fine-tuning only on the top third each iteration, so successive corpora grow both in success rate and in feature diversity.","core_discovery":"Coordinating three classes of LLM workers—initiators seeded by random READMEs and documentation snippets, fixers that patch verifier errors, and extenders that grow verified programs—together with iterative supervised fine-tuning that keeps only the most feature-surprising successful traces, yields large, increasingly diverse synthetic corpora of formally verified programs. Training open models on data extracted from those corpora produces substantial gains on human-written verification benchmarks, in places matching Claude 4.5 Opus.","pith_inferences":["The same initiator–fixer–extender loop with entropy ranking could generate training data for interactive theorem provers where human formalizations are scarce, not only for auto-active verifiers.","If hand-chosen features leave annotation-template diversity below human corpora, automatically searching for features that best predict downstream benchmark gains would further close the remaining gap.","Joint multi-language runs might transfer verification idioms across Dafny, Verus, and Frama-C rather than training each language in isolation."],"forward_implications":["New verification-aware languages can launch with large synthetic training sets instead of waiting for human corpora.","Open models can reach competitive verification performance without proprietary data or closed-model APIs at inference time.","Explicit entropy objectives over program features can counteract diversity collapse when models train on their own outputs.","Rarefaction curves of feature entropy become a practical way to compare heterogeneous program datasets beyond raw size.","The same agenda-and-worker architecture can be retargeted to other formal domains that have a machine-checkable correctness signal."],"fun_headline_variants":["Formal Disco agents create verified corpora lifting open models to Claude","Initiator-fixer-extender workers scale synthetic Dafny Verus Frama-C programs","Entropy ranking on agent traces yields diverse verified code matching Claude","Open models rival Claude after training on Formal Disco verified programs","Three LLM worker classes overcome data scarcity for formal verification"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"That maximizing entropy over a small hand-chosen set of program features, seeded by random READMEs and documentation, yields synthetic data diverse enough that fine-tuning on it improves models on real human-written verification tasks.","fun_headline_variants_meta":{"raw":{"variants":["Formal Disco agents create verified corpora lifting open models to Claude","Initiator-fixer-extender workers scale synthetic Dafny Verus Frama-C programs","Entropy ranking on agent traces yields diverse verified code matching Claude","Open models rival Claude after training on Formal Disco verified programs","Three LLM worker classes overcome data scarcity for formal verification"]},"model":"grok-4.5","effort":"low","cost_usd":0.003988,"raw_usage":{"total_tokens":1302,"prompt_tokens":860,"num_sources_used":0,"completion_tokens":72,"cost_in_usd_ticks":39880000,"prompt_tokens_details":{"text_tokens":860,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":370,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":860,"tokens_out":72,"duration_ms":4052,"temperature":1.0,"reasoning_tokens":370,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T16:06:26.010341+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Fine-tune the same open model on a size-matched Formal Disco corpus versus a non-entropy-maximized or randomly varied synthetic corpus and check whether the entropy-maximized model fails to outperform the baseline on DafnyBench and VerusBench annotation and lemma-proving Pass@k.","supporting_citations":[],"review_version":1}