Law&Order 用神经符号框架将税法表格与填报说明自动形式化为可执行程序，在 51 份留出申报表上达到 100% 单元格级与表格级准确率
相关研究与后续进展
核心概要
该工作提出 Law&Order 神经符号框架，通过结构对应与指称对应两种法律—逻辑对应关系，结合大语言模型合成、单元格级验证与基于人工编写的 OpenTaxSolver 申报表的迭代局部错误修复，将税法表格与填报说明自动形式化为可执行符号程序，并在从未参与生成或修复的独立留出 TaxCalcBench 申报表上评估：最强 LLM 仅达 66% 准确率，而 Law&Order 在 51 份留出申报表上达到 100% 单元格级与表格级准确率。
Figure 1: The Law&Order generation–verification–repair loop. Starting from an initial set of cell functions F and a repair-set of test cases T, the system repeatedly executes F on T and compares each cell’s model output o against its gold annotation G. Any cell function f whose output disagrees with G is regenerated by an LLM using that cell’s natural-language instruction, and the cycle repeats until every cell matches across all repair-set test cases. The resulting corrected F is then evaluated once on a held-out test set — never seen during synthesis or repair — to produce the final reported accuracy.
arXiv深度剖析
提出 Law&Order 神经符号框架，可自动将税法表格与填报说明形式化为可执行符号程序，处理算术、分支、递归与表格推理等大型计算结构。 此前将法律文本翻译为准确符号表示的可扩展方法尚不成熟，该工作以税法为具体场景给出端到端的形式化流程。 摘要层面描述了框架组成与目标，未提供组件级消融或内部实现细节。
建立法律与逻辑之间的两种对应关系：结构对应对齐单元格、附表等法律与符号组件，指称对应要求符号组件实现其法律对应物所规定的计算。 将形式化正确性拆解为结构一致与语义一致两个可检验维度，为验证提供明确判据。 摘要给出定义性描述，未报告对应关系各自的独立验证结果。
将大语言模型合成与单元格级验证、迭代局部错误修复相结合，并以人工编写的 OpenTaxSolver 申报表作为修复依据。 把 LLM 生成与符号验证闭环结合，而非仅依赖单次 LLM 输出。 摘要说明方法组合方式，未给出修复迭代次数或收敛行为数据。
在独立编写、从未在生成或修复阶段暴露的留出 TaxCalcBench 申报表上，Law&Order 在 51 份申报表上达到 100% 单元格级与表格级准确率，而最强 LLM 仅 66%。 以留出集对比展示 LLM 合成加符号验证相对单用 LLM 的差距。 摘要报告了留出集规模（51 份）与两类准确率数字，未提供置信区间或逐表分布。
启示与展望
该结果面向税法表格与填报说明这一规则密集、计算结构明确的场景，适用于需要将法律文本转为可执行符号程序并进行单元格级与表格级验证的读者，例如法律信息学、合规计算与形式化方法研究者。摘要所述评估基于独立编写、未参与生成或修复的留出 TaxCalcBench 申报表，因此其适用范围以该基准与税法领域为界。
摘要未说明单元格级验证与迭代局部错误修复的具体实现、修复迭代次数与失败模式，也未给出 100% 与 66% 之外的逐表分布或统计不确定性；此外，留出集为 51 份 TaxCalcBench 申报表，其在更广泛税法条款与其他法律领域的可迁移性仍需后续工作检验。