"AI로 세법 공식화함"… 美 국세청 세금 양식을 기계 검증 데이터로 만든 깃허브 프로젝트

요약 미국 국세청(IRS)의 복잡한 연방 소득세 양식과 작성 지침을 기계가 검증하고 실행할 수 있는 데이터 구조로 정형화한 오픈소스 프로젝트 'us-tax-model'이 해커뉴스에 공개되어 개발자 커뮤니티의 관심을 모았습니다. 제작자는 이 프로젝트가 LLM(대형 언어 모델) 에이전트를 대거 활용해 구축된 '바이브 코딩(vibe-coded)' 결과물이라고 밝혔습니다. 동시에 작성자인 AI를 무조건 신뢰할 수 없다는 전제하에, 외부 의존 없이 저장소 내부 데이터만으로 모든 계산 규칙과 출처를 엄격히 검증할 수 있도록 다층 검증 아키텍처를 설계했다고 설명했습니다. 프로젝트의 핵심 검증 체계는 철저한 데이터화와 정형 검증에 있습니다. 모든 세무 양식 라인은 원본 IRS 문서의 판본, 인용 위치, 원문 해시값과 1:1로 매핑되는 YAML 데이터로 관리되며, 인용 검증 도구(tools/citations.py)를 통해 수천 건의 앵커와 인용문 일치 여부를 빌드 시점에 확인합니다. 또한 세금 계산식은 복잡한 사용자 정의 함수나 루프 대신 합계, 감산, 최솟값 비교 등 사전에 엄격히 정의된 약 20여 개의 기본 연산(Closed atom vocabulary)만 사용하도록 제한했습니다. 부동소수점 오차를 원천 차단하기 위해 모든 금액은 정수 센트 단위로 처리되며, 정리 증명 언어인 린(Lean)을 통해 연산자의 수학적 성질과 결정론적 종료를 공식 증명했습니다. 실제로 린(Lean)과 타입스크립트(TypeScript) 기반의 두 평가 엔진을 1,600개 이상의 테스트 케이스와 289만 건이 넘는 라인 값에 교차 실행한 결과 단 하나의 오차도 발생하지 않았습니다. 해당 소프트웨어는 사용자의 세무 데이터를 외부로 전송하거나 국세청에 직접 대리 제출하지 않고 로컬에서만 동작합니다.