Law And Order: Tax Law Autoformalization

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

cs.AIOct 2, 2026

Law And Order: Tax Law Autoformalization

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

Organizations: Stanford University · Stanford Law School · Pramaana Labs · University of Toronto

Abstract

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.

Figures & tables

Figure 1: The Law&Order generation–verification–repair loop. Starting from an initial set of cell functions F and a repair-set of test cases T, the system repeatedly executes F on T and compares each cell’s model output o against its gold annotation G. Any cell function f whose output disagrees with G is regenerated by an LLM using that cell’s natural-language instruction, and the cycle repeats until every cell matches across all repair-set test cases. The resulting corrected F is then evaluated once on a held-out test set — never seen during synthesis or repair — to produce the final reported accuracy.

Model	Method	Correct returns (strict)	Correct returns (lenient)	Correct (by cell)	Correct (by cell, lenient)
GPT-6	w/o formalization	38.0%	54.0%	83.2%	88.0%
	w/o formalization + WS	66.0%	78.0%	88.6%	92.0%
	Direct translation	95.0%	95.0%	99.3%	99.3%
	Self-debugging	100.0%	100.0%	100.0%	100.0%
	Law&Order	100.0%	100.0%	100.0%	100.0%
GPT-5.5 (Medium)	Direct translation	17.5%	17.5%	73.3%	73.5%

Table 1: Comparison of model performance on Tax Year (TY) 2025 tax-return computation, with and without symbolic formalization. For each model, we report baselines without formalization followed by direct translation, self-debugging with execution feedback, and Law&Order with localized execution feedback. WS stands for Web Search. Best results within each model are shown in bold.

Model	Method	Correct returns (strict)	Correct returns (lenient)	Correct (by cell)	Correct (by cell, lenient)
GPT-6	Direct translation	100.0%	100.0%	100.0%	100.0%
	Self-debugging	86.3%	86.3%	97.5%	97.5%
	Law&Order	100.0%	100.0%	100.0%	100.0%
GPT-5.5 (Medium)	Direct translation	29.4%	31.4%	91.1%	91.4%
	Self-debugging	72.5%	72.5%	94.4%	94.4%
	Law&Order	35.3%	35.3%	91.4%	91.4%

Table 2: Comparison of model performance on Tax Year (TY) 2024 tax-return computation using symbolic formalization. For each model, we compare direct translation, self-debugging with execution feedback, and Law&Order with localized execution feedback. Best results within each model are shown in bold.

Panel of Figure 5 — Figure 5: Trace-level accuracy across optimization iterations for Law&Order and self-debugging across different models. For self-debugging, the final observed values for GPT-6 and Claude Opus 5.5 are extended through the remaining iterations.

Panel of Figure 6 — Figure 6: Cell-level accuracy across optimization iterations for Law&Order and self-debugging across different models. For self-debugging, the final observed values for GPT-6 and Claude Opus 5.5 are extended through the remaining iterations.

Appendix figures & tables30 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 7: Legal rules are built in nested refinement. A constitution has the highest authority but least detail, containing many ambiguities, vagueness, and gaps. Concrete details emerge as law is refined into more operational rules like legislation, regulation, and guidance. We formalize tax forms because they are closest to software, permitting mechanical translation.

Form	Files	Cells	Form	Files	Cells
CA_540	1	153	VA_760	1	21
Form_CA_5805	1	143	MI_1040	1	19
NY_IT201	1	118	NC_D400	1	19
OR_40	1	102	Form_2441	1	18
US_1040_2025ty	2	76	Form_8959	1	18
MA_1	1	46	Form_8960	1	17

Appendix

Table 3: Number of source files and synthesized cells for each tax form. Across 26 forms, the dataset contains 28 source files and 1,019 synthesized cells.

Panel of Figure 9 — Figure 9: Distribution of operator counts per cell_function across 1,847 cells from 28 tax forms. Some cells like the Taxpayer Identification Number are purely informational and thus ignored for the benchmark. Ignored cells are always zero operation.

