Leanを用いて米国税法を形式化し、起草ミスや抜け穴を特定する

研究チームは、法規をLean（数学的証明を検証できる型チェッカーを備えたプログラミング言語）に翻訳することで、米国税法における138件の起草ミスを特定しました。法律を検証可能な定義の集合として扱うことで、チームは、米国法典第26編の公式テキスト内に存在する壊れた相互参照、誤字、および不整合な細分化を自動的にフラグ立てすることができました。

この表は、初期の監査段階で見つかった起草ミスの具体的な例を提供しています。

内国歳入法の自動監査

研究チームは、パーサーを使用して、税法内のすべての相互参照を読み取りました。これには「(b)項の(2)項」のようにプレーンテキストで書かれたものも含まれます。公式テキストではこれらの参照にハイパーリンクがないため、法律が更新される際に「デッドリンク」になりやすいという問題があります。

Leanは、法典のバージョン管理された履歴に対して各参照を検証しました。テストスイートは257件の発見を報告し、その後AIエージェントがそれらを分類しました。多くは過去の期間を意図した規則でしたが、138件は移動した規定への引用や誤った細分化の名前など、実際の欠陥として確認されました。

lexifina.comの報告数値に基づくHN Digest作成の図表。数値は出典の通りに表示。

「私たちの主張は、AIと証明チェッカーを法典のバージョン管理された記録に向ければ、人間が見落とす矛盾や機械的なミスを見つけられるというものです。」

— Formalizing the US tax code | Lexifina

税務ロジックの検証可能なコードへの書き換え

単純なテキストチェックを超えて、チームは2025年の連邦所得税計算をLeanに書き換えました。これには、所得（調整後総所得まで）、控除、税金計算（代替最低税を含む）、および税額控除の4つの異なるコンポーネントのモデリングが含まれます。

この図は、税法を表現するために使用された形式的なLeanモデルの規模と構成を視覚化したものです。

自然言語を形式的なコードに翻訳することは「情報の損失」を伴うステップであるため、チームはIRSが公開した数値および3つの独立した税務プログラムに対するテストを行い、モデルを強化しました。また、アドバーサリアルAIエージェントを導入し、法規を実際に遵守せずにテストをパスするように設計された「ズル」のロジックがないか、コードのレビューを行いました。

隠れた抜け穴とソフトウェアのバグの発見

形式的なモデルにより、チームは税務計画戦略の「ブラインドサーチ」を実行することが可能になりました。これにより、社会保障給付の上限の仕組みにより、同居する夫婦が別々に申告することで節約できる特定の期間など、実務家のガイドには見つからなかった3つの新しい抜け穴が明らかになりました。

このプロジェクトは、既存のツールにおける不一致も露呈させました。例えば、ある人気税務ソフトウェアは申告書にSchedule Cを添付できず、自営業所得が消失する原因となっていました。さらに、チームはIRSの税金表が法律の計算式の完全な反映ではないことを証明し、多くの納税者において最大6ドルの差異があることを示しました。

この表は、研究チームによって明らかにされた特定の抜け穴とソフトウェアのバグを強調しています。

限界と人間の解釈の役割

Leanは法律の逐一的なテキストに対して厳格なチェックを提供しますが、このプロジェクトは重要な境界、すなわち法律の「精神」を浮き彫りにしています。機械はテキストが許可する内容を証明できますが、特定の解釈が法廷において法的に許容されるかどうかについては、人間の裁判官が最終的な裁定者となります。

さらに、法規からコードへの移行は、依然として解釈を伴う手動のプロセスです。研究チームは、Leanによって「所得が上昇するあらゆる入力において特定の控除が決して増加しないこと」を証明できる一方で、法律をそれらの定義に初期翻訳する段階では、形式化が立法意図を正確に捉えているかを確認するために依然として人間の監視が必要であることを指摘しました。