이 글은 프로그래밍 언어 Lean을 활용하여 미국 내부 국세법(Internal Revenue Code) 전체를 형식화하는 방법을 제시합니다. 이를 통해 법률 텍스트에 숨겨진 모순점과 오류를 찾아낼 수 있으며, 실제로는 138개의 초안 오류가 발견되었습니다. 이 시스템은 버전 관리된 기록을 기반으로 법규의 변경 사항을 추적하고 검증할 수 있습니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 HN OpenAI Codex의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기어제 우리는 알려진 세금 허점을 Lean 검색을 통해 식별할 수 있음을 확인했습니다. 오늘은 미지의 허점(버그)을 찾기 위해 전체 내부 국세법(Internal Revenue Code)을 형식화하는 작업을 진행했습니다.
Lean은 타입 체커(type checker)가 수학적 증명을 확인할 수 있는 프로그래밍 언어입니다. Lean이 증명을 받아들이면, 모든 단계는 정의에서 파생되며 아무것도 맹신할 필요가 없습니다. 이전 게시물에서는 이러한 종류의 형식화가 법률 분야에서 얼마나 멀리까지 도달할 수 있는지 논의했으며,[1] 어제 우리는 은퇴 계좌 규칙에 이를 적용하여 '백도어 로스(backdoor Roth)'를 재발견했습니다.[2]
이 작업은 버전별 입법 및 판례 기록을 담고 있는 CC0 리포지토리인 global-law의 일부입니다.[3] 우리의 주장은 AI와 증명 검사기를 법률의 버전 관리된 기록에 적용하면, 사람들이 놓치는 모순점과 기계적인 실수를 찾아낼 수 있다는 것입니다. 특히, 우리는 텍스트상의 오류를 포착하고 규칙이 무엇을 허용하는지, 심지어 우연히 무엇을 허용하는지를 확인할 수 있습니다. 이를 위해 법률의 각 섹션을 해당 법규의 원문 표현에 가깝게 Lean으로 번역했으며, IRS가 양식과 지침서에 인쇄하는 작업 예제와 비교 테스트를 수행했습니다.
세법은 US Code의 Title 26입니다. 공식 텍스트는 하원(House of Representatives)에서 법전을 편찬하는 사무소인 법률 개정 자문관실(Office of the Law Revision Counsel)에 의해 구조화된 데이터로 게시됩니다.[4] 우리는 2026년 11월 3일자 최신 버전을 사용했습니다.
이후 파서가 '단락 (2)의 소항 (b)', '그러한 하위 단락(such subparagraph)', '섹션 922부터 927까지'와 같이 단어로 작성된 모든 상호 참조를 포함하여 모든 교차 참조를 읽습니다. 이들은 하이퍼링크가 없습니다. Lean은 각각을 확인합니다. 해당 조항이 존재하는지? 여전히 효력이 있는지?(버전별 기록을 통해 검증 가능) 이러한 점검은 테스트 스위트(test suite)로 실행되며, 이전 버전에서는 문제가 없었던 오류를 새로운 릴리스가 추가할 때마다 실패합니다.
이 시스템은 총 257개의 발견 사항을 보고하며, 각 항목은 공식 텍스트 및 편집자 주석에 대해 AI 에이전트에 의해 검사되었습니다: 98개는 의도된 것(과거 기간의 규칙 및 제정되었으나 아직 발효되지 않은 조항), 21개는 편집자가 만든 하이퍼링크상의 오탐지, 그리고 138개의 실제 오류입니다:
| 오류 유형 | 개수 | 예시 |
|---|---|---|
| 폐기되거나 이동했거나 재작성된 것에 대한 참조로, 일치하는 변경 사항이 없는 경우 | 67 | §1(f)(7)(A)는 재작성된 조항인 §168(n)(2)(G)를 인용함 |
| ... |
138개의 각 오류에는 증명서가 첨부되어 있습니다: 공식 XML에서 증거를 가져와 오류를 입증하는 짧은 Lean 진술입니다. 폐기된 참조의 경우, 증거는 인용된 조항 하에 실제로 존재하는 모든 항목 목록입니다. Lean은 약 2분 반 만에 138개 전체를 재검사합니다.
미국 법전(US Code)에 대한 우리의 기록은 git 히스토리이며, 공법 하나당 하나의 커밋으로 구성되어 있어,[5] 각 오류가 어떤 법률에 의해 작성되었는지 추적할 수 있습니다. 제26편(Title 26)의 경우 기록이 1994년 판까지 거슬러 올라갑니다.
이 검사는 반복하기에 비용이 적게 듭니다. 법전의 새로운 출판본마다 실행하면, 오류가 나타나는 즉시 플래그를 지정하고 이를 유발한 법률을 명시합니다.
다음으로 우리는 법이 계산하는 내용을 기록했습니다: 즉, 2025년 한 가구의 연방 소득세로, 이는 2025년 7월에 One Big Beautiful Bill Act가 만든 변경 사항을 포함하여 Form 1040 상의 숫자를 의미합니다.[6],[7] 우리는 이를 네 부분으로 나누어 진행했습니다:
**소득(Income)**부터 조정 총소득(Adjusted Gross Income, AGI)까지입니다. AGI는 IRA 기여금이나 학생 대출 이자 등 몇 가지 항목을 제외한 총소득액입니다. 대부분의 다른 세법 규칙은 AGI에 의존합니다.**공제 항목(Deductions)**에는 표준 공제 또는 항목별 공제, 그리고 팁, 초과 근무 수당, 자동차 대출 이자 및 만 65세 이상 인원에 대한 새로운 공제 항목이 포함됩니다.**세금 자체(The tax itself)**에는 높은 소득자가 공제 항목을 통해 세금을 너무 많이 줄이는 것을 막는 두 번째 계산 방식인 대체 최소세(Alternative Minimum Tax, AMT)가 포함됩니다.**세액공제(Credits)**로는 아동 세액공제(child tax credit)나 저소득 및 중산층 근로자를 위한 소득세 공제(Earned Income Tax Credit, EITC) 등이 있습니다.
저희는 AI를 사용하여 이 법규정을 Lean 언어로 번역했습니다. 이는 정보 손실이 발생할 수 있는 단계이므로, 다음과 같은 조치들을 통해 이를 보강했습니다:
Lean이 궁극적으로 추가하는 것은 샘플 기반이 아닌 모든 입력값을 포괄하는 증명입니다. 예를 들어, 소득이 증가할 때도 SALT 한도액(SALT cap)이나 자동차 대출 및 초과 근무 수당 공제액이 어떤 소득 수준과 신고 상태에서도 절대 늘어나지 않음을 증명합니다.
다른 세무 소프트웨어와의 비교는 논리적 오류를 포착하는 데 도움을 줍니다. 이를 통해 저희 자체 모델에서 두 가지 실수를 발견할 수 있었습니다. 또한, 산술적인 오류가 아닌 논리적인 버그를 다른 도구들에서도 찾아냈습니다. Tax-Calculator는 배우자들이 별거했는지 여부를 확인하지 않고도 EITC를 분리 신고자에게 지급하며, UsTaxes는 2025년 신고서에 Schedule C를 절대 첨부하지 않아 자영업 소득이 사라지는 문제가 발생합니다.
모델을 작성하는 과정에서 다섯 가지 사항이 드러났습니다:
발표된 법전은 2025년과 2026년의 법을 혼합하고 있습니다. 통합 법전(consolidated Code)에는 이미 2026년에 시작되는 2025년 법 개정 사항이 여섯 곳에 걸쳐 나타나고 있습니다. 효력 발생일 주석 없이 읽으면, 잘못된 2025년 세금(예: AMT의 단계적 축소액을 25%가 아닌 50%로 계산하거나, 자선 기부 한도 및 항목별 공제 상한액)이 제시됩니다. 이들은 아직 적용되지 않는 사항들입니다.같은 법안은 반대 방향으로 반올림합니다. 새로운 팁(tips) 및 초과 근무 수당 공제는 기준을 초과하는 매 1,000달러의 소득당 100달러씩 줄어들기 때문에, 소득이 1달러만 늘어나도 공제가 100달러나 비용이 될 수 있습니다. 새로운 자동차 대출 공제는 '또는 그 일부(or portion thereof)' 기준 매 1,000달러당 200달러씩 줄어드는 반면, 이는 반대 방향으로 계산되어 제시된 정수보다 999달러가 더 빨리 소진됩니다.부부는 별도로 신고할 경우 주 및 지방세(SALT)를 더 많이 공제받을 수 있습니다. 주 및 지방세(SALT) 공제액은 상한선이 있으며, 이 상한선은 공동 신고 시 소득이 50만 달러를 초과할 때마다 30센트씩 줄어듭니다. 별도 신고의 경우, 법률은 상한선을 축소시킨 후 그 금액을 절반으로 줄입니다. 따라서 소득 1달러당 단지 15센트만 줄어드는 것입니다. 각각 30만 달러를 버는 부부는 두 개의 별도 신고서로 최대 25,000달러까지 공제받을 수 있지만, 하나의 공동 신고서로는 10,000달러에 불과합니다.세금표(Tax Table)가 세금 공식은 아닙니다. 소득세 과세 대상 소득이 10만 달러 미만인 대부분의 사람들은 계산하는 대신 IRS 세금표를 참고합니다. 이 표는 법률상의 공식과 최대 −5달러에서 +6달러까지 차이가 나며, Lean은 10만 달러 미만의 모든 소득 및 모든 신고 상태에 대해 이 범위가 사실임을 증명합니다.1달러가 8,046달러의 비용을 초래할 수 있습니다. 일부 혜택은 점진적으로 감소하는 것이 아니라 한 지점에서 완전히 사라집니다. 자녀가 세 명인 가구는 투자 소득이 11,950달러를 1달러 초과했을 때 전체 EITC(Earned Income Tax Credit)를 최대 8,046달러까지 잃을 수 있습니다. 은퇴 저축에 대한 공제인 saver’s credit도 같은 방식으로 작동합니다. 각각 퇴직 계좌에 2,000달러씩 넣은 부부는 소득이 47,500달러일 때는 2,000달러를 받지만, 소득이 47,501달러가 되면 800달러만 받게 됩니다.## 3. 이미 사용 중인 세무 소프트웨어와의 테스트
모델은 정확한 답을 제공할 때만 유용합니다. 저희의 모델을 검증하기 위해, 저희는 5,000개의 샘플 가구를 만들고 각 가구의 2025년 세금을 네 가지 방식으로 계산했습니다: 저희 모델로, 그리고 다른 팀들이 자체적으로 개발한 세 가지 도구로 각각 독립적으로 계산했습니다:
PolicyEngine-US: 연구원과 정책 입안자들이 세금 및 복지 변화가 가구에 미치는 영향을 추정하는 데 사용하는 오픈 소스 모델입니다[8]. Tax-Calculator: Policy Simulation Library의 연방 소득세(federal income tax)에 대한 오픈 소스 모델입니다[9]. UsTaxes: 사용자가 직접 세금 신고를 준비할 수 있는 무료 오픈 소스 앱입니다[10].
2,000개의 가구는 일반적이었습니다. 나머지 3,000개 가구는 의도적으로 복잡한 경우였습니다: 별도로 신고하는 부부, 미망인 및 사별자, 학생, 팁이나 초과 근무 수당이 있는 사람, IRA(Individual Retirement Accounts)와 건강 저축 계좌(health savings accounts), 교육 및 저축 크레딧 관련 항목, 그리고 대규모 투자 수익을 가진 연 소득 100만 달러 이상의 경우였습니다.
저희 모델과 PolicyEngine-US는 5,000개 가구 중 4,993개 가구의 모든 수치에 대해 일치했습니다. 나머지 7개 가구는 최대 $11까지 차이가 나며, 이 금액은 모두 EITC(Earned Income Tax Credit)에서 발생합니다. 저희 모델은 IRS가 인쇄한 EITC 표를 읽어들이는 반면, PolicyEngine-US는 그 뒤에 숨겨진 공식(formula)을 사용합니다[11].
Tax-Calculator는 법률이 요구하는 배우자들이 실제로 떨어져 살고 있는지 확인하지 않고도 별도로 신고하는 부부에게 EITC와 자녀 및 부양가족 양육 크레딧(child and dependent care credit)을 지급했습니다. 또한, 다른 두 계산기가 $14,881을 계산한 한 고소득의 단독 신고자에게는 AMT(Alternative Minimum Tax)를 전혀 계산하지 않았습니다.
UsTaxes는 14개의 버그를 가지고 있었으며, 각 버그는 영향을 받은 가구를 재계산하여 확인되었습니다. 이 앱은 사업 소득 양식인 Schedule C를 2025년 신고서에 첨부하지 않기 때문에 경고 없이 자영업 소득(self-employment income)을 누락합니다. 또한 자녀 양육 크레딧이 신고서에 반영되지 않습니다. EITC의 연령 테스트는 항상 통과됩니다. 그리고 자영업세는 배우자의 급여를 사회보장세(Social Security tax) 상한액 계산에 포함시킵니다. 이 버그들이 결합되어 약 6가구 중 1가구의 일반 가구에 영향을 미칩니다.
비교 결과는 우리 모델 자체의 두 가지 실수도 발견했습니다. 우리는 자영업 소득에 대한 20% 공제액 계산 시 자영업 이익을 포함하지 않았습니다. 또한 법은 더 적은 금액으로 항목별 공제를 선택할 수 있게 하지만, 우리는 항상 표준 공제와 항목별 공제 중 더 큰 금액만 취했습니다. 이는 대체최소세(AMT)를 낮출 때 유용할 수 있습니다. 이를 수정하자 한 가구는 2,070달러 적게 납부해야 했습니다. 두 가지 실수 모두 독립적인 두 도구가 우리보다 서로에 동의했기 때문에 드러났습니다.
참조 소프트웨어와 일치하는 모델을 사용하여, 우리는 은퇴 규칙(retirement rules)에 사용했던 것처럼 이를 활용했습니다. 즉, 세금 계획(tax planning)을 전혀 모르는 검색 엔진의 오라클로 사용한 것입니다. 첫 번째 검색은 5,000가구 각각에 대해 평범한 선택지들을 시도했으며, 총 195,787건의 신고서를 포함했습니다:
두 번째 검색은 키디세(kiddie tax), 신탁 과세(trust taxation), 로스 전환(Roth conversions), 필수 인출금(required withdrawals), 증여 및 사망을 추가하는 다년 가족 모델을 사용했습니다. 이 모델은 34년에서 47년에 걸쳐 네 가구에 대해 약 30,000개의 계획을 시도했습니다. 두 검색이 발견한 모든 큰 내용은 이미 기획 문헌(planning literature)에 나와 있습니다:
| 검색 결과 | 최적 사례 | 이미 설명된 출처 |
|---|---|---|
| 사업주가 §199A 기준 이하로 신고하기 위해 별도로 신고함 | 연간 6,317달러 | Kitces[12] |
| ... |
백도어 Roth와 마찬가지로, 이들 중 어느 것도 검색에 설명되지 않았습니다. 규칙 자체가 명확하게 작성되어 허용하기 때문에 그것들이 발견된 것입니다.
세 가지 결과는 실무자 자료(practitioner sources), 국세청(IRS) 지침 또는 세금 소프트웨어 포럼에서 발견되지 않았습니다.
별도로 신고하는 것이 함께 거주하는 부부의 사회보장세(Social Security) 세금을 절감할 수 있습니다. 일반적인 조언은 사회보장 혜택을 받는 사람이 있을 경우 함께 사는 부부는 절대 따로 신고해서는 안 된다는 것입니다.[16] 배우자와 함께 살았던 별도 신고자는 기본 금액이 전혀 없습니다. 하지만 과세 대상 혜택은 혜택의 85%와 임시 소득(provisional income)의 85% 중 더 적은 금액으로 제한되며,[17],[18] 검색 결과는 이 상한선 때문에 별도 신고가 더 저렴해지는 부부들을 찾아냈습니다. 공동 신고 시, 일하는 배우자의 급여가 임시 소득에 포함되므로, 보통 수준의 급여만으로도 혜택을 최대치인 85%까지 끌어올립니다. 반면, 별도 신고 시에는 은퇴자의 혜택이 오직 그 은퇴자 자신의 소득과 비교하여 측정됩니다. 혜택이 $48,000이고 급여가 $60,000일 경우, 부부는 공동으로 $7,050를 내고 별도로는 $5,568를 내어 $1,482 적게 납부합니다. 두 번째 검토자가 손으로 재계산했을 때도 같은 답이 나왔습니다. 급여가 $100,000일 때는 결과가 바뀌므로, 그 범위는 실재하지만 좁습니다.
한 신고서에 급여, 다른 신고서에 투자금. 투자 소득세(investment income) 3.8%는 공동으로 $250,000을 초과하는 소득액 또는 별도로 $125,000을 초과하는 소득액과 투자 소득 중 더 적은 금액에 적용됩니다.[19] 공동 신고 시에는 급여가 먼저 그 기준점을 사용합니다. 별도 신고 시에는 투자 배우자의 소득이 다른 배우자의 급여를 제외하며, 그들의 수익은 자신만의 0% 구간에서 시작됩니다. 각각 약 $200,000일 경우, 이는 $1,621을 절약해 줍니다. 모든 설명 자료는 이 기준점을 제시합니다. 하지만 분리(split)에 대해 설명하거나 어느 지점에서 비용 절감이 발생하는지에 대한 내용은 찾지 못했습니다.