인공지능(AI) 기반의 수학 정리 증명 시스템이 최근 놀라운 발전을 이루었지만, 여전히 중요한 한계에 직면해 있었습니다. 바로 일상적인 자연어 표현을 컴퓨터가 이해할 수 있는 형식 언어(Lean 4)로 정확하게 변환하는 과정에서 발생하는 '엄밀함의 환상'이라는 문제입니다. 표준 타입 검사기는 문법적으로는 올바르지만, 실제로는 가설을 누락하거나, 의미 없는 참을 도입하거나, 수학적 범위를 미묘하게 변경하는 등 의미론적 오류를 포함한 코드도 허용했습니다. 이러한 문제는 AI가 생성한 증명의 신뢰성을 떨어뜨리는 주요 원인이었습니다.
이러한 문제를 해결하기 위해 'Sage'(Semantic Agent-Guided Formalization Engine)라는 새로운 에이전트 기반 프레임워크가 개발되었습니다. Sage는 단일 번역 방식 대신 4단계로 분해된 생성 파이프라인과 이중 신호 의미 교정 루프를 결합한 것이 특징입니다. 이 교정 루프는 Lean 4 컴파일러 진단과 다차원 의미 피드백을 동시에 활용하여, 구문적 유효성뿐만 아니라 수학적 충실도까지 강제합니다. 이를 통해 기존의 단일 방식에서 70.9%에 달했던 '답변 누출'(모델이 검증되지 않은 답을 추측하여 높은 형식화율을 달성하는 현상)을 2.7%까지 억제하는 데 성공했습니다. 결과적으로 Sage는 Omni-MATH 데이터셋에서 73.3%의 컴파일 및 의미 정확도를 달성했으며, 이는 기존의 미세 조정된 Goedel-Formalizer-V2 기준선(42.0%)보다 훨씬 높은 수치입니다.
Sage의 등장은 AI 기반 수학 증명 분야에 중요한 전환점이 될 것으로 보입니다. 특히, 175개의 미형식화된 국제 수학 올림피아드(IMO) 문제로 구성된 새로운 IMO-Unformalized 데이터셋에서 Sage는 기준선(19.4%) 대비 87.4%의 검증된 정확도를 기록하며 뛰어난 제로샷 일반화 능력을 보여주었습니다. 이는 AI가 복잡하고 새로운 수학 문제를 인간 수준으로 이해하고 증명하는 데 한 걸음 더 다가섰음을 의미합니다. 앞으로 Sage와 같은 기술은 수학 연구의 속도를 높이고, 새로운 정리 발견을 돕는 강력한 도구가 될 잠재력을 가지고 있습니다.