AI 수학 증명 검증의 함정, 자동형식화는 신뢰할 수 없다

핵심 요약

• AI가 자연언어 수학 증명을 Lean 같은 형식 언어로 자동 번역하는 '자동형식화'가 수학 검증에 널리 쓰이고 있으며, OpenAI의 나비에-스토크스 방정식 해의 폭발성 증명도 이 방식으로 검증되었다.
• 그러나 이 논문은 형식 언어로 검증된 증명이 원래 자연언어 증명의 정확성을 보장하지 않음을 보인다.
• 문제는 자연언어 수학 텍스트의 모호성을 해결하려면 의미론적으로 충실한 번역이 필수인데, 이 모호성 해결 문제가 계산 복잡도 계층(Solvability Complexity Index)에서 무한 수준(SCI = ∞)에 위치한다는 것이다.
• 즉, 완벽한 AI 자동형식화는 정지 문제(SCI = 1)보다도 훨씬 어려운 문제이며, 이론적으로 불가능한 수준의 난제다.
• 논문은 Lean으로 번역된 증명이 원래 자연언어 증명과 일치하지 않는 구체적 사례들을 제시하며, OpenAI의 나비에-스토크스 증명도 이런 불일치의 예로 든다.
• 결론적으로 형식 언어 검증이 통과했다고 해서 그것이 원래 수학 증명의 정확성을 의미하지는 않으며, 번역 과정에서의 근본적인 한계를 무시할 수 없다.