跳到正文
Hacker News· dnw·· 14 小时前AI 评分64

用 Lean 形式化美国税法：查出 138 处起草错误并搜索税收漏洞

Formalizing US Tax Code (Using Lean)

AI 导读

作者将美国税法典 Title 26 逐条翻译成 Lean，用证明检查器校验交叉引用，在 2026 年 11 月 3 日的版本中报告 257 项发现，其中 138 处为真实起草错误，包括 67 处引用已废止或改写的条款、30 处括号未闭合。

正文 · AI 翻译

昨天，我们验证了可以用 Lean 搜索识别出已知的税收漏洞。今天，我们着手将整个《国内税收法典》形式化，以搜寻未知的漏洞（bug）。

用证明检查器审视法条

Lean 是一种编程语言，其类型检查器也能检查数学证明：如果 Lean 接受一个证明，那么每一步都从定义中推出，没有任何东西是凭空相信的。早前的一篇文章讨论了这种形式化在法律中能走多远，[1]而昨天我们将其用于退休账户规则，一次盲搜索重新发现了后门 Roth。[2]

这项工作属于 global-law 的一部分，这是一个采用 CC0 许可的、带版本的法律和判例法仓库。[3] 我们的论点是，将 AI 和证明检查器指向带版本的法律记录，可以发现人们遗漏的矛盾和机械性错误。特别是，我们可以发现文本中的错误，并看清规则允许什么，包括它们意外允许什么。为此，我们将法律的每一节翻译成 Lean，尽量贴近法条自身的措辞，并用 IRS 在其表格和说明中印出的示例进行测试。

1. 税法文本有 138 处起草错误

税法是《美国法典》第 26 编。其官方文本由法律修订顾问办公室（众议院负责编纂法典的办公室）以结构化数据形式发布。[4] 我们使用的是截至 2026 年 11 月 3 日的当前版本。

然后，一个解析器读取每一处交叉引用，包括用文字写成的引用（“subsection (b) 的 paragraph (2)”、“such subparagraph”、“sections 922 through 927”），这些引用不带超链接。Lean 会逐一检查。它指向的条款是否存在？是否仍然有效？（可通过我们的版本历史验证）这些检查作为测试套件运行，每当新版本添加了上一版本没有的故障时，测试就会失败。

该套件报告了 257 项发现，每一项都由 AI 代理对照官方文本及其编辑注释进行检查：98 项是有意为之（针对过去期间的规则，以及已颁布但尚未生效的条款），21 项是编辑自身超链接中的误报，138 项是真正的故障：

故障数量示例
引用已被废除、移动或重写的内容，且没有相应的符合性修改67§1(f)(7)(A) 引用了一个被重写的条款§168(n)(2)(G) 引用了一个被移动的条款
拼写错误、错误的分项或未命名的法案24§1400Z-2(f)(1) 引用了错误的子节§72(t)(2)(A)(viii) 的引用中有拼写错误
错误的层级用词8§9818(a)(1)(A) 将子节称为段落
两个条款编号相同9§1202(b)(4) 出现了两次§45X(d)(4) 出现了两次
括号从未闭合（13 处被编辑加脚注，17 处未加）30§165(h)(1) 留下一个未闭合的括号§38(c)(6)(C) 留下一个未闭合的括号

这 138 处每一处都有一份证书：一个简短的 Lean 陈述，从官方 XML 中携带证据并证明该故障。对于失效引用，证据是所引用条款下确实存在的完整列表。Lean 在大约两分半钟内重新检查了全部 138 处。

我们对《美国法典》的记录是一段 git 历史，每一条公法对应一次提交，[5]因此每个错误都能追溯到写下它的那条法律。对于第 26 编，记录可回溯至 1994 年版。

这项检查重复执行的成本很低。对每一版新发布的《法典》运行它，一旦出现新错误就能立即标记出来，并指出导致该错误的法律。

2. 将所得税改写为可检查的代码

