Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

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

technique: counterexample-guided LRM synthesis

What it is. The method prompts a large reasoning model (LRM) to emit a register-transfer-level Verilog module from a TLSF temporal specification, then checks the module with a sound model checker. If the module violates the specification, the checker returns a counterexample trace; the next LRM call receives that trace and repairs the module. The paper summarizes this as “a guess-and-check loop: Neural models generate a candidate design, which is subsequently verified by a symbolic model-checking procedure, i.e., an exhaustive verification algorithm that returns a counterexample if the design does not satisfy the specification” (section 1, page 2).

When to use it. Use it for reactive hardware specifications in TLSF/LTL when direct symbolic synthesis is expensive or fails, and when a candidate can be represented in Verilog and model-checked. The approach handles both realizable specifications, where the goal is a satisfying module, and unrealizable specifications, where the model is instructed to produce an environment strategy showing unrealizability (section 3.2, page 4).

How to apply it. (1) Remove benchmark comments, names, and descriptions so the model cannot use hints about realizability (section 3.1, page 4). (2) Prompt the LRM with the TLSF directly instead of first compiling to automata; request a Verilog module with fixed clock and extraction format constraints (section 3.2, page 4; appendix A.1). (3) Translate Verilog to AIGER with Yosys, then to nuXmv input with aigtosmv (section 3.2, page 4). (4) Run nuXmv’s IC3 routine with a 32 GB memory limit and 600-second timeout (section 3.2, page 4). (5) If verified, retain the module. Otherwise, pass the counterexample and an explicit repair instruction back to the LRM and iterate (figure 2 and section 3.2, page 4). The paper also decomposes the specification into sub-specifications to make checking manageable and feedback fine-grained (section 3.2, page 4).

Evidence. The evaluation used all 1,586 SYNTCOMP 2025 LTL-track specifications. Of these, metadata identified 458 realizable and 419 unrealizable; the rest had unknown status (section 3.1, page 4). With two CEX iterations, Gemini 3.1 Pro solved 1,355/1,586 and GPT-5.5 solved 1,467/1,586; the symbolic baselines ltlsynt and SemML solved 1,297/1,586 and 1,295/1,586 (table 1, page 5). Gemini improved from 1,193 with zero iterations to 1,355 with two, while GPT-5.5 improved from 1,392 to 1,467 (table 1, page 5). The authors report that GPT-5.5’s 1,392 solved instances split into 640 realizable and 752 unrealizable (section 3.3, page 5). An ablation found that no reasoning tokens reduced GPT-5.5 to 123 solved instances; solved counts rose with larger reasoning budgets, with diminishing returns on a log-linear trend (section 3.3, page 5).

Verus form. Inference: the same loop maps to Rust/Verus as: generate Rust plus requires/ensures, run Verus, feed the first failing verification diagnostic or counterexample abstraction to the model, and repair. Verus proof failures are not temporal-model-checker traces, so the feedback must include the failing obligation and relevant state assumptions. Inference: for concurrent Rust, a state-machine model and invariants would be required; the paper’s Verilog semantics and nuXmv checks do not establish Rust memory or concurrency correctness.

technique: parameterized synthesis by bounded instantiation

What it is. Parameterized synthesis asks for one implementation template that works for arbitrary process counts, an undecidable problem for LTL. The LRM emits Verilog with a parameter declaration. Because parameterized verification is also undecidable, the authors instantiate the module at finite parameter values and model-check each instance (section 4, page 6).

How to apply it. (1) Identify specifications equivalent up to parameter value; the authors derived 57 general parameterized specifications from SYNTCOMP (section 4.1, page 6). (2) Prompt the model to add a parameter declaration in the module header (section 4.2, page 6). (3) Instantiate the generated module and specification at each parameter value up to the largest value represented in the competition class. (4) Run the same model-checking pipeline. (5) If any instance fails, return its sound counterexample for repair. If all tested values pass, retain the result only as bounded evidence: “we can no longer guarantee correctness in the positive case” (section 4.2, page 6).

Evidence. Across three runs, Gemini solved 35.0 ± 1.0 / 57 without feedback and 38.3 ± 1.1 / 57 with counterexample guidance; GPT-5.5 solved 35.7 ± 2.5 / 57 both with and without guidance (table 2, page 6). The denominator is the 57 parameterized specifications, and ± is the reported standard deviation across runs. Inference: this is testing, not a proof for arbitrary parameter values.

