# Law And Order: Tax Law Autoformalization

arXiv: https://arxiv.org/abs/2610.02792 · HTML: https://mlsanity.com/paper/2610.02792/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 49 references that are in the map.
- First posted on arXiv 2 Oct 2026.

## Builds on (most cited first, 16 of 16)

- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering](https://mlsanity.com/paper/2005.05257/) (2020)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [P-FOLIO: Evaluating and Improving Logical Reasoning with Abundant Human-Written Reasoning Chains](https://mlsanity.com/paper/2410.09207/) (2024)
- [Scheherazade: Evaluating Chain-of-Thought Math Reasoning in LLMs with Chain-of-Problems](https://mlsanity.com/paper/2410.00151/) (2024)
- [An LLM Agentic Approach for Legal-Critical Software: A Case Study for Tax Prep Software](https://mlsanity.com/paper/2509.13471/) (2025)
- [DeonticBench: A Benchmark for Reasoning over Rules](https://mlsanity.com/paper/2604.04443/) (2026)
- ['Put the Car on the Stand': SMT-based Oracles for Investigating Decisions](https://mlsanity.com/paper/2305.05731/) (2023)

## Abstract (arXiv)

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.