法律与秩序：税法自动形式化

中文摘要 AI 辅助

法律体系日益通过软件实施，但将法律文本转化为准确的符号表示的可扩展方法仍不完善。我们通过税法研究这一问题，其中表格和申报说明定义了涉及算术、分支、递归和表格推理的大型计算结构。我们提出Law&Order，一个用于将税务表格和说明自动形式化为可执行符号程序的神经符号框架。我们的方法在法律与逻辑之间建立了两种对应关系：结构对应，将法律与符号组件（如单元格和附表）对齐；以及指称对应，要求符号组件实现其法律对应部分所规定的计算。我们将大语言模型合成与单元格级验证以及使用人工编写的OpenTaxSolver纳税申报表进行的迭代局部错误修复相结合。然后，我们在独立编写、保留的TaxCalcBench申报表上评估所得的形式化结果，这些申报表在生成或修复过程中从未暴露。尽管最先进的大语言模型仅达到66%的准确率，Law&Order在51份保留申报表上实现了100%的单元格级和表格级准确率，证明了与单独使用大语言模型相比，将基于大语言模型的合成与符号验证相结合用于可扩展且可验证的大规模法律形式化的有效性。

英文摘要

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.

发表机构

• Stanford University（斯坦福大学）
• Stanford Law School（斯坦福法学院）
• Pramaana Labs
• University of Toronto（多伦多大学）

机构由 AI 辅助整理，请以论文原文为准。