"OpenAI가 풀었다던 수학 난제, 알고보니 AI 오역 덕분?" 검증 허점 폭로 논문 화제

요약 OpenAI가 과거 발표했던 '나비에-스토크스 방정식의 해 폭발(blow-up)' 증명과 관련해, AI의 수학적 자동 형식화(Autoformalisation) 및 검증 프로세스에 심각한 허점이 있다는 연구 논문이 아카이브(arXiv)에 공개되었습니다. 현재 AI를 통한 수학 정리 증명 분야에서는 인공지능이 자연어로 작성된 수학적 논증을 린(Lean)과 같은 정형 언어로 번역하고, 컴퓨터가 이를 기계적으로 무결하게 검증하는 방식이 널리 쓰이고 있습니다. 그러나 연구진(알렉산더 바스투니스 등)은 이러한 번역 과정 자체가 원문의 의미를 온전히 담보하지 못해 검증 결과에 착시가 발생한다고 지적했습니다. 연구진에 따르면 자연어로 된 수학 텍스트의 모호성을 완전히 해소하여 의미론적으로 완벽한 번역을 수행하는 작업은 가산 복잡도(Solvability Complexity Index, SCI)상 무한대(SCI = ∞)에 해당합니다. 이는 정지 문제(Halting Problem, SCI = 1)를 포함한 기존의 모든 계산 문제보다 이론적으로 더 어려운 수준입니다. 논문은 실제 인공지능이 자연어 명제와 증명을 Lean 코드로 옮기는 과정에서 왜곡이 발생하는 다양한 사례를 분석했습니다. 특히 OpenAI가 발표했던 나비에-스토크스 방정식 관련 증명의 경우, Lean으로 형식화되어 통과된 증명이 원래 자연어로 작성된 해의 폭발 증명 내용과 실제로는 일치하지 않는 것으로 드러났습니다. 연구진은 기계적 검증이 통과되었다고 해서 원래의 자연어 수학 증명이 참이라는 보장은 전혀 될 수 없다고 결론지었습니다.