接下来我们写下了法律所计算的内容：一个家庭的 2025 年联邦所得税，即 1040 表上的数字，包括 2025 年 7 月《One Big Beautiful Bill Act》带来的变化。[6],[7]我们分四部分完成：

  • 收入，直至调整后总收入（AGI）。AGI 是总收入减去少数项目，例如 IRA 缴款和助学贷款利息。大多数其他税收规则都依赖它。
  • 扣除：标准扣除或分项扣除，以及针对小费、加班费、汽车贷款利息和 65 岁以上人群的新扣除。
  • 税款本身，包括替代性最低税（AMT），这是一种第二套计算，防止高收入者通过扣除把税款削减得过多。
  • 抵免，例如儿童税收抵免和劳动所得税抵免（EITC），后者是面向中低收入者的抵免。

我们用 AI 将法条翻译成 Lean。这是有损的一步，因此我们用以下措施加以强化：

  • 每一部分都对照 IRS 公布的数字（税率表、EITC 表、工作表及其出版物中的示例）进行测试，并在 5,000 个家庭上与三个独立税务程序进行核对（第 3 节）。
  • 第二个 agent 并未编写该部分，它以对抗方式审查，寻找错误和作弊行为，例如为通过测试而非遵循法条而编写的代码。

Lean 最终增加的是覆盖所有输入而非样本的证明。例如，它证明 SALT 上限以及汽车贷款和加班费扣除在收入上升时从不增长，对每一种收入和每一种申报身份都成立。

与其他税务软件的比较帮助我们捕捉逻辑错误。我们正是这样在自己的模型中发现了两处错误。也正是这样，我们在其他工具中发现了逻辑性而非算术性的 bug：Tax-Calculator 将 EITC 给予单独申报者，却不检查配偶是否分居；UsTaxes 从不将 Schedule C 附到 2025 年申报表上，因此自雇收入消失了。

Dependency map of the Lean tax code: 2,159 definitions and theorems by depth, in three columns: drafting checks and certificates, the 2025 income tax, and the loophole searches

编写模型的过程中发现了五件事：

  • 公布的《法典》混合了 2025 年和 2026 年的法律。在六处，合并版《法典》已经显示了 2025 年法案中自 2026 年起生效的修正。若不看生效日期注释来阅读，会得出错误的 2025 年税额：AMT 逐步淘汰按 50% 而非 25%，以及尚不适用的慈善下限和分项扣除上限。
  • 同一法案的取整方向相反。新的小费和加班费扣除在收入超过限额后，每满 1,000 美元减少 100 美元，因此多 1 美元收入可能损失 100 美元扣除。新的汽车贷款扣除每 1,000 美元“或其部分”减少 200 美元，取整方向相反，因此它比整数所暗示的提前 999 美元耗尽。
  • 已婚夫妇分开报税可以扣除更多的州和地方税。州和地方税（SALT）扣除设有上限，且上限随收入上升而缩小：联合报税时，收入每超过 500,000 美元 1 美元，上限就减少 30 美分。分开报税时，法律先将上限减半再缩小，因此每 1 美元只减少 15 美分。一对各赚 300,000 美元的夫妇在两张单独税表上最多可扣除 25,000 美元，但在联合报税表上只能扣除 10,000 美元。
  • 税率表不是税收公式。大多数应税收入低于 100,000 美元的人会查阅 IRS 税率表而非自行计算。该表与法律中的公式相差 −5 美元到 +6 美元之间，Lean 证明了这一范围适用于 100,000 美元以下的每一收入水平和每一种申报身份。
  • 一美元可能让你损失 8,046 美元。有些福利在某个界限处直接消失，而非逐渐减少。一个有三个孩子的家庭可能因为投资收入超过 11,950 美元一美元而失去全部 EITC，最高达 8,046 美元。储蓄者抵免（一项退休储蓄抵免）也是如此：一对夫妇各向退休账户存入 2,000 美元，在收入为 47,500 美元时可获得 2,000 美元抵免，而在收入为 47,501 美元时只能获得 800 美元。

