Dùng Lean kiểm chứng toàn bộ luật thuế Mỹ, tìm 138 lỗi

Một dự án nghiên cứu đã dịch toàn bộ Bộ luật Thuế vụ Mỹ (Internal Revenue Code, tức Title 26 của Bộ luật Hoa Kỳ) sang Lean, ngôn ngữ lập trình có trình kiểm tra kiểu (type checker) đồng thời kiểm chứng được các chứng minh toán học. Mục tiêu không phải học thuật thuần túy: nếu Lean chấp nhận một chứng minh thì mọi bước đều suy ra từ định nghĩa, không có gì được tin tưởng suông. Áp dụng vào luật, điều đó nghĩa là có thể chỉ ra chính xác chỗ văn bản luật tự mâu thuẫn hoặc dẫn chiếu sai.

Minh họa kiểm chứng hình thức bằng Lean

Công trình nằm trong global-law, một kho lưu trữ theo giấy phép CC0 chứa luật và án lệ có đánh phiên bản. Trước đó, nhóm đã dùng Lean để kiểm tra các quy định về tài khoản hưu trí và một tìm kiếm mù đã tái phát hiện thủ thuật "backdoor Roth". Lần này, họ chuyển từng điều khoản của luật thuế sang Lean, giữ sát ngôn ngữ của điều luật, và đối chiếu với các ví dụ mẫu mà Sở Thuế vụ Mỹ (IRS) in trên biểu mẫu và hướng dẫn.

138 lỗi soạn thảo trong văn bản luật thuế

Văn bản chính thức của Title 26 được Văn phòng Cố vấn Sửa đổi Pháp luật (thuộc Hạ viện Mỹ) công bố dưới dạng dữ liệu có cấu trúc. Nhóm nghiên cứu dùng bản phát hành hiệu lực đến ngày 3/11/2026, rồi viết bộ phân tích (parser) đọc mọi dẫn chiếu chéo, kể cả những dẫn chiếu viết bằng chữ như "paragraph (2) of subsection (b)", "such subparagraph" hay "sections 922 through 927" — vốn không có siêu liên kết. Lean kiểm tra từng dẫn chiếu: điều khoản được trỏ tới có tồn tại không, còn hiệu lực không (đối chiếu qua lịch sử phiên bản).

Bộ kiểm thử báo 257 phát hiện, mỗi phát hiện được một tác tử AI đối chiếu với văn bản chính thức và ghi chú biên tập: 98 trường hợp là có chủ đích, 21 là báo động giả trong siêu liên kết của chính ban biên tập, và 138 lỗi thật:

• 67 lỗi dẫn chiếu tới điều khoản đã bị bãi bỏ, chuyển chỗ hoặc viết lại mà không có sửa đổi tương thích, ví dụ §1(f)(7)(A) dẫn tới một điều khoản đã bị viết lại, §168(n)(2)(G) dẫn tới điều khoản đã chuyển chỗ.
• 24 lỗi chính tả, sai phân mục hoặc sai tên đạo luật, ví dụ §1400Z-2(f)(1) dẫn sai tiểu mục, §72(t)(2)(A)(viii) có lỗi chính tả trong dẫn chiếu.
• 8 lỗi sai cấp bậc từ ngữ, ví dụ §9818(a)(1)(A) gọi một tiểu mục là "paragraph".
• 9 lỗi hai điều khoản trùng số hiệu, ví dụ §1202(b)(4) và §45X(d)(4) mỗi số xuất hiện hai lần.
• 30 lỗi ngoặc đơn không bao giờ đóng, trong đó 13 chỗ đã được ban biên tập chú thích, 17 chỗ chưa.

Mỗi lỗi trong 138 lỗi đều có một "chứng chỉ": một câu lệnh Lean ngắn mang bằng chứng từ XML chính thức và chứng minh lỗi tồn tại. Với một dẫn chiếu chết, bằng chứng là danh sách đầy đủ những gì thực sự tồn tại dưới điều khoản được trích. Lean kiểm tra lại cả 138 chứng chỉ trong khoảng hai phút rưỡi.