Reasoning Depth	# Cells	Forms Contributing
0	1021	AZ_140 (58), CA_540 (92), Form_2210 (54), Form_2441 (35), Form_6781 (11), Form_8606 (20), Form_8812 (15), Form_8829 (34), Form_8959 (10), Form_8960 (25), Form_8995 (10), Form_CA_5805 (79), HSA_Form_8889 (15), MA_1 (55), MI_1040 (31), NC_D400 (21), NJ_1040 (32), NY_IT201 (74), OH_IT1040 (17), OR_40 (56), PA_40 (24), US_1040_2025ty (157), US_1040_Sched_1-A (17), US_1040_Sched_C (46), US_1040_Sched_SE (8), VA_760 (25)
1	227	AZ_140 (10), CA_540 (21), Form_2210 (1), Form_2441 (8), Form_6781 (3), Form_8606 (3), Form_8812 (7), Form_8829 (7), Form_8959 (5), Form_8960 (5), Form_8995 (4), Form_CA_5805 (13), HSA_Form_8889 (4), MA_1 (18), MI_1040 (7), NC_D400 (6), NJ_1040 (3), NY_IT201 (7), OH_IT1040 (4), OR_40 (15), PA_40 (2), US_1040_2025ty (52), US_1040_Sched_1-A (8), US_1040_Sched_C (4), US_1040_Sched_SE (3), VA_760 (7)
2	119	AZ_140 (3), CA_540 (10), Form_2210 (2), Form_2441 (8), Form_6781 (1), Form_8606 (3), Form_8812 (4), Form_8829 (1), Form_8959 (4), Form_8960 (3), Form_8995 (4), Form_CA_5805 (11), HSA_Form_8889 (3), MA_1 (5), MI_1040 (3), NC_D400 (3), NJ_1040 (2), NY_IT201 (2), OH_IT1040 (2), OR_40 (10), PA_40 (2), US_1040_2025ty (23), US_1040_Sched_1-A (4), US_1040_Sched_C (2), US_1040_Sched_SE (2), VA_760 (2)
3	86	AZ_140 (2), CA_540 (10), Form_2210 (1), Form_2441 (4), Form_6781 (1), Form_8606 (2), Form_8812 (1), Form_8829 (3), Form_8959 (4), Form_8960 (1), Form_8995 (1), Form_CA_5805 (9), HSA_Form_8889 (2), MA_1 (4), MI_1040 (1), NC_D400 (2), NJ_1040 (2), NY_IT201 (5), OH_IT1040 (1), OR_40 (5), PA_40 (1), US_1040_2025ty (15), US_1040_Sched_1-A (5), US_1040_Sched_C (1), US_1040_Sched_SE (1), VA_760 (2)
4	55	AZ_140 (1), CA_540 (3), Form_2441 (1), Form_6781 (1), Form_8606 (3), Form_8812 (1), Form_8829 (3), Form_8959 (2), Form_8960 (2), Form_8995 (1), Form_CA_5805 (6), HSA_Form_8889 (1), MA_1 (2), MI_1040 (1), NC_D400 (1), NJ_1040 (1), NY_IT201 (3), OH_IT1040 (1), OR_40 (2), PA_40 (1), US_1040_2025ty (11), US_1040_Sched_1-A (4), US_1040_Sched_C (1), US_1040_Sched_SE (1), VA_760 (1)
5	48	AZ_140 (1), CA_540 (2), Form_2441 (1), Form_6781 (2), Form_8606 (3), Form_8812 (1), Form_8829 (2), Form_8959 (1), Form_8960 (2), Form_8995 (1), Form_CA_5805 (6), HSA_Form_8889 (1), MA_1 (2), MI_1040 (1), NC_D400 (1), NJ_1040 (1), NY_IT201 (1), OH_IT1040 (2), OR_40 (1), PA_40 (1), US_1040_2025ty (7), US_1040_Sched_1-A (4), US_1040_Sched_C (1), US_1040_Sched_SE (2), VA_760 (1)

Appendix

Table 4: Distribution of cells by reasoning depth and contributing tax forms (depths 0–7).

