Sebuah upaya terbaru menggunakan bahasa pemrograman Lean untuk memformalkan seluruh Internal Revenue Code guna mendeteksi kesalahan dan celah hukum yang belum diketahui. Pendekatan ini menggabungkan kecerdasan buatan dan pemeriksa bukti untuk memindai undang-undang pajak federal Amerika Serikat.
Pemeriksaan Draf dan Celah Undang-Undang
Lean adalah bahasa pemrograman yang penguji tipenya mampu memvalidasi pembuktian matematis secara mutlak berdasarkan definisi tanpa asumsi. Pekerjaan ini merupakan bagian dari repositori global-law yang merekam legislasi dan putusan pengadilan dalam format CC0 seperti dilaporkan Hacker News: Front Page (lexifina.com). Dengan mengarahkan kecerdasan buatan serta pemeriksa bukti ke catatan undang-undang bersejarah, inkonsistensi dan kesalahan mekanis dapat teridentifikasi.
Berdasarkan rilis Undang-Undang Pajak Title 26 per 3 November 2026, sistem parser membaca seluruh referensi silang dan diuji melalui Lean. Dari pengujian tersebut, terdapat 257 temuan yang mencakup 98 aturan sah untuk periode lalu atau masa depan, 21 alarm palsu pada hyperlink editor, serta 138 kesalahan nyata. Setiap kesalahan memiliki sertifikat berupa pernyataan Lean singkat yang membuktikan cacat tersebut berdasarkan data XML resmi.
Pemrograman Pajak Pendapatan dan Perbandingan Perangkat Lunak
Model ini kemudian digunakan untuk menghitung pajak penghasilan federal 2025 bagi rumah tangga, termasuk penyesuaian dari One Big Beautiful Bill Act yang disahkan pada Juli 2025. Perhitungan tersebut mencakup pendapatan hingga AGI, berbagai potongan, perhitungan pajak termasuk alternatif minimum tax, serta kredit pajak. Penggunaan kecerdasan buatan dalam menerjemahkan undang-undang ke Lean divalidasi melalui data IRS dan diuji terhadap tiga program perpangkatan independen pada 5.000 sampel rumah tangga.
Hasil pengujian menunjukkan kesepakatan tinggi, namun juga mengungkap beberapa celah dan inkonsistensi aturan. Sejumlah ketentuan pajak menunjukkan perbedaan pembulatan, aturan pengajuan terpisah yang memengaruhi batasan SALT, serta perbedaan antara rumus undang-undang dan tabel pajak resmi IRS. Pencarian lanjutan juga mendapati strategi penghematan pajak tertentu seperti pengajuan terpisah untuk memangkas pajak Jaminan Sosial serta celah pada formulir Schedule 8812.
Pemeriksaan teks undang-undang kini dapat berjalan secara otomatis melalui unduhan rilis baru dengan bantuan perintah git untuk melacak perubahan. Meskipun model ini memiliki keterbatasan cakupan seperti pengecualian pajak anak tertentu atau pendapatan luar negeri, verifikasi berbasis bukti ini menawarkan metode baru untuk mengaudit kepatuhan dan konsistensi regulasi fiskal.
Sumber: Hacker News: Front Page