Vì hồ sơ Bộ luật được lưu dưới dạng lịch sử git, mỗi commit ứng với một đạo luật công khai, nên mỗi lỗi đều truy được về đạo luật đã tạo ra nó. Với Title 26, hồ sơ lùi về tận bản năm 1994. Đây là điểm quan trọng: phép kiểm tra rất rẻ để chạy lại, và khi chạy trên mỗi bản phát hành mới, nó báo lỗi mới ngay khi xuất hiện, kèm tên đạo luật gây ra.

Viết lại thuế thu nhập thành mã có thể kiểm chứng

Bước tiếp theo là mô hình hóa phần luật quy định cách tính: thuế thu nhập liên bang năm 2025 cho một hộ gia đình, tức các con số trên mẫu Form 1040, bao gồm thay đổi từ đạo luật One Big Beautiful Bill Act ban hành tháng 7/2025. Mô hình chia làm bốn phần:

• Thu nhập đến mức thu nhập chịu thuế điều chỉnh (AGI) — tổng thu nhập trừ một số khoản như đóng góp IRA và lãi vay sinh viên. Phần lớn quy tắc thuế khác đều phụ thuộc vào AGI.
• Các khoản khấu trừ: khấu trừ tiêu chuẩn hoặc khấu trừ theo từng khoản, cùng các khoản khấu trừ mới cho tiền tip, tiền làm thêm giờ, lãi vay mua xe và người trên 65 tuổi.
• Bản thân thuế, gồm cả thuế tối thiểu thay thế (AMT) — một cách tính thứ hai nhằm ngăn người thu nhập cao lạm dụng khấu trừ.
• Các khoản tín dụng, như tín dụng thuế trẻ em và tín dụng thuế thu nhập lao động (EITC) dành cho người thu nhập thấp và trung bình.

Bước dịch luật sang Lean do AI thực hiện và đây là khâu "gây mất mát thông tin", nên nhóm gia cố bằng ba biện pháp: đối chiếu từng phần với số liệu IRS công bố (bảng thuế, bảng EITC, các bảng tính và ví dụ trong ấn phẩm hướng dẫn), so sánh với ba chương trình thuế độc lập trên 5.000 hộ, và cho một tác tử thứ hai không tham gia viết phần đó rà soát đối kháng, tìm cả lỗi lẫn các kiểu "gian lận" như viết mã để đạt kiểm thử thay vì tuân theo luật.

Điều Lean mang lại mà phần mềm thường không có là chứng minh phủ mọi đầu vào thay vì chỉ một mẫu. Ví dụ, nó chứng minh rằng mức trần khấu trừ thuế bang và địa phương (SALT), cùng các khoản khấu trừ cho lãi vay xe và tiền làm thêm giờ, không bao giờ tăng khi thu nhập tăng — ở mọi mức thu nhập và mọi tình trạng khai thuế.

Năm phát hiện khi viết mô hình

Quá trình mô hình hóa làm lộ ra những điểm đáng chú ý:

1. Bộ luật hợp nhất trộn luật 2025 với luật 2026. Ở sáu chỗ, văn bản hợp nhất đã thể hiện các sửa đổi của đạo luật 2025 bắt đầu có hiệu lực từ 2026. Đọc mà bỏ qua ghi chú về ngày hiệu lực sẽ ra thuế 2025 sai: mức giảm dần của AMT là 50% thay vì 25%, cùng một ngưỡng sàn từ thiện và mức trần khấu trừ theo từng khoản chưa áp dụng.
2. Cùng một đạo luật làm tròn theo hai hướng ngược nhau. Khoản khấu trừ mới cho tip và tiền làm thêm giờ giảm 100 USD mỗi 1.000 USD thu nhập vượt ngưỡng trọn vẹn, nên thêm một đô thu nhập có thể mất 100 USD khấu trừ. Khoản khấu trừ lãi vay xe giảm 200 USD mỗi 1.000 USD "hoặc phần của 1.000 USD", tức làm tròn ngược lại, nên hết hiệu lực sớm hơn 999 USD so với con số tròn.
3. Vợ chồng có thể khấu trừ SALT nhiều hơn nếu khai riêng. Trần SALT giảm khi thu nhập tăng: 30 cent mỗi đô vượt 500.000 USD với hồ sơ khai chung. Với hồ sơ khai riêng, luật giảm trần trước rồi chia đôi, nên chỉ giảm 15 cent mỗi đô. Một cặp mỗi người kiếm 300.000 USD có thể khấu trừ tới 25.000 USD trên hai hồ sơ riêng, nhưng chỉ 10.000 USD khi khai chung.
4. Bảng thuế không phải công thức thuế. Phần lớn người có thu nhập chịu thuế dưới 100.000 USD tra bảng thuế của IRS thay vì tự tính. Bảng này lệch so với công thức trong luật trong khoảng từ −5 đến +6 USD, và Lean chứng minh được khoảng đó cho mọi mức thu nhập dưới 100.000 USD và mọi tình trạng khai thuế.
5. Một đô có thể "đắt" 8.046 USD. Một số phúc lợi tắt hẳn tại một ngưỡng thay vì giảm dần. Một gia đình ba con có thể mất toàn bộ EITC, tối đa 8.046 USD, chỉ vì thu nhập từ đầu tư vượt 11.950 USD đúng một đô. Tín dụng tiết kiệm hưu trí cũng vậy: một cặp mỗi người góp 2.000 USD vào tài khoản hưu trí nhận 2.000 USD ở mức thu nhập 47.500 USD, và chỉ 800 USD ở mức 47.501 USD.

