Law&Order：税法自动形式化

法律系统日益由软件实现，但把法律文本翻译为准确符号表示的可扩展方法仍不成熟。我们以税法研究该问题——申报表与填报说明定义了涉及算术、分支、递归与表格推理的大型计算结构。我们提出Law&Order，把税表与说明自动形式化为可执行符号程序的神经符号框架。方法建立法律与逻辑间的两种对应：结构对应（对齐单元格、附表等法律与符号组件）与指称对应（要求符号组件实现其法律对应物规定的计算）。我们把LLM合成与单元级验证、以及使用人工编写的OpenTaxSolver申报表的迭代局部错误修复相结合。在独立撰写、生成与修复期间从未暴露的TaxCalcBench留出申报表上评估：最先进LLM单独仅66%准确率，Law&Order在51份留出申报表上实现100%的单元级与表级准确率，证明LLM合成与符号验证相结合对可扩展可验证的大规模法律自动形式化的有效性。