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

Law And Order: Tax Law Autoformalization

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

system and result

LAW&ORDER translates tax forms and instructions into executable symbolic programs, verifies intermediate cell outputs on repair cases, and repeatedly repairs only functions whose outputs disagree. The abstract reports 100% cell-level and form-level accuracy on 51 held-out TaxCalcBench returns, while the strongest LLM alone reaches 66% accuracy. The paper’s key design is structural correspondence (cells, schedules, dependencies align with functions) plus denotational correspondence (functions implement prescribed computations). Its stated objective is “to synthesize a symbolic program that exactly reproduces the computations specified by a tax form and its accompanying instructions.” (Section 3, p. 4.)

Inference: this is directly relevant to VL because a Verus project can align each source rule and intermediate state with a Rust function and contract, then use localized counterexamples to repair one obligation. Finite tests are evidence of behavior on tested inputs, while Verus proofs can extend evidence to all inputs covered by a specification.

technique 1: extract structure and generate a computational skeleton

The pipeline first applies a regex algorithm to tax-form PDFs, extracting computationally relevant cells and definitions. Each cell becomes a function. The authors manually audited federal and state forms and report no observed extraction errors (Section 3.1, p. 4). For every extracted cell, they generate an empty function specification: only the interface exists, and implementation logic is omitted (Section 3.2, p. 4). A cell c_i has a value type in integers, reals, or booleans and a function f_i : X_i → C_i, where X_i contains referenced inputs. The signatures form the tax form’s computational skeleton independently of implementation language.

Inference: VL can parse Rust APIs, source specifications, and requirements into a graph of functions, inputs, postconditions, and dependencies before asking a model to fill proof bodies. Keep interfaces stable during repair so a failed proof points to a local implementation or lemma. Extraction itself needs review because a parser can omit a source obligation.

technique 2: instruction-grounded synthesis

For each function signature, the LLM receives the tax form, official instruction text, and signature, then writes executable symbolic logic implementing that instruction (Section 3.3, p. 4). The authors treat instructions as the authoritative semantic source because they are operational and require less legal interpretation than statutes or regulations. The generated artifact can be Lean, C++, Python, Epilogue, or another deterministic language.

Inference: a VL generator should receive the natural-language requirement, Rust signature, requires/ensures contract, and dependency summaries. Source text should remain linked to every generated function. The model’s output must be compiled and verified; textual alignment alone is insufficient.

technique 3: repair-set-assisted verification and localized correction

Repair cases contain inputs and expected outputs for every cell. The system executes the generated dependency graph, compares each cell output with its expected value, and identifies the first or affected function. That function is regenerated with its form and instruction context. Validation repeats until every cell agrees on every repair case. Algorithm 1 states the loop: execute all functions on all (I^(k), G^(k)); for each mismatch, set f_j ← LLMCorrect(f_j, {x_j^(k)}, I_j); stop when all outputs equal gold outputs. The paper explains, “When a discrepancy is identified, the function corresponding to the affected cell is regenerated by prompting the LLM with the relevant tax form and instruction context to correct the implementation.” (Section 3.4, p. 5.)

Inference: a VL repair loop can run Verus, collect the failing obligation and counterexample, and ask an agent to revise only the implicated function, invariant, or lemma. Preserve passing proof artifacts and rerun the full dependency chain after each local repair. A compiler diagnostic is stronger than an output mismatch, but both support localization.

The paper distinguishes finite behavioral agreement from universal equivalence: “Agreement on a finite benchmark establishes cell-level behavioral agreement on the repair set examples rather than universal semantic equivalence over all possible taxpayer inputs.” (Section 3.4, p. 5.) Inference: VL should state this same boundary for test-based checks and separately report Verus’s quantified proof obligations.

technique 4: separate repair and held-out evaluation

