OpenAI, 나비에-스토크스 증명 과정에서 수학을 코드로 오번역

OpenAI가 Navier-Stokes 문제의 증명을 발표할 때 미묘한 오류를 범한 것으로 보인다고 수학자 팀이 주장했다. 이 오류가 증명이 틀렸다거나 OpenAI가 문제를 올바르게 해결하지 못했다는 것을 의미하지는 않지만, AI 모델이 생성한 수학적 결과를 항상 신뢰할 수 있는지에 대한 의문을 제기한다.

“이러한 대규모 언어 모델이 생성한 모든 증명에 대해 수행해야 할 일은 인간이 이를 읽어야 한다는 것이며, 이는 수학자들에게 엄청난 추가 부담을 줍니다.”라고 University of Cambridge의 Anders Hansen은 말한다.

8 September, OpenAI는 수학에서 가장 유명한 미해결 문제 중 하나인 Navier-Stokes 문제의 해법을 찾았다고 발표했다. OpenAI는 이 증명을 두 가지 버전으로 발표했는데, 하나는 인간 수학자가 작성하는 방식인 영어와 수학 기호가 결합된 “자연어” 버전이고, 다른 하나는 컴퓨터 코드 Lean으로 작성된 버전이다. Lean 증명은 자연어 버전의 형식화로 의도되었으며, 컴퓨터가 모든 논리적 진술이 참인지 기계적으로 검증할 수 있게 한다. 문제는 Hansen과 그의 팀의 말에 따르면, 이 두 버전이 일치하지 않는다는 점이다.

“이 형식화 과정은 동료 검토를 대체하려고 시도하는 것입니다.”라고 팀원 Fabian Circelli(역시 University of Cambridge 소속)는 말한다. “동료 검토는 인간의 눈으로 증명을 살펴보는 것을 의미합니다. 하지만 우리가 이 논문에서 보여준 것은 이러한 유형의 AI 자동 형식화가 동일한 목적을 달성할 수 없다는 것입니다.”

분명히 하자면, 연구원들은 OpenAI가 Navier-Stokes 문제를 해결하는 데 실패했다고 말하는 것이 아니다. Pythagoras’s theorem의 유효한 증명이 수백 가지인 것처럼, 자연어 증명과 Lean 증명 모두 해법을 제공할 가능성은 충분하다. 대신 그들의 주장은 더 미묘한 지점에 있다. 즉, OpenAI의 모델이 Lean으로 변환할 때 “오역”을 했다는 것이다.

“우리는 자연어 증명이 틀렸다고 말하는 것이 아닙니다.”라고 Hansen은 말한다. “또한 그것이 옳다고 말하는 것도 아닙니다.” 문제는 OpenAI가 두 증명을 동일한 것으로 제시하며, Github에 명시한 바와 같이 “이 저장소에는 [논문] ‘Finite time blowup for Navier–Stokes’에 제시된 결과의 Lean 4 형식화가 포함되어 있다”고 했다는 점이다.