technique: natural-language synthesis and inspectable autoformalization

What it is. The authors hand-authored 57 natural-language descriptions (NATURAL) for the parameterized specifications and compare two routes: NL → TLSF autoformalization → LRM Verilog synthesis, and direct NL → Verilog synthesis. Both generated modules are checked against the manually crafted ground-truth TLSF and, where available, the autoformalized TLSF (figure 4 and section 5, pages 7–8).

How to apply it. For the autoformalization route, prompt the LRM with the full TLSF grammar, parameterized-signal conventions, and LTL operators. The paper says: “Autoformalization is a challenging task, we find that the LRM cannot always produce a syntactically correct TLSF specification within three attempts” (section 5.2, page 8). Run syntax feedback for up to three attempts. Check formal-spec equivalence with Spot’s ltlfilt; then synthesize Verilog, checking against both autoformalized and ground-truth specifications (section 5.2, page 8). The paper deliberately uses the first-try autoformalization for synthesis even if syntactically broken, because syntax repair can shift semantics; repaired versions are used for later checking when syntax is required (section 5.2, page 8). For the direct route, prompt the LRM with NL and verify the resulting Verilog against both specifications.

Evidence. The autoformalizer produced syntactically invalid TLSF after three attempts for 12.7 ± 0.5 / 57; Spot proved 9.3 ± 0.6 / 57 equivalent and 8.7 ± 0.6 / 57 inequivalent, while 26.3 ± 0.9 / 57 equivalence checks timed out after 30 minutes and 32 GB per specification (section 5.2, page 8). Via autoformalization, 30.0 ± 0.0 / 57 modules satisfied ground truth and 33.7 ± 1.7 / 57 satisfied the autoformalized specification; 25.7 ± 0.6 / 57 satisfied both. Direct synthesis satisfied ground truth for 31.7 ± 1.2 / 57 and autoformalized specs for 30.7 ± 1.9 / 57 (table 3, page 8). These fractions are means over three Gemini 3.1 Pro runs at high reasoning.

Verus form. Inference: a Rust workflow can expose an intermediate specification for review, then synthesize or repair code against that contract. Verify generated Rust with Verus and separately compare the natural-language requirement to the contract using a structured judge or reviewed translation. A Verus proof of the generated function establishes the contract, not the natural-language intent, so the paper’s dual-check idea transfers directly.

what is proved, trusted, and limited

A successful nuXmv check proves the finite Verilog instance satisfies the supplied TLSF specification. It does not prove the natural-language description was translated correctly, and bounded parameter checks do not prove arbitrary parameters. The LRM, prompts, TLSF grammar, Yosys/AIGER translation, nuXmv/IC3 implementation, and hand-authored ground truth remain trusted. The authors note that inequivalence to ground truth can reflect ambiguity or underspecification rather than an incorrect formalization (section 5.2, page 8). Inference: for agent-written verified Rust, the threat is high at the requirement-to-contract boundary and moderate inside a reviewed contract, because model checking or Verus can certify only the supplied formal statement.

Existing work already covers symbolic synthesis baselines, LRM synthesis with feedback, and natural-language temporal-logic translation; VL should not redo a generic “LLM plus checker” claim. The useful transferable design is a bounded repair loop with sound diagnostics, explicit dual checking against an independently authored specification, and reporting of timeout and denominator details. The paper concludes that “These promising observations motivate concrete next steps: creating new synthesis benchmarks based on natural-language hardware specifications” (section 7, page 9).

techniques for the catalog

• CEX-LRM loop: generate Verilog, model-check it, and repair from sound counterexample traces
• specification decomposition: split temporal requirements to produce manageable, localized checker feedback
• parameterized bounded synthesis: test one parameterized implementation across finite instantiations and mark positive results non-proof
• inspectable autoformalization: expose NL-to-TLSF output for review before synthesis
• dual specification checking: verify generated code against both autoformalized and independently authored ground truth
• syntax-feedback repair: iterate formal-spec generation with grammar diagnostics while monitoring semantic shifts

Checked 2026-10-15 against the paper by a Codex agent for natural_synthesis_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15