Legal systems are increasingly implemented as software, yet scalable methods for converting legal texts into precise symbolic representations remain underdeveloped. We investigate this gap through tax law, where tax forms and filing instructions constitute massive computational structures involving arithmetic, branching, recursion, and tabular reasoning. To address it we introduce Law&Order, a neuro‑symbolic framework that automatically formalizes tax forms and instructions into executable symbolic programs. The framework defines two correspondences: structural correspondence aligns legal elements (cells, schedules) with symbolic components, and denotational correspondence requires the symbolic parts to perform the computations specified by their legal counterparts. Practically, we employ large language model (LLM) synthesis, followed by cell‑level verification and iterative localized error repair using human‑written OpenTaxSolver tax returns. We then evaluate the formalizations on an independently created held‑out set, TaxCalcBench, which is never seen during generation or repair. While the most advanced LLM alone attains only 66% accuracy, Law&Order achieves 100% cell‑level and form‑level accuracy on 51 held‑out returns, demonstrating the power of combining LLM‑based synthesis with symbolic verification for scalable, verifiable large‑scale legal auto‑formalization.
Review