LLM-Based FORM Code Generation with Verification-Driven Fine-Tuning

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

problem and contribution

The paper studies code generation for Form, a symbolic-algebra DSL used for very large particle-physics expressions. It reports that “contemporary large language models (LLMs), including frontier models with hundreds of billions of parameters, achieve a zero-percent execution pass rate on our instruction-following and tutorial-style Form tasks without documentation in a single attempt” (Abstract, unnumbered title page). Its central technique is to make the Form executable itself an oracle for producing training data, then fine-tune a small model. The paper says the pipeline “uses the Form binary itself as an execution oracle to produce and validate a corpus of 4,633 training examples” (Abstract, unnumbered title page).

technique: feature-stratified verified data generation

The method first defines “a taxonomy of 16 Form features, each with three complexity levels (basic, intermediate, advanced), yielding 48 feature-complexity cells” (Section 3.1, p.5). Features include wildcard matching, tensor and gamma traces, preprocessor loops, expression manipulation, and polynomial operations. For every cell, DeepSeek-V4 Flash (304B parameters, temperature 0.8) receives a plain-English instruction specifying symbols, expressions, and operations. The generation stage produces approximately 10,000 candidate programs (Section 3.1, p.5).

Each deterministic candidate passes four stated filters. (1) “Deterministic-word check: The instruction is scanned for non-deterministic words (“think”, “appropriate”, “suitable”) that could lead to variable outputs” (Section 3.1, p.5). (2) “Form binary syntax validation: The program is executed through the Form binary (FORM 5.0, April 2025)” (Section 3.1, p.5); failures are rejected and Form’s stdout error is fed to repair. (3) “Non-trivial output check: Programs that produce empty or trivially simple output (e.g., 0 or 1) are rejected” (Section 3.1, p.5). (4) An independent GLM-5.2 auditor (756B parameters, temperature 0.1) “evaluates whether the generated program is semantically consistent with the instruction” (Section 3.1, p.5). The auditor gets a curated Form factsheet. Exact-match and normalized-text deduplication follow the checks.

The resulting counts are 2,465 verified deterministic examples, 1,050 open-ended examples (63 of 1,113 held out for validation), 43 tutorial programs, and 1,075 knowledge Q&A examples, for 4,633 examples and a 314-example validation split (Section 3.1, pp.5–6). A documentation-in-context slice of 355 rows is included within these categories: the first 6,000 characters of a syntax guide are prepended to 10% of code rows. The paper states: “Test sets are generated before training data to prevent data leakage; we verify zero exact-match contamination between train and test instructions.” (Section 3.1, p.6).

Inference: in Verus, the executable oracle would be verus verification plus any separately justified runtime tests. A candidate should carry a specification (requires/ensures), loop invariants, and proof code; the pipeline must reject verification failures before training. A Form output check does not establish a Rust memory or specification property. The deterministic-word filter transfers as a prompt/data-quality rule, while the independent semantic audit remains an inference-layer check and must not be treated as proof.

technique: parameter-efficient specialization

The author fine-tunes Qwen3-8B with QLoRA: the base model is quantized to 4-bit precision, frozen, and trained with low-rank adapters. The paper states that this “reduces the number of trainable parameters by ∼99% while preserving performance comparable to full fine-tuning” (Section 2.3, p.4). The specialist is evaluated against seven open-weight baselines on four benchmarks: B1 has 664 fully specified deterministic tasks; B2 has 100 open-ended tasks; B3 has 44 tutorial tasks; B4 has 32 complex multi-step tasks (Section 4.1, pp.7–8).

The principal results are denominator-specific. FORM-8B obtains 97.7% exact-output match on all 664 B1 tasks and 83.0% execution on all 100 B2 tasks (Table 3, p.12). On the 89 adjudicable B2 tasks, strict Form-verified output match is 18.0% for FORM-8B versus 5.6% for the best frontier models (Table 3, p.12). These tasks have reference outputs, but many instructions do not uniquely determine them. The paper cautions: “part of its 18.0% vs. 5.6% lead over the best frontier model may reflect this familiarity rather than raw skill.” The familiarity refers to training data and B2 references generated by the same pipeline family (Section 5.3, p.14). Its paired tests give p = 0.007 against GLM-5.2 and GLM-5.3 on B2, while the reported leading-model comparisons on B3/B4 give p ≥ 0.375 (Section 5.3, p.15). General capability changes by −2.6 percentage points on MMLU, −1.5 on GSM8K, and −0.6 on HumanEval (Table 5, p.17).

technique: execution versus semantic success

The paper separates execution success from solutions with strict output matching: “Equality is verified by Form itself through a difference-to-zero check, Local Z = (ref) - (gen);”. It tries the reference and generated declaration sets in turn, requires every reference expression to be reproduced, and tolerates extra generated expressions. B2 excludes 11 references with no named result expression, leaving 89/100 tasks; B3 excludes three, leaving 41/44 (Section 5.3, p.13). B2 underspecification is a separate limitation of the retained tasks (Section 5.3, p.14). B4 retains 22/32 tasks because ten allow a freely chosen polynomial (Section 5.3, p.15). The paper reports confidence-interval half-widths up to ±20 percentage points and calls the small-set results “suggestive rather than significant” (Section 6.3, p.19). It states “We do not conduct a user study with physicists.” and “The evaluation benchmarks and the fine-tuned model were developed by the same author”. It measures correctness rather than runtime performance (Section 6.3, pp.19–20).

what is proved, measured, and trusted

Measured: candidate execution, exact output, strict output matching, bootstrap 95% intervals, paired McNemar tests, and capability preservation. The Form binary is trusted as syntax/output oracle; GLM-5.2’s semantic audit is an additional model judgment. The paper’s own limitations state that no physicist user study was done and that the benchmark/model were author-constructed (Section 6.3, pp.19–20).

techniques for the catalog

• verifier-oracle data curation — generate domain-code candidates and retain only programs passing syntax, execution, non-trivial-output, and independent consistency checks
• feature-complexity stratification — cover a DSL by feature × difficulty cells before generation
• execution-versus-output evaluation — report both runnable rate and strict expected-output match on adjudicable tasks
• parameter-efficient specialization — adapt a quantized frozen model with low-rank adapters while measuring held-out domain and general capability

Last edited: 2026-10-19