Kavram kanıtı, ABD federal vergi formlarını kaynak gösterilen, makinece doğrulanabilir veriye dönüştürüyor

Proje ne yapıyor

GitHub'daki emmilco/us-tax-model adlı kavsum kanıtı deposu, ABD federal bireysel gelir vergisinin formlar ve talimatlar katmanını herkese açık, kaynak gösterilen, makinece doğrulanabilir veri olarak sunduktan sonra Hacker News ana sayfasına ulaştı. Projenin ilk istemcisi, rehberli bir kendi kendine beyan hazırlama görüşmesi: bir kişiye sorular soruyor, hangi formların geçerli olduğuna karar veriyor, bunları hesaplıyor, her değeri açıklıyor ve kişinin kendisinin gönderdiği bir değerler sayfası geri veriyor. Projenin dokümantasyonuna göre yazılım hiçbir beyanı göndermiyor, imzalamıyor ya da iletmiyor ve hiçbir beyan verisi makineden dışarı çıkmıyor. Özellikle belirtmek gerekir ki, kodlanan şey IRS'nin yayımlanmış prosedürü, İç Gelir Kanunu'nun (Internal Revenue Code) kendisi değil.

Güvenilmek için değil, denetlenmek için tasarlandı

Kodlama büyük ölçüde dil modeli ajanları tarafından yazıldı ve proje, kimin yazdığı nedeniyle bu koda güvenilemeyeceği konusunda açık sözlü. Bunun yerine, yapıyı, yazarların hiçbirine güvenmeyen birinin yalnızca depodan yola çıkarak önemli olan her şeyi denetleyebilmesi şeklinde kurgulanmış.

Her form veya çalışma sayfası bir YAML dosyası; her satırda bir kimlik, basılı satır numarası, IRS etiketi, tür, tek bir ifade ve okunduğu arşivlenmiş sayfanın belge adı, vergi yılı, revizyon, konum belirteci ve hash'ini içeren bir kaynak atfı taşıyor. Herhangi bir satır, parametre, koşul veya soru kaynak atfından yoksunsa derleme başarısız oluyor ve bir doğrulama betiği her alıntıyı ve konum belirtecini arşivlenmiş metinle karşılaştırıyor. 2025 kaynak atıfları raporu 2.313 çapa ve 1.252 alıntıyı kapsıyor; 305 hesaplanan satır konum belirteci segmenti ise doğrulanamayacak kadar kaba olduğu için işaretlenmiş durumda.

Her hesaplanan satır, toplama, sıfırda tabanlanan çıkarma, küçüğü seçme, oranla çarpma, yuvarlama, tablo arama ve koşullu seçme gibi yaklaşık yirmi küçük işlemden oluşan kapalı bir söz dağarındaki tam olarak tek bir atomu uyguluyor. Kullanıcı tanımlı fonksiyon, döngü, değişken, dizi ya da özyineleme yok. Derleme zamanı denetleyicisi daha sonra askıda kalan referansları, döngüleri, sent, oran, sayı ve boolean arasındaki tür karışıklıklarını ve koşullu alternatiflerdeki herhangi bir boşluğu ya da örtüşmeyi reddediyor.

Okunabilirlik ve kesinliği hedefleyen iki ek katman daha var. Bir görüntüleyici her satırın İngilizcesini, resmi etiket ve kaynak atfının yanında IRS çalışma sayfası dilinde yazıyor; böylece bir veri değişikliği incelemede okunabilir bir İngilizce diff olarak görünüyor. Aritmetik yalnızca tamsayılarla: para birimi tamsayı sent, oranlar tamsayı çiftleri ve değerlendirici kayan noktalı sayı kullanmaksızın BigInt ile çalışıyor. Yuvarlama yalnızca kaynak atfıyla belgelenmiş bir talimat yuvarlama dediği yerde yapılıyor ve çözümlenmemiş okumalar ayrı bir belirsizlikler dosyasına kaydediliyor.

Biçimsel ispatlar ve dürtmeleyici test

Depo, her atomu tamsayılar üzerinde tanımlayan, yukarı-yarı-yuvarlamanın eşkuvvetliliği gibi özellikleri ispatlayan ve sonlanması ile deterministik olması ispatlanmış bir referans değerlendirici içeren bir Lean biçimselleştirmesi barındırıyor. TypeScript ve Lean değerlendiricileri her fixture ve üretilmiş beyan üzerinde çalıştırıldı: 1.648 vaka ve karşılaştırılan 2.895.826 satır değeri, sıfır farkla.

Proje bunun neyi ispat etmediğini de hemen belirtiyor. Değerlendiricilerin uyuşması verinin doğru olduğunu değil, değerlendiricilerin uyuştuğunu gösteriyor. Projenin tipik örneği BUG-0001: 1040 Formu 9. satır, 3a'nın yanında 3b'yi de toplamıştı ve dışarıdan bir motor yakalayana dek her iki değerlendirici de yanlış toplamla aynı sonucu veriyordu.

Kodlamayı kaynağa karşı yoklamak için, depoya erişimi ve ağı olmayan yalıtılmış modeller çalışma sayfalarını yeniden yazıyor, üretilmiş İngilizce metni arşivlenmiş sayfalarla karşılaştırıyor ve dal kapsayan girdileri elle işliyor; her anlaşmazlık, alıntısı kaydedilerek sayfa aleyhine karara bağlanıyor. Üretilen beyanlar ayrıca üç bağımsız motordan geçiriliyor — PolicyEngine-US 2.49.4, Tax-Calculator 6.8.5 ve OpenTaxSolver 23.06 — 1.700 beyan boyunca ve her satır düzeyindeki farkın kaynak atıflı bir nedene bağlanması gerekiyor. Güncel raporda açıklanmamış fark yok, ancak motorlardan ikisi öncelikli olarak satır düzeyinde değil özet satırlarına ulaşıyor.

Dürüst sınırlar

Kanıt raporuna göre 1.515 hesaplanan satırın 198'i — yüzde 13,1 — şu anda Claude model ailesi dışından en az bir doğrulamaya sahip; şimdiye dek kaydedilmiş sıfır insan elle çalıştırma ve sıfır insan kaynak okuma katkısı var. 2441 Formu'nun eksik olan üç STOP çıktısı hâlâ katkısız ve form düzeyinde incelemesi bekliyor. Proje bu skor tablosunu ilk sırada basıyor ve dış doğrulama kapsamını hareket ettirmeye çalıştığı tek sayı olarak görüyor.

Neden önemli

Vergi hazırlama, tek bir yanlış satırın para kaybına ya da cezaya yol açabildiği, ama kuralların çoğunlukla düz yazı olarak var olduğu bir alan. Bu proje, o düz yazıyı küçük, denetlenebilir bir biçimsel sisteme dönüştürme konusunda ciddi bir girişim: kapalı bir işlem söz dağarı, arşivlenmiş sayfa hash'lerine inen kaynak atıfları, makinece doğrulanmış ispatlar ve yerleşik motorlara karşı dürtmeleyici test. En az bunun kadar kayda değer olanı, yapay zekâ tarafından üretilmiş koda yaklaşımı — kimseyi model yazımı kodlamalara güvenmeye çağırmak yerine, doğrulamayı yazarlıktan bağımsız kılmaya çalışıyor ve kendi hatalarını ve eksiklerini yayımlıyor. Yaklaşım ölçeklenirse, aritmetiği herkesin denetleyebildiği vergi yazılımına ve diğer düzenlenmiş alanlarda LLM tarafından üretilmiş biçimselleştirmeleri doğrulamak için yeniden kullanılabilir bir şablona işaret ediyor.