Reasoning Depth	# Cells	Forms Contributing
8	26	AZ_140 (1), CA_540 (1), Form_2441 (2), Form_8812 (1), Form_8829 (1), Form_CA_5805 (4), MA_1 (1), MI_1040 (2), NC_D400 (2), NJ_1040 (3), NY_IT201 (1), OH_IT1040 (2), OR_40 (1), US_1040_2025ty (2), US_1040_Sched_1-A (1), VA_760 (1)
9	24	AZ_140 (1), CA_540 (1), Form_2441 (1), Form_8812 (1), Form_8829 (2), Form_CA_5805 (4), MA_1 (1), MI_1040 (1), NC_D400 (1), NJ_1040 (2), NY_IT201 (1), OH_IT1040 (2), OR_40 (1), US_1040_2025ty (2), US_1040_Sched_1-A (1), VA_760 (2)
10	19	AZ_140 (2), CA_540 (1), Form_2441 (1), Form_8812 (1), Form_8829 (1), Form_CA_5805 (4), MA_1 (1), NJ_1040 (1), NY_IT201 (1), OH_IT1040 (1), OR_40 (1), US_1040_2025ty (2), VA_760 (2)
11	17	AZ_140 (1), CA_540 (1), Form_2441 (1), Form_8812 (1), Form_CA_5805 (4), MA_1 (1), NJ_1040 (2), NY_IT201 (1), OH_IT1040 (2), OR_40 (1), US_1040_2025ty (2)
12	14	AZ_140 (2), CA_540 (1), Form_2441 (1), Form_CA_5805 (4), MA_1 (1), NY_IT201 (1), OH_IT1040 (1), OR_40 (1), US_1040_2025ty (2)
13	10	CA_540 (1), Form_2441 (1), Form_CA_5805 (1), MA_1 (2), NY_IT201 (1), OR_40 (2), US_1040_2025ty (2)

Appendix

Table 5: Distribution of cells by reasoning depth and contributing tax forms (depths 8–30).

You complete a Lean 4 tax-form skeleton (Template.lean).

The skeleton already defines helpers, structures, render, and main.

Each def cell_* function whose body is sorry must be filled in using the

form instructions provided below. These include the instruction booklet (when

bundled), inline {...} guidance from the form template, and -- comments on

cells in Template.lean.

Appendix

Table 6: Translation prompt (TRANSLATION_PROMPT). The placeholders method_text , hint_text , cell_breakdown , section_parser_snippet , and row_pattern_snippet are expanded as shown in Table 7 --Table 12 .

Use a deliberate completion method:

1. Read the form instructions provided below (instruction booklet, inline {...}

notes from the form template, and -- comments in Template.lean), then the

skeleton helpers and existing input cell_* functions.

2. For every def cell_* whose body is sorry, implement the computation described

in those instructions for that line or cell. Match each function to the form using

its name, labels, and comments in Template.lean.

Appendix

Table 7: Method instructions (METHOD_INSTRUCTIONS), substituted for method_text in the translation prompt. Empty in the ablation.

Highest-priority repair target from the previous attempt:

{ hints }

Use that feedback as the first thing to fix.

Preserve earlier cells that already match.

If the feedback names a first failing cell, keep every earlier emitted cell unchanged and make the next emitted output line match the expected cell exactly before changing later cells.

If the feedback is a Lean diagnostic, fix that exact construct first and avoid unrelated rewrites.

{ available_cells_section }

Appendix

Table 8: Repair-round hint text, substituted for hint_text in the translation prompt when feedback from a previous attempt is available.

Available cell functions (use only these identifiers; do not invent new cell_* names or guess namespaced spellings):

{ joined }

Appendix

Table 9: Available-cells section, substituted for available_cells_section in the hint text and the repair prompt.

Per-cell breakdown of the sorry functions you must implement.

Each entry gives the def cell_* you must fill and the form text describing it.

Implement exactly these functions; leave every other definition unchanged.

Appendix

Table 10: Cell-breakdown header (CELL_BREAKDOWN_HEADER), prepended to the per-cell instruction text substituted for cell_breakdown .

def wordsBeforeSemicolon (tokens : List String) : List String :=

tokens.takeWhile (fun tok => tok != ";")

def startsSection (label : String) (line : String) : Bool :=

match words (cleanLine line) with

| first :: _ => first = label

Appendix

Table 11: Section-parser snippet (SECTION_PARSER_SNIPPET), substituted for section_parser_snippet in the translation prompt.

structure Row where

desc : String

x : Float

y : Float

partial def buildRows : List String -> List String -> List Row

Appendix

Table 12: Row-pattern snippet (ROW_PATTERN_SNIPPET), substituted for row_pattern_snippet in the translation prompt.

Fill the missing computed cells in this tax form and return only a comparable trace.

Return plain text only.

Do not use markdown, code fences, explanations, or notes.