3. 用人们已在使用的税务软件进行测试

模型只有给出正确答案才有用。为了检验我们的模型，我们构建了 5,000 个样本家庭，并用四种方式计算每个家庭的 2025 年税款：我们的模型，以及其他团队独立于彼此、也独立于我们构建的三个工具：

  • PolicyEngine-US，一个开源模型，研究人员和政策制定者用它来估算税收和福利变化对家庭的影响；[8]
  • Tax-Calculator，政策模拟库（Policy Simulation Library）的联邦所得税开源模型；[9]
  • UsTaxes，一款免费、开源的自行报税应用。[10]

两千个家庭是普通情况。另外 3,000 个则刻意设置得较为棘手：分开报税的夫妇、寡妇和鳏夫、学生、有 tip 或加班收入的人、IRA 和健康储蓄账户、教育抵免和储蓄者抵免，以及收入超过 100 万美元且有大量投资利得的人。

我们的模型和 PolicyEngine-US 在 5,000 个家庭中的 4,993 个上对每一个数字都一致。其余七个最多相差 11 美元，全部在 EITC 上：我们的模型读取 IRS 印刷的 EITC 表，而 PolicyEngine-US 使用其背后的公式。[11]

Tax-Calculator 在未核实配偶分居（法律要求）的情况下，向分开报税的已婚人士提供了 EITC 以及儿童和被抚养人护理抵免。它还为一位高收入的单独申报者计算了零 AMT，而另外两个计算器算出了 14,881 美元。

UsTaxes 有 14 个 bug，每个都通过重新计算受影响家庭得到确认。它在没有警告的情况下丢弃自雇收入，因为其 2025 年税表从不附上 Schedule C（商业收入表格）。其儿童护理抵免从未进入税表。其 EITC 年龄测试总是通过。其自雇税将配偶的工资计入社会保障税上限。这些 bug 合计影响约六分之一的普通家庭。

这次比对也在我们自己的模型里发现了两处错误。我们没有把自雇利润计入小企业收入20%的扣除额。而且我们总是取标准扣除和分项扣除中较大的那个，尽管法律允许你选择分项扣除一个较小的金额，这在降低AMT时可能划算。修正之后，有一个家庭少缴了2,070美元。这两处错误之所以暴露，是因为两个独立工具彼此一致，却与我们不一致。

4. 一次搜索发现了税务顾问早已在用的漏洞

有了与参考软件匹配的模型，我们就像使用退休规则时那样使用它：把它当作一个不懂任何税务筹划的搜索的“神谕”。第一次搜索为5,000个家庭逐一尝试了常规选项，共计195,787份申报表：

  • 分别申报，以及哪一方配偶持有哪些投资、支付哪些账单、申报哪些子女；
  • 向IRA缴款；
  • 少赚一点；
  • 实现更多或更少的收益。

第二次搜索使用了一个多年期家庭模型，其中加入了儿童税、信托税、Roth转换、强制提款、赠与和死亡。它为四个家庭在34至47年间尝试了约30,000个方案。两次搜索发现的所有重大结果都已存在于筹划文献中：

搜索发现的结果最佳情形已有描述者
企业主分别申报以低于§199A门槛每年6,317美元Kitces[12]
收入较低的一方在单独申报表中申报子女每年3,090美元实务指南[13]
少实现收益以保持在EITC投资限额之下递延5,000美元可省6,798美元IRS Publication 596[11]
分项扣除较小金额以削减AMT每年2,070美元Form 1040说明
在领取社会保障之前的空档年份进行Roth转换一生+84万美元Kitces
给子女发工资，并为他们开设Roth IRA+46万美元Kitces[14]
进行转换，使继承人不会叠加十年期提款+43万–57万美元Journal of Accountancy[15]

与后门Roth一样，这些都没有被描述给搜索。它之所以发现它们，是因为明文写下的规则允许它们。

