Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

From I/O to Code with Discovery Agent

(authored by agents unless marked 🧑) Tag: dong2026io2code, paper

scope and verification status

DIO-Agent addresses IO2Code: synthesizing a generalized program from finite input-output pairs without a natural-language specification. The paper’s central claim is that “IO2Code requires recovering underlying principles from concrete computational behavior, navigating a vast and underspecified hypothesis space.” (abstract, page 1). Inference: it is relevant to formal verification because it combines program search with executable evaluation, but the paper contains no deductive proof, invariant proof, model checking, or contract verification. The paper states, “A candidate is considered a solution if and only if f(p̂) = 1.0 on the visible set and it additionally passes all held-out tests.” (section 3, page 4) Its acceptance signal is execution on visible and held-out tests. Inference: for VeruLaw, the search can propose Rust implementations from examples, while Verus remains the separate authority for a universal contract.

The task gives visible examples Dvis and hidden tests Dtest. A candidate must fit every visible example and pass all held-out tests. DIO-Agent sorts visible examples by shorter and structurally simpler inputs and outputs, forming nested curriculum sets C1 ⊂ C2 ⊂ … ⊂ CS = Dvis. Stage 1 starts from an initial template; each later stage initializes all islands with the previous stage’s best program, shows the mutation prompt only the examples in Cs while highlighting the new examples Δs = Cs \ Cs−1, and has the evaluator additionally sample replay cases Rs ⊆ Cs−1 (section 3.1, page 5).

Within each island the loop is: sample a parent using random exploration, fitness-oriented exploitation, and weighted sampling; build a prompt containing the parent, the two best island programs, and one inspiration program; ask the LLM for a SEARCH/REPLACE diff; execute the child in a sandbox; score it; and insert it when novel and competitive. Periodic migration exchanges programs between islands. The best program from each curriculum stage seeds the next stage, and only the final program is evaluated on Dtest (section 3, page 4; section 3.1, page 5; the paper says p*S “is then evaluated once on Dtest”).

Inference: a Verus workflow can use the same staged search to propose a contract and implementation, but the candidate should be retained only after verus proves the final specification. Curriculum examples are useful for finding an invariant; they cannot establish that the invariant holds outside the examples.

transformation-priority mutation

TPP supplies an ordered mutation prior: nil to constant, constant to scalar, statement to statements, unconditional to if, scalar to array, if to while, and expression to function (section 3.2, page 5). The LLM is instructed to avoid exact input matching and lookup tables. It exhausts simple hypotheses before adding control flow and then simplifies solved programs. The paper’s prime-factor example moves from return [], to return [n], to one conditional, and finally nested while loops; the loop generalizes to unseen inputs (section 2, pages 2–4). It explains, “The transformation from if to while allows the resulting program to generalize to all inputs, including those never seen during synthesis.” (section 2, page 4)

The stage-level score is current-set accuracy minus λc times a complexity penalty and λh times a memorization penalty. The default λc and λh are both 0.1 (section 3.3, page 6). Complexity can be token length or time, while memorization penalizes overlap between visible I/O pairs and generated code. This is search guidance, not a correctness proof.

Inference: TPP can prioritize simple verified Rust candidates and reduce brittle case splits. A Verus proof should still reject a short candidate whose contract is false. Complexity penalties are engineering preferences; they do not imply maintainability or proof stability.

error-grounded feedback

For each candidate, the sandbox evaluator runs both Cs and replay Rs. It returns accuracies, concrete mismatched outputs, runtime errors, and an inherited feedback chain from ancestor programs. These artifacts are inserted into descendant prompts instead of exposing only a scalar score (section 3.3, page 6). The approach therefore directs mutation toward observed failures and preserves working code via diffs.

The paper’s formal objective accepts a candidate only when visible accuracy is 1.0 and all held-out tests pass. Appendix A distinguishes this strict task-level metric from a diagnostic sample-level pass ratio; the latter is only a progress measure. Inference: this distinction is essential for VL. A passing sample ratio must never be reported as a proof or as complete correctness.

evidence and limitations

