AI 자동 형식화, 정지 문제보다 어려워… OpenAI Navier-Stokes 증명 검증 신뢰성 훼손

Alexander Bastounis, Fabian Circelli, Anders C. Hansen이 작성한 새로운 arXiv 논문은 Lean과 같은 형식 검증 도구를 사용해 AI 생성 수학적 증명을 검증하는 것의 신뢰성에 의문을 제기한다. 저자들은 자연어(NL)를 형식 코드로 변환하는 자동 형식화(autoformalisation) 과정에서 본질적인 의미 모호성으로 인해 형식 증명이 원래 자연어 논증과 일치함을 보장할 수 없다고 주장한다.

자동 형식화의 계산적 한계

핵심 논거는 Solvability Complexity Index (SCI) 계층 구조에 기반한다. 논문은 수학 자연어 텍스트의 모호성을 해결해 의미적으로 충실한 번역을 달성하는 것이 SCI 계층 구조에서 임의로 높으며, 구체적으로 **SCI = ∞**임을 입증한다. 이는 충실한 AI 자동 형식화가 정지 문제(Halting problem)(SCI = 1)를 포함한 모든 표준 계산 문제보다 계산적으로 더 어렵다는 것을 의미한다.

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

저자들은 이 이론을 OpenAI가 발표한 Navier-Stokes 방정식 해의 폭발(blow-up) 증명을 적용한다. 형식 Lean 증명이 자연어 증명과 일치하지 않는 AI 오역의 구체적 사례를 제시한다. 따라서 Lean 코드에 대한 기계적 검증은 Navier-Stokes 방정식에 관한 원래 자연어 논증의 정확성에 대해 신뢰성을 제공하지 못한다.