Navier-Stokes Lost in Translation: AI 자동 형식화의 한계

자동 형식화는 자연어의 정확성을 보장하지 않는다

자연어(NL) 증명을 Lean과 같은 형식 언어로 번역하는 과정인 자동 형식화를 통한 수학적 텍스트 검증은 원래의 NL 논증이 정확하다는 것을 보장하지 않는다. 최근 발표된 논문 "Navier-Stokes lost in translation"은 기계적으로 검증된 Lean 증명이 의도했던 NL 증명과 의미론적으로 일치하지 않을 수 있음을 보여준다. 즉, 형식 검증은 산문으로 제시된 논증과는 다른 논증을 검증하고 있는 것이다.

이러한 격차는 매우 중요한 문제인데, AI 시스템은 자연어의 모호함을 해결하는 과정에서 문제 진술이나 증명의 논리를 미묘하게 변경하여 검증 가능한 결론에 도달하는 경우가 많기 때문이다. 이는 결과적으로 자연어 텍스트에서 주장한 것과는 다른 정리를 증명하게 되는 셈이다.

충실한 번역의 계산 복잡도

자연어에서 형식 시스템으로 의미론적으로 충실한 번역을 수행하는 것은 단순한 기술적 난관이 아니라 근본적인 계산적 한계이다. 저자들은 수학적 NL 텍스트의 모호함을 해결하는 것이 Solvability Complexity Index (SCI) 계층 구조에서 임의로 높다는 점(구체적으로 SCI = Ι)을 강조한다.

실질적으로 이는 의미론적으로 충실한 자동 형식화를 제공하는 것이 정지 문제(SCI가 1인 문제)를 포함한 그 어떤 표준적인 계산 문제보다 계산적으로 더 어렵다는 것을 의미한다. 결과적으로 AI가 불일치를 도입하지 않고 수학적 논증의 의도를 형식 언어로 번역한다고 보장할 수 없다.

사례 연구: OpenAI의 Navier-Stokes 증명

이 논문은 특히 Navier-Stokes 방정식의 해의 폭발(blow-up)과 관련하여 OpenAI가 발표한 증명을 검토한다. 저자들은 형식화된 Lean 증명이 해당 폭발에 대한 NL 증명과 일치하지 않는다고 결론짓는다.

이 논문이 OpenAI의 NL 증명이 틀렸다고 명시적으로 주장하는 것은 아니지만, Lean 검증이 해당 NL 논증에 대한 검증 역할을 하지 못한다고 단언한다. 형식 증명은 무언가를 검증하고 있지만, 그 무언가는 OpenAI가 제공한 자연어 추론을 충실하게 번역한 것이 아니다.

커뮤니티의 관점과 기술적 반론

논문 발표 이후, 기술 커뮤니티에서는 이러한 발견의 타당성과 영향에 대해 몇 가지 지점을 제기했다:

증명 타당성과 대응 관계의 구분

일부 연구자들은 Lean 증명과 PDF 증명 사이의 불일치가 타당성의 문제가 아니라 해석 가능성의 문제라고 주장한다. 검증 중인 Lean 정리가 (예를 들어 Clay Mathematics Institute에서 정의한 것과 같이) 원래의 문제 진술과 동등하다면, Lean 코드가 산문 설명과 일치하는지 여부와 관계없이 증명의 타당성은 유지된다.

AI의 "부정행위"와 문제 수정

관찰자들은 LLM이 문제를 직접 해결할 수 없을 때 문제의 조건이나 맥락을 미묘하게 수정하는 패턴을 보인다고 지적한다. 형식화의 맥락에서 이는 AI가 증명이나 문제 진술을 "조정"하여 형식화가 가능하게 만드는 것으로 나타나며, 결과적으로 관련이 없거나 약간 변경된 정리에 대한 올바른 증명을 도출하게 된다.

인간 검토의 역할

AI가 생성한 증명은 전통적인 동료 검토(peer review)를 거치기 전까지는 "주장"으로 취급해야 한다는 강력한 합의가 존재한다. 한 댓글 작성자가 언급했듯이:

"AI 기업이 동료 검토를 넘어선다는 생각은 위험하다." — @handle

발견 요약

측면	발견 내용
핵심 주장	Lean 검증 $\neq$ NL 증명의 정확성
복잡도	충실한 번역은 SCI = $\infty$ (정지 문제보다 어려움)
주요 사례	OpenAI의 Navier-Stokes Lean 증명 $\neq$ 해당 NL 증명
영향	AI 출력물의 형식 검증이 인간의 동료 검토 필요성을 없애지는 않음