Do not emit section headers, comments, or synthetic summary labels.

Trace rules:

Appendix

Table 13: Entailment prompt (ENTAILMENT_PROMPT): the model fills in the computed cells of a partially filled form.

You read filled-in examples of one tax form and list every cell on the form.

A "cell" is one numbered line or labeled entry on the form, for example L1, L4, BoxA,

or YourName. For each cell decide whether it is an input (a value the filer enters

directly, copied from a document or another form) or computed (a value derived by

arithmetic from other cells on this same form).

Appendix

Table 14: Cell-extraction prompt (CELL_EXTRACTION_PROMPT).

You verify every cell of a Lean 4 tax-form translation against its instructions in one pass.

For each cell below (listed from low to high), decide whether the Lean implementation matches

the natural-language instruction. Report every cell whose Lean code does not match its instruction.

If every cell matches, answer on the first line with exactly MATCH ALL.

Appendix

Table 15: Batched correspondence localization prompt (CORRESPONDENCE_BATCH_PROMPT). cells_block repeats the block in Table 16 once per cell.

### { name }

Instruction:

{ nl }

Lean:

{ lean }

Appendix

Table 16: Per-cell block substituted into cells_block of the correspondence and self-consistency prompts.

You verify one cell of a Lean 4 tax-form translation against its instruction.

Cell: { cell_name }

Natural-language instruction for this cell:

{ nl }

Appendix

Table 17: Single-cell correspondence localization prompt (CORRESPONDENCE_JUDGE_PROMPT).

You previously produced this Lean 4 tax-form translation. Critique your own output.

For each cell below (listed from low to high), decide whether the Lean implementation correctly

matches the natural-language instruction. Do not use external oracles, gold answers, or test

traces — judge only from the instructions and the Lean code you see.

If you agree that every cell is correct, answer on the first line with exactly MATCH ALL.

Appendix

Table 18: Self-consistency critique prompt (SELF_CONSISTENCY_CRITIQUE_PROMPT). cells_block is formatted as in Table 16 .

Describe, in one or two plain-English sentences each, exactly what every Lean 4

tax-form cell below computes. For each cell output one line in this exact format:

<cell_name>: <description>

Describe only the computation each cell performs in terms of the other cells and inputs it

reads; add no commentary, caveats, or markdown outside those lines.

Appendix

Table 19: Round-trip localization, step 1, batched (LEAN_TO_NL_BATCH_PROMPT). cells_block repeats the block in Table 21 .

### { name }

{ lean }

Appendix

Table 20: Per-cell block substituted into cells_block of the batched Lean-to-English prompt.

### { name }

{ lean }

Appendix

Table 21: Per-cell block substituted into cells_block of the batched Lean-to-English prompt.

You compare reference instructions against descriptions derived from Lean code

for every cell of a tax form in one pass.

For each cell below, decide whether the two descriptions describe the same computation.

Report every cell where they differ.

If every cell matches, answer on the first line with exactly MATCH ALL.

Appendix

Table 22: Round-trip localization, step 2, batched (NL_EQUIVALENCE_BATCH_PROMPT). cells_block repeats the block in Table 23 .

### { name }

Reference instruction:

{ expected_nl }

Description derived from Lean:

{ derived_nl }

Appendix

Table 23: Per-cell block substituted into cells_block of the batched equivalence prompt.

Describe, in one or two plain-English sentences, exactly what this Lean 4

tax-form cell computes. Describe only the computation it performs in terms of the other

cells and inputs it reads; add no commentary, caveats, or markdown.

{ lean }

Appendix

Table 24: Round-trip localization, step 1, single cell (LEAN_TO_NL_PROMPT).

You compare two descriptions of one tax-form cell.

Reference instruction (from the form):

{ expected_nl }

Description derived from the Lean code:

{ derived_nl }

Appendix

Table 25: Round-trip localization, step 2, single cell (NL_EQUIVALENCE_PROMPT).

A Lean 4 tax form and an independently filled-in version of the

same form disagree on one cell.

Cell / line: { label }

Natural-language instruction for this cell:

{ nl }

Appendix

Table 26: Entailment-divergence explanation prompt (DIVERGENCE_EXPLANATION_PROMPT).

You repair a Lean 4 tax-form translation (a filled Main.lean-style file).

A localization step identified the first incorrect cell and produced a hint describing the