5. 我们发现的新漏洞

有三项结果未出现在实务来源、IRS指引或税务软件论坛中。

分别申报可以降低社会保障税的税负，即使对同居的夫妻也是如此。 标准建议是，当一方领取社会保障时，同居的夫妻绝不应分别申报。[16] 与配偶同住的单独申报人完全得不到基础金额。但应税福利的上限为福利的85%或临时收入的85%中的较小者，[17],[18] 而搜索找到了对某些夫妻而言该上限使单独申报更便宜的情况。在联合申报中，工作配偶的工资计入临时收入，因此中等工资就已将福利推至85%的上限。在单独申报中，退休人员的福利仅与退休人员自己的收入相比较。在48,000美元福利和60,000美元工资的情况下，夫妻联合申报需缴7,050美元，单独申报需缴5,568美元，少缴1,482美元。第二位复核者手工重算，得到了相同答案。在100,000美元工资时结果反转，因此这个窗口真实存在但很窄。

工资走一份申报表，投资走另一份。 3.8% 的投资收入税适用于投资收入与收入超出 25 万美元（联合申报）或 12.5 万美元（单独申报）部分两者中的较小值。[19] 在联合申报中，工资先占用该门槛。在单独申报中，投资一方配偶的收入不计入另一方的工资，其收益从自己的 0% 档开始。若双方各有约 20 万美元，这样可节省 1,621 美元。每篇解释文章都会给出该门槛。我们没有找到任何一篇描述这种拆分方式或其在何处划算。

Schedule 8812 支付的金额超过法规允许。 这是 IRS 表格与法律之间的差距，而非一种筹划方案。法规对每个合格子女的可退还儿童抵免设定了上限，计算时不包含其他受抚养人的 500 美元抵免。而表格则对合并抵免设定上限，因此在逐步淘汰区间内，当没有剩余税款可吸收时，它会以现金形式退还这 500 美元抵免。[20],[21] 例如：一个孩子和一个其他受抚养人，收入 24 万美元，无剩余税款。法规给出 200 美元，表格给出 700 美元。Lean 证明该表格永远不会低于法规，并且在没有其他受抚养人时与法规完全一致。

6. 为什么一年的税法中不存在大的漏洞

后门 Roth 之所以规模大，是因为两项条款结合完全消除了收入限制，而且资金随后在数十年内免税复利增长。单一年度的个人所得税充满了悬崖和按申报表设定的门槛，但每一个都是有界的：我们发现的最大波动只有几千美元。在数十年间，大的收益来自已经公开发表的操作。我们唯一找不到书面记载的组合是在 Roth 转换的同一年向子女付款，这大约增加 0.5%。我们的猜测是，任何与 Roth 规模相当且未公开的做法，都存在于实体与其所有者之间的价值转移中：合伙企业、S 公司和 C 公司。

7. 其中大部分现在可以自动运行

“长期问题是如何让这种漏洞搜寻工作常规化，例如作为测试套件的一部分。有些方法并非真正可自动化，因为它们需要大量人力和 AI 智能体的工作。”

仍然需要人来决定的是发现结果意味着什么。有些悬崖是故意的。另一些存在于 IRS 的表格中，而非法律中，还有一些来自官方文本的汇编方式，然而：

  • 文本检查是常规的。 新版本只需一次下载和一条命令，它会在上一个版本没有的任何故障上失败，而 git blame 会指出负责的法案。
  • 模型是一次性成本。 一旦编写并证明，它就是一个构建：如果后续更改破坏了已证明的属性，构建就会失败。当法律变化时，只需重写变更的条款。
  • 比较是常规的，一旦输入映射正确。让它们正确才是困难的部分，而同样的比较发现了每一个映射错误。