Đối chiếu với phần mềm thuế đang được dùng

Nhóm nghiên cứu dựng 5.000 hộ mẫu và tính thuế 2025 của từng hộ theo bốn cách: mô hình của họ và ba công cụ do các nhóm khác xây dựng độc lập — PolicyEngine-US, Tax-Calculator (thuộc Policy Simulation Library) và UsTaxes (ứng dụng khai thuế mã nguồn mở miễn phí). Hai nghìn hộ là thông thường; 3.000 hộ còn lại được cố ý tạo tình huống khó: vợ chồng khai riêng, người góa, sinh viên, người có thu nhập từ tip hoặc làm thêm giờ, người có IRA và tài khoản tiết kiệm y tế, người dùng tín dụng giáo dục và tín dụng tiết kiệm, cùng các hộ thu nhập trên 1 triệu USD với lãi đầu tư lớn.

Mô hình của nhóm và PolicyEngine-US khớp mọi con số ở 4.993/5.000 hộ; bảy hộ còn lại lệch tối đa 11 USD, đều ở EITC, do mô hình đọc bảng EITC in sẵn của IRS còn PolicyEngine-US dùng công thức phía sau bảng.

Tax-Calculator mắc lỗi logic: cấp EITC và tín dụng chăm sóc trẻ cho người khai riêng mà không kiểm tra vợ chồng có sống ly thân hay không — điều luật bắt buộc; và không tính AMT cho một người khai riêng thu nhập cao, trong khi hai công cụ khác tính ra 14.881 USD.

UsTaxes có 14 lỗi, mỗi lỗi được xác nhận bằng cách tính lại hộ bị ảnh hưởng. Nó bỏ mất thu nhập tự kinh doanh mà không cảnh báo vì tờ khai 2025 không bao giờ đính kèm Schedule C; tín dụng chăm sóc trẻ không bao giờ vào tờ khai; điều kiện tuổi cho EITC luôn đúng; và thuế tự kinh doanh tính cả tiền lương của vợ/chồng vào mức trần thuế An sinh xã hội. Tính chung, những lỗi này ảnh hưởng khoảng một trong sáu hộ thông thường.

Bản so sánh cũng bắt được hai lỗi trong chính mô hình của nhóm: không tính lợi nhuận tự kinh doanh vào khoản khấu trừ 20% cho thu nhập doanh nghiệp nhỏ, và luôn chọn khoản khấu trừ lớn hơn giữa tiêu chuẩn và theo từng khoản, dù luật cho phép chọn khấu trừ theo từng khoản ít hơn khi điều đó có lợi về AMT. Sau khi sửa, một hộ giảm được 2.070 USD tiền thuế. Cả hai lỗi lộ ra vì hai công cụ độc lập đồng ý với nhau và không đồng ý với mô hình của nhóm.

Sơ đồ minh họa cấu trúc văn bản luật

Tìm kiếm mù và những lỗ hổng chưa từng được ghi lại

Với mô hình đã khớp phần mềm tham chiếu, nhóm dùng nó làm "nhà tiên tri" (oracle) cho một tìm kiếm không biết gì về lập kế hoạch thuế. Tìm kiếm thứ nhất thử các lựa chọn thông thường cho 5.000 hộ, tổng cộng 195.787 tờ khai: khai riêng, vợ hay chồng đứng tên khoản đầu tư nào, trả hóa đơn nào, nhận nuôi con nào; góp IRA; kiếm ít đi một chút; hiện thực hóa lãi nhiều hay ít hơn. Tìm kiếm thứ hai dùng mô hình gia đình nhiều năm, thêm thuế trẻ em (kiddie tax), thuế tín thác, chuyển đổi Roth, khoản rút bắt buộc, quà tặng và thừa kế — thử khoảng 30.000 phương án cho bốn gia đình trong 34 đến 47 năm.

Mọi kết quả lớn mà hai tìm kiếm tìm ra đều đã có trong tài liệu lập kế hoạch thuế: chủ doanh nghiệp khai riêng để xuống dưới ngưỡng §199A (6.317 USD/năm), người thu nhập thấp hơn nhận nuôi con trên tờ khai riêng (3.090 USD/năm), hiện thực hóa lãi ít hơn để nằm dưới hạn mức đầu tư của EITC (6.798 USD khi hoãn 5.000 USD), khấu trừ ít hơn để cắt AMT (2.070 USD/năm), chuyển đổi Roth trong các năm trống trước khi nhận An sinh xã hội (+0,84 triệu USD trong cả đời), trả lương cho con và mở Roth IRA cho con (+0,46 triệu USD), chuyển đổi để người thừa kế không bị dồn khoản rút 10 năm (+0,43–0,57 triệu USD).

Ba kết quả không xuất hiện trong tài liệu hành nghề, hướng dẫn của IRS hay diễn đàn phần mềm thuế:

• Khai riêng có thể giảm thuế An sinh xã hội, ngay cả với cặp vợ chồng sống chung. Lời khuyên phổ biến là không bao giờ khai riêng khi một người nhận An sinh xã hội. Nhưng phúc lợi chịu thuế bị giới hạn ở mức nhỏ hơn giữa 85% phúc lợi và 85% thu nhập tạm tính, và tìm kiếm tìm ra những cặp mà mức trần đó khiến khai riêng rẻ hơn. Với 48.000 USD phúc lợi và 60.000 USD tiền lương, cặp này nợ 7.050 USD khi khai chung và 5.568 USD khi khai riêng, ít hơn 1.482 USD. Ở mức lương 100.000 USD, kết quả đảo chiều, nên "cửa sổ" này có thật nhưng hẹp.
• Lương trên một tờ khai, đầu tư trên tờ kia. Thuế 3,8% trên thu nhập đầu tư áp lên mức nhỏ hơn giữa thu nhập đầu tư và phần vượt 250.000 USD (khai chung) hoặc 125.000 USD (khai riêng). Khi khai chung, tiền lương "ăn" vào ngưỡng trước. Khi khai riêng, thu nhập của người đầu tư không gồm lương của người kia, và lãi của họ bắt đầu trong khung 0% của chính mình. Với khoảng 200.000 USD mỗi người, cách này tiết kiệm 1.621 USD.
• Schedule 8812 hoàn nhiều hơn luật cho phép. Đây là khoảng cách giữa biểu mẫu IRS và luật, không phải một kế hoạch. Luật giới hạn tín dụng trẻ em hoàn lại theo từng con đủ điều kiện, tính không gồm khoản 500 USD cho người phụ thuộc khác. Biểu mẫu lại giới hạn tín dụng gộp, nên trong vùng giảm dần, khi không còn thuế để bù trừ, nó hoàn cả khoản 500 USD bằng tiền mặt. Ví dụ: một con và một người phụ thuộc khác, thu nhập 240.000 USD, không còn thuế phải nộp — luật cho 200 USD, biểu mẫu cho 700 USD. Lean chứng minh biểu mẫu không bao giờ thấp hơn luật và khớp chính xác khi không có người phụ thuộc khác.

Vì sao một năm luật thuế không chứa lỗ hổng lớn

Backdoor Roth lớn vì hai điều khoản kết hợp xóa sạch một giới hạn thu nhập, rồi số tiền sinh lãi miễn thuế trong nhiều thập kỷ. Một năm của thuế thu nhập cá nhân đầy những "vách đá" và ngưỡng tính theo từng tờ khai, nhưng mỗi ngưỡng đều có biên: mức dao động lớn nhất tìm được chỉ vài nghìn USD. Qua nhiều thập kỷ, lợi ích lớn đến từ những nước đi đã được công bố. Tổ hợp duy nhất chưa thấy ai viết ra là trả lương cho con trong cùng những năm chuyển đổi Roth, thêm khoảng 0,5%. Nhóm nghiên cứu phỏng đoán rằng thứ gì đó cỡ Roth mà chưa ai công bố nằm ở nơi giá trị dịch chuyển giữa các thực thể và chủ sở hữu của chúng: hợp danh, công ty S và công ty C.

Phần nào đã có thể chạy tự động

Theo nhóm nghiên cứu, việc còn cần con người là quyết định một phát hiện có ý nghĩa gì — có ngưỡng là cố ý, có ngưỡng nằm trong biểu mẫu chứ không trong luật, có ngưỡng do cách hợp nhất văn bản chính thức. Còn lại:

• Kiểm tra văn bản là việc thường quy. Một bản phát hành mới là một lần tải về và một lệnh, lệnh này thất bại nếu có lỗi mà bản trước không có, và git blame chỉ ra đạo luật chịu trách nhiệm.
• Mô hình là chi phí một lần. Khi đã viết và đã chứng minh, nó là một bản build: nếu thay đổi sau này phá vỡ một tính chất đã chứng minh, bản build thất bại. Khi luật đổi, chỉ cần viết lại các điều khoản đã đổi.
• So sánh là việc thường quy một khi ánh xạ đầu vào đúng — và chính phép so sánh đã tìm ra mọi lỗi ánh xạ.

Nhóm cũng nêu rõ giới hạn: mô hình chỉ phủ thuế thu nhập cá nhân 2025 cho một bản ghi hộ gia đình, bỏ qua kiddie tax trên tờ khai một năm, lãi 28% và §1250, thu nhập nước ngoài, quy tắc hoạt động thụ động và phần lớn các ưu đãi AMT. Việc phân loại soạn thảo và rà soát do các tác tử AI thực hiện, chưa được luật sư hay kế toán công chứng nhận. Và sự đồng thuận không đồng nghĩa với chân lý: nếu cả bốn công cụ cùng hiểu sai một chỗ, chúng vẫn có thể khớp nhau.

Góc nhìn

Với kỹ sư và lập trình viên Việt Nam, giá trị lớn nhất ở đây không phải câu chuyện thuế Mỹ mà là một mẫu thiết kế: đưa các quy tắc nghiệp vụ phức tạp — thuế, bảo hiểm, tuân thủ, thậm chí các điều khoản hợp đồng — vào một ngôn ngữ có thể kiểm chứng hình thức (formal verification), rồi biến việc kiểm tra thành bộ test chạy tự động trong CI. Khi quy tắc thay đổi theo phiên bản và mỗi thay đổi có thể truy vết bằng git, một lỗi dẫn chiếu hay một ngưỡng bị hiểu sai sẽ lộ ra ngay thay vì vài năm sau mới thành sự cố.

Điểm thứ hai đáng học là cách nhóm này đối xử với AI: dùng AI để dịch luật sang mã và rà soát, nhưng không tin AI, mà ràng buộc bằng đối chiếu với dữ liệu chính thức, bằng tác tử thứ hai rà soát đối kháng và bằng so sánh chéo với các hệ thống độc lập. Chính phép so sánh này đã bắt được lỗi của cả mô hình của họ lẫn của các công cụ khác. Với các nhóm đang xây phần mềm có yếu tố pháp lý hoặc tài chính, quy trình "AI viết, nhiều nguồn kiểm chứng, chứng minh phủ toàn miền đầu vào" là hướng đi thực dụng hơn là chờ một mô hình ngôn ngữ đủ tốt để tự đảm bảo tính đúng đắn.