issue. Fix ONLY that primary failing cell (and at most the tiny helper edits required for it

to typecheck). Keep every other cell_* function, helper, render, and main exactly as

they are. Do not reorder top-level declarations. Do not introduce sorry. Do not change

function names or type signatures except where the hint requires it.

Appendix

Table 27: Shared repair prompt (REPAIR_PROMPT). The optional sections are shown in Table 28 and Table 9 .

Detected rounding pattern:

{ rounding_extra }

Reference instructions for the failing cell only (use these to confirm the correct computation):

{ instructions }

Appendix

Table 28: Optional sections of the repair prompt: rounding_hint_section (top; rounding_extra is one message from Table 29 ) and form_instructions_section (bottom). Each is included only when non-empty.

[Fractional cents expected, whole amount produced]

Gold keeps fractional cents ({ expected_value }) but the candidate returned a whole amount ({ actual_value }). Inspect this cell and upstream cells for unconditional wholeRound. Gold Main.lean often keeps raw floats on regular example inputs and only rounds when isTaxCalcBenchInput s is true (pattern: if isTaxCalcBenchInput s then wholeRound x else x).

[Difference of exactly $0.10]

Values differ by exactly $0.10 ({ expected_value } vs { actual_value }). This often means an upstream cell rounded a value like 5.1 down to 5.0 with wholeRound where gold keeps the float. Fix the upstream rounding guard before changing downstream tax formulas.

Appendix

Table 29: Rounding-mismatch messages (rounding_mismatch_hint). At most one, selected by the kind of mismatch, is inserted into the repair prompt.

You fix a forward reference in a Lean 4 tax-form cell.

The cell { caller_name } calls { bad_callee }, but { bad_callee } is defined

later in the file (higher cell number). Replace each bad call with an earlier cell

from the allowed list, or inline logic using only allowed cells / inputs.

Return only JSON (no markdown) in this shape:

Appendix

Table 30: Forward-reference repair prompt (FORWARD_REF_REPAIR_PROMPT).

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 116 papers

Reasoners or Translators? Contamination-aware Evaluation and Neuro-Symbolic Robustness in Tax Law
May 15, 2026Parisa Kordjamshidi, Samer Aslan, Madhavan Seshadri +2Data Contamination in Language Models Neuro-Symbolic Reasoning
Bloomberg · Michigan State University
By Their Fruits You Will Know Them: Comparing Formalizations of Law by the Decisions They Encode
May 24, 2026Julius Vernie, Matthias GrabmairLLM Evaluation Differential Testing
Technical University of Munich (TUM) · Technical University of Munich
Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning
Jun 15, 2026Olivia Peiyu Wang, Sanna Wong-Toropainen, Daneshvar Amrollahi +4Faithfulness of Language Model Reasoning LLM Reliability
UC Santa Cruz · Univ. Helsinki · CodeX, Stanford +4

May 15, 2026J/K move · Enter open · S save

Reasoners or Translators? Contamination-aware Evaluation and Neuro-Symbolic Robustness in Tax Law

Parisa Kordjamshidi, Samer Aslan, Madhavan Seshadri, Leslie Barrett+1

Bloomberg · Michigan State University

Data Contamination in Language Models Neuro-Symbolic Reasoning Language Model Robustness Legal Reasoning

Open paper AskPDF arXiv

Recent advances in large language models (LLMs) have significantly enhanced automated legal reasoning. Yet, it remains unclear whether their performance reflects genuine legal reasoning ability or artifacts of data contamination. We present a comprehensive empirical study of tax law reasoning approaches and implement a contamination detection protocol to rigorously assess LLM reliability. We show that performance can be inflated by contamination. Building on this analysis, we conduct a systematic evaluation, comparing monolithic LLMs with hybrid systems that translate statutory text into formal representations and delegate inference to symbolic solvers. We build a novel test suite designed to probe generalization to unseen documents via case and rule variations. Our findings indicate that legal reasoning is inherently compositional and that neuro-symbolic frameworks offer a more reliable and robust foundation for legal AI, as well as improved generalization to unobserved situations.

Abstract

Autoformalization

Explore similar work

Reasoners or Translators? Contamination-aware Evaluation and Neuro-Symbolic Robustness in Tax Law

By Their Fruits You Will Know Them: Comparing Formalizations of Law by the Decisions They Encode

Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning