法律系统正日益通过软件实现，但将法律文本转化为精确符号表示的可扩展方法仍不成熟。我们以税法为切入点，税表和申报指引本身构成了包含算术、分支、递归和表格推理的大规模计算结构。为此我们提出 Law&Order，一种神经符号框架，能够自动将税表及其说明形式化为可执行的符号程序。框架建立了两类对应关系：结构对应把法律要素（如单元格、附表）与符号要素对齐；语义对应要求符号组件实现其法律对应项规定的计算。实现上，我们将大语言模型（LLM）用于程序合成，随后在单元格层面进行验证，并利用人工编写的 OpenTaxSolver 税表返回进行局部错误修复的迭代。最终在独立构造的 TaxCalcBench 持出集上进行评估，这些返回在生成和修复阶段均未出现。单纯使用最先进的 LLM 只能达到 66% 的准确率，而 Law&Order 在 51 份持出返回上实现了 100% 的单元格级和表单级准确率，证明了 LLM 合成结合符号验证在大规模法律自动形式化中的有效性。
点评