나비에-스토크스 방정식, 번역의 벽에 갇히다

AI 요약

arXiv에 제출된 논문으로, AI 자동 형식화(autoformalisation)를 통한 Lean 검증이 자연어 증명의 정확성을 보장하지 않는다는 문제를 제기한다. 저자들은 자연어 수학 텍스트의 모호성을 해결하는 문제가 계산 가능성 계층에서 임의로 높은 위치(SCI = ∞)에 있어, 정지 문제보다도 어렵다고 주장한다. OpenAI가 발표한 나비에-스토크스 방정식 폭발 해 증명 사례를 포함해, AI가 자연어를 Lean으로 잘못 번역한 여러 실제 사례를 제시한다.

핵심 포인트

• 자연어 수학 텍스트의 모호성 해결 문제는 SCI 계층에서 SCI = ∞로, 정지 문제(SCI = 1)보다 어려움
• OpenAI가 발표한 나비에-스토크스 방정식 해 폭발 증명의 Lean 형식화가 자연어 증명과 대응하지 않음
• AI 자동 형식화의 의미론적 충실 번역이 사실상 불가능할 수 있음을 실증적으로 제시
• 논문은 25페이지, 4개 그림 포함, 2026년 10월 6일 제출

향후 전망

• AI 생성 수학 증명의 신뢰성 검증 방법론에 대한 근본적 재검토 필요
• Lean 등 형식 검증 도구의 한계를 인식한 새로운 검증 프레임워크 개발 촉구