局限

  • 覆盖范围。 该模型涵盖家庭记录的 2025 年个人所得税。它遗漏了单年度申报表上的儿童税、28% 和 §1250 收益、外国收入、被动活动规则以及大多数 AMT 优惠项。多年模型保持 2025 年法律不变。
  • 谁检查了什么。 起草分诊和审查由 AI 智能体对照官方文本完成，尚未经过律师或注册会计师的检查。
  • 一致不等于真相。当四个计算器都给出相同结果时，它们可能共享同一个误读。定理和 IRS 示例测试才是对模型本身的检验。

代码、证书、对比和搜索都在 global-law 的 lean-proofs 文件夹中。[3]

参考文献

  1. Alan Yahya，《数学的自动形式化与法律之比较》（Lexifina，2026年9月7日）<lexifina.com/blog/auto-formalisation-of-law>
  2. Alan Yahya，《用 LEAN 证明搜索美国税法漏洞》（Lexifina，2026年11月9日）<lexifina.com/blog/searching-the-tax-code-for-loopholes>
  3. Lexifina，global-law，lean-proofs <github.com/lexifina/global-law/tree/main/lean-proofs>
  4. 法律修订顾问办公室，《美国法典：下载》（发布点 119-138）<uscode.house.gov/download/download.shtml>
  5. Alan Yahya，《美国法典的 Git 版本管理》（Lexifina）<lexifina.com/blog/git-for-the-us-code>
  6. 美国国税局，Rev Proc 2024-40 <www.irs.gov/pub/irs-drop/rp-24-40.pdf>
  7. 《为落实 H. Con. Res. 14 第二编而制定的和解法案》，Pub L 119-21（2025年7月4日）<www.congress.gov/bill/119th-congress/house-bill/1>
  8. PolicyEngine，policyengine-us（版本 2.116.9）<github.com/PolicyEngine/policyengine-us>
  9. Policy Simulation Library，Tax-Calculator（版本 6.8.5）<github.com/PSLmodels/Tax-Calculator>
  10. UsTaxes（提交 49cd0f2，2026年11月7日）<github.com/ustaxes/UsTaxes>
  11. 美国国税局，第 596 号出版物，《劳动所得抵免》（2025）<www.irs.gov/publications/p596>
  12. 《小企业主的第 199A 条 QBI 扣除策略》（Kitces.com）<www.kitces.com/blog/small-business-owner-section-199a-qualified-business-income-qbi-deduction-strategies/>
  13. 《已婚单独申报的儿童税收抵免》（Taxstra）<taxstra.com/child-tax-credit-married-filing-separately/>
  14. 《家族企业中雇佣子女的税务规则》（Kitces.com）<www.kitces.com/blog/tax-rules-hiring-children-family-business-flsa-tax-savings-standard-deduction-roth-contribution/>
  15. 《避免继承 IRA 带来的高额税单》（Journal of Accountancy，2026年5月）<www.journalofaccountancy.com/issues/2026/may/avoiding-a-big-tax-bill-on-inherited-iras/>
  16. 《我和妻子是否应分开报税，以避免为其福利缴纳所得税？》（Maximize My Social Security）<www.maximizemysocialsecurity.com/ask-larry/should-my-wife-and-i-file-separate-tax-returns-avoid-paying-income-taxes-her-benefits>
  17. 美国国会研究服务处，《社会保障：福利征税的计算与历史》（RL32552）<www.everycrsreport.com/files/20150120_RL32552_fa08c40941ceb4e9565c7c7cbd9a4e8e8ba46cdc.html>
  18. 美国国会研究服务处，《P.L. 119-21 中社会保障福利征税与老年人扣除：简报》（R48613）<www.everycrsreport.com/reports/R48613.html>
  19. 26 USC § 1411 <www.law.cornell.edu/uscode/text/26/1411>
  20. 26 USC § 24(d), (h)(4)–(5) <www.law.cornell.edu/uscode/text/26/24>
  21. 美国国税局，附表 8812（表格 1040）（2025 年）<www.irs.gov/forms-pubs/about-schedule-8812-form-1040>

来源：Hacker News · lexifina.com

推理能力数据与训练论文研究#论文/研究#推理#数据/训练