인공지능(AI)이 수학적 텍스트를 형식 언어로 자동 변환하여 증명을 검증하는 방식에 심각한 오류 가능성이 제기되었습니다. 최근 발표된 연구 논문 'Navier-Stokes lost in translation'에 따르면, AI 시스템이 자연어(NL)로 작성된 수학적 논증을 Lean과 같은 형식 언어로 옮기는 과정에서 의미론적 불일치가 발생할 수 있으며, 이는 기계적 검증(mechanical verification)이 원본 자연어 논증의 정확성을 보장하지 못하게 만든다고 지적합니다.
연구진은 이러한 번역 과정의 어려움이 수학적 자연어 텍스트의 모호성을 해결하는 데서 비롯된다고 설명합니다. 수학적 자연어의 모호성을 의미론적으로 충실하게 번역하는 문제는 '솔바빌리티 복잡성 지수(Solvability Complexity Index, SCI)' 계층에서 임의로 높은 수준에 해당하며, 이는 정지 문제(Halting problem)보다도 해결하기 어려운 문제라는 것을 의미합니다. 실제 사례로 OpenAI가 발표한 나비에-스토크스(Navier-Stokes) 방정식 해의 폭발(blow-up) 증명을 들며, 형식화된 Lean 증명이 원본 자연어 증명과 일치하지 않는다는 점을 구체적으로 보여주었습니다.
이러한 연구 결과는 AI 기반 수학 증명 및 자동 형식화(autoformalisation) 기술의 발전에 중요한 시사점을 던집니다. AI가 복잡한 수학적 난제를 해결하는 데 기여할 잠재력은 크지만, 자연어의 미묘한 의미와 맥락을 정확히 이해하고 형식 언어로 변환하는 데는 여전히 상당한 기술적 한계가 존재함을 보여줍니다. 이는 AI가 생성하거나 검증한 수학적 증명을 맹목적으로 신뢰하기보다는, 인간 전문가의 비판적인 검토와 심층적인 이해가 여전히 필수적임을 강조하는 대목입니다.