AI 수학 자동형식화, 근본적 신뢰성 문제 제기
원제: Navier–Stokes Lost in Translation
왜 중요한가
AI의 수학 증명 능력이 연구·산업 전반에 적용되기 시작한 시점에, 검증 파이프라인의 신뢰성 공백이 공식 확인됐다.
2026년 10월 6일, 케임브리지대 등 소속 Alexander Bastounis 외 2인이 arXiv에 논문을 게재해, AI 자동형식화(autoformalisation)가 자연어 수학 증명을 Lean 같은 형식언어로 번역할 때 의미적 충실도를 보장할 수 없다고 밝혔다. OpenAI의 Navier-Stokes 방정식 블로업 증명 발표를 구체적 사례로 분석했다.
이 논문은 AI 자동형식화의 구조적 한계를 수학적으로 규명한다. 핵심 주장은 이렇다. 자연어(NL) 수학 텍스트의 모호성을 해소해 의미적으로 충실한 번역을 수행하는 문제는, Solvability Complexity Index(SCI) 계층에서 SCI = ∞에 해당한다. 이는 정지 문제(Halting Problem, SCI = 1)보다 계산 복잡도가 높다는 뜻이다. 즉, 어떤 계산 가능한 방법으로도 완전한 의미 보존 번역이 보장되지 않는다.
저자들은 이 이론적 결과를 실제 사례로 뒷받침한다. 논문은 AI가 NL 수학 진술과 증명을 Lean으로 번역하는 과정에서 발생한 오역 사례 다수를 제시하며, OpenAI가 발표한 Navier-Stokes 방정식 해의 블로업 증명을 직접 분석한다. 분석 결과, Lean으로 형식화된 증명이 OpenAI가 공개한 자연어 증명과 대응하지 않는다는 점을 구체적으로 보여준다. Lean 검증이 통과됐다고 해서 원래 자연어 증명이 옳다는 결론으로 이어질 수 없다는 것이다.
이 논문은 25페이지 분량으로, 수학 편미분방정식(PDE), 인공지능(AI), 논리학(Logic) 분야를 교차하며 논증을 전개한다. 자동형식화 기반 AI 수학 검증의 신뢰성 자체에 근본적 의문을 제기한다는 점에서 학계의 주목을 받고 있다.