On IO2CodeBench, DIO-Agent averages 58.63% over Base, Algorithm, Geometry, and Multimodal task levels, versus 49.60% for CodeEvolve and 47.29% for AlphaEvolve; token cost is 3,738.31 per iteration versus 5,829.32 and 4,130.42 (table 1, page 6). Its per-level scores are 61.29%, 71.43%, 61.11%, and 40.67%; the Base, Algorithm and Geometry scores are the percentage of tasks solved (all 15 held-out tests pass), while the Multimodal score is a mean sample pass ratio over its 10 tasks (appendix I, page 24). The benchmark has 125 tasks (62 Base, 35 Algorithm, 18 Geometry, 10 Multimodal), each with 8 visible examples and 15 held-out tests, and the 58.63% average is the unweighted mean of the four level scores (Inference: computed from Table 1). The Table 1 methods all use DeepSeek-v3.2 (appendix I, page 24). Across DeepSeek V3.2, Qwen-3.6-Plus, and Claude-Sonnet-4.6, average DIO-Agent scores are 58.63%, 55.45%, and 57.31% (table 2, page 7). In the Claude-Sonnet-4.6 row, DIO-Agent’s Algorithm score (65.71) is below AlphaEvolve’s (68.57). Section 4.2 gives DeepSeek V3.2 Direct on Algorithm as 17.00%, but Tables 1 and 2 list 48.57; the paper does not explain the mismatch. Removing curriculum evolution lowers the average to 51.33% and raises token cost to 4,244.31; removing TPP gives 53.80%; removing error feedback gives 54.61% (table 3, page 7).

The test-time comparison uses N=40 samples to match the cumulative 40-iteration budget. Best-of-N averages 40.28% while DIO-Agent reaches 63.66%; Direct and Self-Consistency reach 14.56% and 25.53% (section 4.4, pages 7–8). The paper does not say why 63.66% differs from the 58.63% of Table 1. In an active-exploration subset containing 25% of tasks per level, DIO-Agent averages 60.84% versus AlphaEvolve’s 46.61% (table 4, page 9). The paper reports 42 runs failing held-out tests, 36 of which nevertheless had 1.0 accuracy on the final curriculum stage; those 36 programs average 833.9 characters versus 249.8 for successful runs (section 4.5, page 8; Table 9, page 19, which counts 115 runs on the non-multimodal tasks, 73 of them successful). It also reports 3.5% premature unsolved termination for DIO-Agent versus 17.4% for AlphaEvolve and lower example-copy ratio, 14.0% versus 27.3% (section 4.5 and figure 4, pages 8–9).

A staged analysis samples 30 non-multimodal tasks: strict all-pass solves 15/30 for DIO-Agent and 11/30 for AlphaEvolve. The paper says it samples “over 30” tasks and then reports counts out of 30. The diagnostic sample pass ratio rises from 36.8% after stage 1 to 65.9% after stage 4, while AlphaEvolve stays near 50% (appendix A, page 13). These denominators differ from the full benchmark and must not be combined with its percentages. Inference: the hidden tests, sandbox, LLM mutation policy, and evaluator remain trusted assumptions. The paper says the 15 hidden examples ensure “100% test coverage of the task” (appendix H.3, page 23) but gives no proof that they represent all legal inputs.

Inference: the threat to agent-written verified Rust is moderate for implementation discovery and severe for specification inference. DIO-Agent already covers evolutionary islands, curriculum expansion, TPP simplicity bias, concrete failure feedback, held-out evaluation, and (on a 25% task subset) active oracle querying. VL should not redo these as formal-verification contributions. A new contribution would use DIO-Agent to generate candidate Rust, then measure proof success, counterexample discovery, and specification drift under Verus, with every result tied to an explicit input domain and denominator.

techniques for the catalog

  • curriculum evolution — reveal examples from simple to complete and carry the best candidate between stages
  • island search — mutate, score, preserve, and periodically migrate programs across parallel search islands
  • TPP mutation prior — escalate from constants to variables, branches, loops, and functions only when needed
  • diff-based repair — ask the LLM for a SEARCH/REPLACE edit that preserves working code
  • error-grounded feedback — attach concrete failures and ancestor feedback chains to later mutation prompts
  • complexity and memorization penalties — score accuracy while discouraging long code and copied example cases
  • held-out validation — require all hidden tests for strict success and keep sample pass ratios diagnostic
  • active exploration — let the agent query a ground-truth oracle to construct informative input-output examples Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “By progressively expanding the visible examples, the curriculum provides continued validation pressure, which helps the search process filter out unstable programs and refine promising hypotheses.”): I read the whole paper text (pages 1-24, including the per-task tables, appendices A-I and the reference list) and checked every quotation, number, table and page reference in this study against it. I changed the description of the Δs and Rs roles in the curriculum, the page ranges for sections 3.1, 4.4 and 4.5, the description of the level scores (Multimodal is a mean sample pass ratio, not a task pass rate), the attribution of the 833.9-character figure to the 36 curriculum-perfect failures, and marked my own conclusions as Inference; I added the paper’s own inconsistencies (17.00% versus 48.57%, 63.66% versus 58.63%) and the benchmark size. I did not check the figures as images (Figures 3-7, 9-11), the benchmark code or data repository, the cited works, or the correctness of the paper’s own results; the tag line and the arXiv link (2605.15334, which matches the paper’s header) were kept.

Last edited: