PaperlayerView exact revision on arXiv

Source-linked AI summary

Law And Order: Tax Law Autoformalization

Sophia Simeng Han, Yoshiki Takashima, Anjiang Wei, Zhaoyu Li, Michael Genesereth

arXiv:2610.02792v1cs.AI

TL;DR

Scalable translation of legal texts into accurate executable representations remains underdeveloped, and tax forms pose a structured but interdependent formalization challenge. LAW&ORDER synthesizes symbolic programs from forms and instructions, then verifies and repairs them at the cell level. It achieves 100% accuracy on held-out returns, compared with 66% for a frontier LLM.

  • Problem

    Scalable methods for translating legal texts into accurate symbolic representations remain underdeveloped, while interdependent tax-form computations make final-output verification insufficient to locate errors.

    Source: §1 · pp. 1–2

  • Method

    LAW&ORDER preserves form structure by representing computed cells as symbolic functions, then combines LLM synthesis with cell-level verification and iterative localized repair.

    Source: §1 · p. 2

  • Results

    100% accuracy for LAW&ORDER versus 66% of returns correctly computed by a frontier LLM on independently authored, CPA-written held-out returns across 30 tax forms.

    Source: §6 · p. 9

  • Takeaways & Limitations

    The results demonstrate that iterative localized repair improves performance beyond human-written repair cases, including on independently authored held-out returns.

    Source: §6 · p. 10

    The program-generation stage uses IRS form instructions as its semantic source; these require substantially less legal interpretation than statutes and regulations.

    Source: §3.3 · p. 5

Abstract

from arXiv · show

Legal systems are increasingly implemented through software, yet scalable methods for translating legal texts into accurate symbolic representations remain underdeveloped. We study this problem through tax law, where forms and filing instructions define large computational structures involving arithmetic, branching, recursion, and tabular reasoning. We propose Law&Order, a neuro-symbolic framework for automatically formalizing tax forms and instructions into executable symbolic programs. Our approach establishes two forms of correspondence between law and logic: structural correspondence, which aligns legal and symbolic components such as cells and schedules, and denotational correspondence, which requires symbolic components to implement the computations specified by their legal counterparts. We combine large language model synthesis with cell-level verification and iterative localized error repair using human-written OpenTaxSolver tax returns. We then evaluate the resulting formalizations on independently authored, held-out TaxCalcBench returns, that are never exposed during generation or repair. Although the most advanced LLM achieves only 66% accuracy, Law&Order achieves 100% cell-level and form-level accuracy on 51 held-out returns, demonstrating the effectiveness of combining LLM-based synthesis with symbolic verification for scalable and verifiable large-scale legal autoformalization compared with using an LLM alone.

1 INTRODUCTION

Tax forms provide a structured but large-scale test case for legal autoformalization: cell-level rules depend on one another, so final-output checks alone may not locate errors. LAW&ORDER preserves that structure and uses iterative cell-level verification and repair, then tests generalization on held-out returns.

1 INTRODUCTION

  • Legal autoformalization remains difficult to scale: expert legal formalization is largely manual, while existing autoformalization methods focus primarily on mathematics.The IRS Direct File system required $16 million and more than two years to build.Source: §1 · p. 1
  • IRS forms and instructions offer an intermediate, comparatively operational source for formalization, unlike higher-level statutes and regulations.Annual revisions are consolidated within these documents rather than dispersed across amendments and cross-references.Source: §1 · pp. 1–2
  • Tax forms combine taxpayer inputs and computed cells, requiring executable arithmetic, branching, tabular operations, and cell dependencies.Errors can propagate through these dependencies, making final-output verification insufficient to locate where a formalization diverges from the intended rules.Source: §1 · pp. 1–2
  • The system represents computed cells as individual symbolic functions organized by form sections and schedules, enabling discrepancies to be localized and corresponding functions revised.Generation, cell-level verification, and iterative repair form a test-driven formalization loop.Source: §1 · p. 2
  • LAW&ORDER achieves 100% accuracy across held-out returns, compared with 66% for the most advanced LLM.The evaluation uses independently authored, CPA-written returns that were not exposed during generation or correction.Source: §1 · p. 2

2 RELATED WORK

Prior autoformalization research has focused largely on mathematics, while computational-law systems have often relied on human-authored formalizations. LAW&ORDER instead synthesizes programs and uses expected intermediate cell values for localized repair.

2.1 AUTOFORMALIZATION METHODS AND VERIFICATION

  • Compilation and syntactic validity do not establish that a formalization preserves its source meaning, motivating semantic evaluation or formal equivalence checks.Earlier autoformalization work has developed across Olympiad, undergraduate theorem, geometry, and Lean 4 tasks.Source: §2.1 · p. 3

2.2 COMPUTATIONAL LAW AND TAX-LAW FORMALIZATION

  • Prior computational-law systems largely rely on human-authored formalizations, whereas LAW&ORDER synthesizes programs and repairs discrepancies against expected intermediate cell values.Legal benchmarks also evaluate statutory reasoning and executable Prolog generation.Source: §2.2 · pp. 3–4

3 METHOD

LAW&ORDER converts tax forms and instructions into symbolic functions aligned with form structure, then synthesizes, verifies, and repairs their implementations using return examples. Its cell-level comparisons localize mismatches, while agreement on repair examples is not a proof of universal semantic equivalence.

3 METHOD

  • The pipeline transforms forms and instructions into an executable symbolic representation through structure extraction, function-signature generation, program synthesis, and repair-set-assisted verification.Its objective is to reproduce the computations specified by the form and accompanying instructions.Source: §3 · p. 4

3.1 FORM STRUCTURE EXTRACTION

  • Form structure extraction identifies computationally relevant cells and definitions, and audits found no observed errors in the extracted structures across the reviewed forms.A regex-based algorithm extracts the cells and their definitions from form PDFs.Source: §3.1 · p. 4

3.2 FUNCTION SIGNATURE GENERATION

  • Each cell receives a function signature describing its inputs and output type, forming a computational skeleton before implementation logic is added.Audits of generated function signatures across the reviewed forms found no observed errors.Source: §3.2 · pp. 4–5

3.3 INSTRUCTION-GROUNDED PROGRAM SYNTHESIS

  • An LLM synthesizes executable logic for each function using the tax form, its instructions, and the generated function signatures.The method treats official form instructions as its semantic source because they require substantially less legal interpretation than statutes and regulations.Source: §3.3 · p. 5

3.4 REPAIR SET-ASSISTED VERIFICATION AND CORRECTION

  • Validation compares generated cell values with expected values from repair-set returns and regenerates affected functions until every cell matches those examples.The comparison provides localized feedback; matching a finite repair set establishes behavioral agreement on those examples, not universal semantic equivalence.Source: §3.4 · p. 5

4 EXPERIMENTS

Experiments compare model and repair strategies for tax-return computation, define cell- and form-level correctness, and examine both benchmark performance and semantic equivalence. LAW&ORDER substantially improves GPT-5.5 results, though performance varies by model.

4.1 EXPERIMENTAL SETUP

  • Seven language models are evaluated; OpenTaxSolver test returns support program repair, and 51 TaxCalcBench cases evaluate return computation against expected outputs.Baselines include direct translation, self-debugging with execution feedback, and computation without formalization, with or without web search.Source: §4.1 · pp. 5–6

4.3 MAIN RESULTS

  • 95.0% return-level accuracy for GPT-5.5 (Medium) with LAW&ORDER versus 17.5% with direct translation and 37.5% with self-debugging; cell-level accuracy reaches 99.3%.LAW&ORDER also reaches 100% return- and cell-level accuracy with GPT-6, but does not consistently outperform self-debugging across models.Source: Table 1 · p. 6, §4.3 · p. 7

4.2 ACCURACY MEASUREMENT

  • Cell-level accuracy is the fraction of evaluated cells computed correctly, while a form is correct only when all its cells match benchmark outputs.Table 2 compares direct translation, self-debugging, and LAW&ORDER on Tax Year 2024.Source: §4.2 · p. 6, Table 2 · p. 7

4.3 MAIN RESULTS

  • For Tax Year 2024, GPT-5.5’s weaker LAW&ORDER performance is chiefly tied to an error in Form 1040 Line 35a, which affects refund returns but not returns without refunds.Line 35a computes the refund and involves four operations, including division.Source: §4.3 · p. 7
  • Figure 3 compares calculation-chain lengths for correct and incorrect GPT-5.5 predictions.Source: Figure 3 · p. 8

4.4 PROVING SEMANTIC EQUIVALENCE AND DIVERGENCE

  • 43 of 50 sampled Claude Opus 5.5 cells were proven equivalent; among seven counterexamples, six exposed model errors and one exposed a gold-implementation error.Source: §4.4 · p. 8

5 ANALYSIS

The benchmark forms contain long dependency chains, and errors become more common as calculation chains grow. LAW&ORDER improves more steadily across iterations than self-debugging, while a small repair set covers most cells but fewer branches.

5.1 COMPLEXITY ANALYSIS OF THE TEST SET.

  • The 1,847 cells span reasoning depths up to 30, with 1,021 raw-input cells at depth 0.Many computed cells require multiple levels of reasoning, including depths of 5 and 10 or greater.Source: §5.1 · p. 8

5.2 ACCURACY VS LENGTH OF CALCULATION CHAINS

  • Errors concentrate among examples with longer calculation chains, and model accuracy decreases as reasoning depth increases.The authors describe this pattern as consistent with intermediate mistakes accumulating over multi-step computations.Source: §5.2 · p. 8
  • GPT-6 reaches 100% and GPT-5.5 reaches 99.8% line-level accuracy on the independently authored test set as LAW&ORDER improves more steadily than self-debugging.The comparison covers iterative accuracy on repair and test sets; self-debugging with GPT-5.5 fluctuates and regresses substantially.Source: §5.2 · p. 8, Figure 5 · p. 9, Figure 6 · p. 9

5.3 LINE COVERAGE OF THE TEST CASES

  • For TY 2024, the repair set covers 94.6% of cells and 44.0% of branches, versus 98.6% of cells and 73.1% of branches on the 51-input test set.TY 2025 shows a similar gap in branch coverage: 44.0% for repair versus 73% for testing, while cell coverage is 93.3% versus 93%.Source: §5.3 · p. 9

6 CONCLUSION

LAW&ORDER is an iterative optimization framework for tax-law autoformalization with localized program repair. On held-out returns across 30 tax forms, it achieves 100% accuracy, compared with 66% for a frontier LLM.

6 CONCLUSION

  • LAW&ORDER achieves 100% accuracy on independently authored, CPA-written held-out returns across 30 tax forms, while a frontier LLM correctly computes only 66% of returns.The authors report that iterative repair improves performance on the repair set with corresponding improvements on held-out cases.Source: §6 · pp. 9–10

8 STATEMENTS

The authors describe generative-AI assistance in manuscript preparation and related tasks, while excluding its use in research design and experimental interpretation. They state that data, code, outputs, and procedures will be released upon publication.

AI USE STATEMENT

  • Generative AI assisted with writing, tables, figures, literature work, code, and drafting, but not with research methodology, experiments, interpretation, or mathematical proofs.The authors say all AI-assisted content was reviewed and that LLM-generated code was validated against real-world inputs.Source: AI USE STATEMENT · p. 11

REPRODUCIBILITY STATEMENT

  • The authors state that data, code, experimental outputs, and detailed procedures will be made publicly available upon publication.Source: REPRODUCIBILITY STATEMENT · p. 11

A.1 DETAILS ON TAX FILING AND TAX FORMS.

Federal income tax filing is presented as a sequence of interdependent computations from reported income to a refund or balance due. Legal rules are progressively refined through forms and instructions before implementation in software.

A.1 DETAILS ON TAX FILING AND TAX FORMS.

  • Filing aggregates income and applies adjustments to derive AGI, which informs later eligibility criteria, phase-outs, and tax computations.Source: §A.1 · p. 14
  • Deductions determine taxable income, which is used to compute tax liability before credits and payments are reconciled into a refund or balance due.Preferentially treated income, including qualified dividends and capital gains, follows separate computational rules.Source: §A.1 · p. 14
  • Statutes and other high-level sources are refined through regulations, guidance, forms, and instructions before software implementation.Source: §A.1 · p. 14
  • Most equivalence proofs are short and use reflection tactics, as illustrated in Figure 8(a).Source: §A.1 · p. 14

A.2 OTHER ANALYSES

The analyses characterize the dataset’s scale and the wide range of tax-form computation sizes. They also point to tables organizing cells by reasoning depth.

A.2 OTHER ANALYSES

  • Across 26 forms, the dataset contains 28 source files and 1,019 synthesized cells, with form sizes ranging from fewer than 20 cells to 153.CA 540 has 153 cells, Form CA 5805 has 143, NY IT-201 has 118, and OR-40 has 102.Source: §A.2 · pp. 14–15, Table 3 · p. 15
  • 17 cells exceed 200 operators, while operator counts otherwise concentrate at lower values, revealing a long tail of computational complexity.The analysis spans 1,847 cells; Figure 9’s caption describes cells across 28 tax forms, while the prose reports 26.Source: §A.2 · pp. 15–16, Figure 9 · p. 16
  • The paper presents individual forms contributing to cells at different reasoning depths, and lists those forms in Tables 4 and 5.Source: §A.2 · p. 16

A.3 EXPERIMENTAL DETAILS

This appendix describes prompts and implementation constraints for generating and repairing Lean formalizations, including parser and form-cell conventions, trace output requirements, localized repair guidance, and a prompt for forward-reference repair.

A.3 EXPERIMENTAL DETAILS

  • Both self-debugging and Law&Order runs are capped at 20 iterations, with prompts provided for translation, entailment, extraction, correspondence localization, and repair.The prompt set also includes self-consistency and round-trip localization prompts.Source: §A.3 · p. 16, Table 6 · p. 16, Table 13 · p. 22
  • Lean submissions must import only ExampleParse, avoid `sorry`, use available parser helpers conservatively, and typecheck under Lean 4.29.1.Instructions warn against assuming benchmark-specific APIs and against unsupported or deprecated Lean operations.Source: §A.3 · pp. 17, 18, 20
  • Form-cell implementations read inputs from parsed data, compute cells from earlier cells, and parse repeating rows only when row boundaries require it.The instructions distinguish scalar forms from repeated sections and require row labels and order to match the form.Source: §A.3 · pp. 18–19
  • Trace output must use deterministic, ordered cell labels and omit absent optional row cells; repair prompts target the primary failing cell and give guidance for rounding mismatches.Rounding guidance directs repairs to inspect upstream `wholeRound` use when fractional cents are lost or small discrepancies propagate downstream.Source: §A.3 · pp. 19, 28, 29
  • Table 30 presents the forward-reference repair prompt.Source: Table 30 · p. 29

A.4 EXAMPLES

The example presents executable Lean code organized around individual form lines. It shows how separate computations feed into a total additional deduction.

A.4 EXAMPLES

  • The Schedule 1-A example represents each intermediate quantity as a separate Lean function, preserving the form’s line structure and dependencies.The program computes values section by section and renders line-by-line output from a parsed example return.Source: §A.4 · p. 33
  • The example computes deductions for tips, overtime, interest, and eligible taxpayers aged 65 or older, applying caps and income-based phaseouts.Auxiliary operations include nonnegative truncation and minimum and maximum selection.Source: §A.4 · p. 33
  • The final computation aggregates the allowable component deductions into the total additional deduction reported on line 38.The program first parses taxpayer information and values imported from Form 1040, including adjusted gross income, filing status, and age indicators.Source: §A.4 · p. 33
Loading 2610.02792v1…