The repair set comes from OpenTaxSolver human-written returns. After synthesis and repair, the program is frozen and evaluated on independently authored TaxCalcBench returns written by CPAs and never exposed during generation or repair (Section 1, p. 2; Section 4.1, p. 5). TaxCalcBench has 51 cases. Cell accuracy is correctly computed cells divided by total evaluated cells; form-level accuracy requires every cell in a return to match (Section 4.2, p. 6).

Table 2 shows GPT-5.5 Medium LAW&ORDER at 95.0% strict return accuracy and 99.3% cell accuracy; direct translation is 17.5% and 73.3%, and self-debugging is 37.5% and 75.0%. GPT-6 LAW&ORDER reaches 100.0% for both. These percentages use the 51-return held-out set described in the setup; the paper does not provide per-model denominators beyond that shared test set.

Inference: a VL evaluation must keep proof-repair examples separate from final unseen workloads, and report both obligation-level and whole-function success. Held-out tests should include changed dependency paths and adversarial boundary values.

technique 5: semantic equivalence and counterexamples

The authors sample 50 cells and ask Claude Code to prove equivalence between Claude Opus implementations and gold implementations or find divergent inputs. Equivalence is proved for 43/50. Seven have counterexamples; six expose errors in generated code and one exposes an error in the gold implementation (Section 4.4, p. 8). The denominator is the 50 uniformly sampled cells. This check demonstrates that execution agreement does not guarantee semantic equivalence and that formal comparison can uncover specification errors.

Inference: in VL, use Verus lemmas to prove equivalence between a repaired implementation and a reference specification where feasible. If equivalence is unproved, search for a counterexample and record whether the reference or generated code is wrong. This is a verification artifact, not merely a pass/fail score.

technique 6: coverage and dependency depth diagnostics

The benchmark contains 1,847 cells across 26 forms; 1,021 are raw inputs at depth zero, and dependency depth reaches 30 (Section 5.1, p. 8). For TY2024, repair cases with at most two inputs per form achieve 94.6% cell and 44.0% branch coverage; 51 held-out inputs achieve 98.6% cell and 73.1% branch coverage. For TY2025, repair coverage is 93.3%/44.0% and test coverage 93%/73% (Section 5.3, p. 9). The paper reports that errors concentrate in longer calculation chains and that localized repair is more stable than global self-debugging.

Inference: VL should record dependency depth, branch coverage, and which proof obligations each test exercises. A small repair suite can miss branches even when it touches most functions. Long chains deserve compositional lemmas and intermediate assertions.

what is proved, measured, and trusted

The system measures exact output agreement, repair convergence, coverage, and sampled equivalence/counterexamples. It does not prove that every generated program follows the complete tax law, and the authors note that tax forms have less legal authority than statutes or regulations (Section 1, p. 2). Human extraction audits and CPA-written cases are trusted inputs to the evaluation. The single gold implementation error found in the equivalence sample shows that expected outputs can be wrong.

Inference: for VL, trusted components include the Verus checker, Rust compiler, formal specifications, and explicitly accepted library assumptions. Tests, model-generated repairs, source extraction, and gold traces remain fallible. The product threat is a coherent but wrong source specification: localized repair can make every test pass while preserving the wrong rule. Specification review and independent reference models are required.

what VL should reuse and avoid repeating

Inference: the paper already establishes structure extraction, per-function skeletons, instruction-grounded synthesis, localized repair, held-out evaluation, coverage diagnostics, and equivalence/counterexample checks. VL should adapt these to Rust and Verus, measure proof and repair cost, and avoid claiming the generate–execute–repair loop itself as novel.

techniques for the catalog

  • structural correspondence: map source cells or rules and dependency edges to executable functions
  • instruction-grounded synthesis: generate each function from authoritative natural-language instructions plus its interface
  • localized repair: regenerate only the function whose intermediate output or proof obligation fails
  • repair/test split: tune on human-written cases and evaluate once on independent held-out cases
  • equivalence checking: prove sampled implementations equivalent or produce concrete divergence inputs
  • coverage/depth diagnostics: measure cell and branch coverage and prioritize long dependency chains Checked 2026-10-15 against paper han2026law: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: