在 Lean 中形式化美国税法以识别起草错误和漏洞

研究团队通过将法规翻译成 Lean（一种其类型检查器可以验证数学证明的编程语言）识别出了美国税法中的 138 个起草错误。通过将法律视为一组可验证的定义，团队能够自动标记美国法典第 26 编官方文本中存在的失效交叉引用、拼写错误和不一致的细分条款。

该表格提供了初始审计阶段发现的起草错误的具体示例。

《国内税收法》的自动化审计

研究人员使用解析器读取税法中的每一个交叉引用，包括那些以纯文本形式编写的引用，如“子节 (b) 的第 (2) 段”。由于官方文本中缺乏超链接，这些引用在法律更新时很容易变成“死链”。

Lean 根据法典的版本历史验证了每个引用。测试套件报告了 257 个发现，随后由 AI 代理进行分类。虽然其中许多是针对过去时期的预期规则，但有 138 个被确认是真实故障，例如引用了已移动的条款或错误的细分名称。

由 HN Digest 根据 lexifina.com 报告的数据绘制的图表；数值按来源显示。

“我们的论点是，将 AI 和证明检查器指向法律的版本记录，可以发现人们忽略的矛盾和机械错误。”

— Formalizing the US tax code | Lexifina

将税务逻辑重写为可验证的代码

为了超越简单的文本检查，团队将 2025 年联邦所得税计算重写为 Lean。这涉及对四个不同组件的建模：收入（直至调整后总收入）、扣除额、税收计算（包括最低替代税）以及税收抵免。

此图表可视化了用于表示税法的形式化 Lean 模型的大小和组织结构。

由于将自然语言翻译成形式化代码是一个“有损”的步骤，团队通过对照 IRS 发布的数据和三个独立的税务程序对模型进行了强化。他们还雇佣了一个对抗性 AI 代理来审查代码是否存在“作弊”——即旨在通过测试但实际上并未遵循法规的逻辑。

发现隐藏漏洞和软件错误

形式化模型允许团队对税务规划策略进行“盲搜索”。这揭示了三个在从业者指南中未发现的新漏洞，例如一个特定的窗口，由于社会保障福利的上限限制，同居夫妇可以通过分开报税来省钱。

该项目还暴露了现有工具中的差异。例如，一款流行的税务软件未能将 Schedule C 附加到报税单中，导致自雇收入消失。此外，团队证明了 IRS 税务表并不是法律公式的完美反映，显示出许多纳税人的差异高达 6 美元。

此表格突出了研究团队发现的特定漏洞和软件错误。

局限性与人类解释的作用

虽然 Lean 提供了对法律字面文本的严格检查，但该项目强调了一个重要的边界：“法律精神”。机器可以证明文本允许什么，但人类法官仍然是特定解释在法庭上是否具有法律接受性的最终裁决者。

此外，从法规到代码的转变仍然是一个手动解释的过程。研究人员指出，虽然 Lean 可以证明在所有可能的输入下，当收入上升时某些扣除额永远不会增长，但将法律初始翻译成这些定义仍需要人类监督，以确保形式化准确捕捉立法意图。