케임브리지대학교 수학자들은 OpenAI가 나비에-스토크스 문제의 자연어 증명을 Lean 코드로 옮기는 과정에서 두 버전이 달라졌다고 주장했다. 이 불일치가 어느 쪽 증명이 틀렸다는 뜻은 아니지만, AI가 만든 형식화 증명을 원래 증명의 대체물로 믿을 수 있는지에 의문을 제기한다.

OpenAI는 9월 8일 수학의 대표적인 미해결 문제인 나비에-스토크스 문제를 풀었다고 발표하고, 영어와 수학 기호로 쓴 증명 및 이를 컴퓨터가 검증할 수 있도록 Lean으로 형식화한 증명을 공개했다. 케임브리지대학교의 앤더스 한센(Anders Hansen)과 연구팀은 두 증명이 일치하지 않는다고 지적했다.

문제가 드러난 부분은 증명의 보조정리 8.6이다. 자연어 증명에서는 어떤 값이 정수 m에 대해 m + 4보다 작아야 하지만, Lean 증명에서는 같은 값이 m + 5보다 작아야 한다고 돼 있다. 후자는 허용하는 값의 범위가 더 넓어 수학적으로 더 약한 조건이다. 두 조건이 모두 참일 수는 있어도 같은 주장을 뜻하지는 않는다.

연구팀은 OpenAI가 나비에-스토크스 문제를 풀지 못했다고 주장하는 것은 아니다. 자연어 증명과 Lean 증명이 각각 해법을 제공할 가능성은 있지만, OpenAI가 두 증명을 같은 내용으로 제시한 점이 문제라는 설명이다. OpenAI는 두 버전의 불일치를 알고 있으며, 어느 쪽 증명도 무효라는 뜻은 아니라고 New Scientist에 밝혔다. 자연어 증명에서 오류가 발견되면 바로잡고, 이번 주 공개한 수학 논문 722편의 형식화 작업도 이어갈 계획이라고 했다. 이 가운데 일부에만 Lean 증명이 있으며, Lean 증명도 손으로 대조 검토되지는 않았다고 보도됐다.

한센은 AI가 Lean 코드가 오류 없이 컴파일되도록 증명을 작성하다가, 컴파일되지 않는 부분을 만나면 자연어 증명과 달라지더라도 우회 방법을 찾을 수 있다고 설명했다. 케임브리지대학교의 파비안 치르첼리(Fabian Circelli)는 자동 형식화가 동료 심사를 대신할 수 없다고 말했다. 연구팀은 ChatGPT에 두 증명 사이의 차이를 찾도록 한 뒤 직접 확인했으며, 제안된 차이 중 상당수는 실제로는 일치했다. 진짜 불일치를 확인하는 데 약 2주가 걸렸다. 이는 OpenAI가 에이전트의 증명 생성에 들었다고 밝힌 88시간과 비교된다.

임페리얼 칼리지 런던의 케빈 버저드(Kevin Buzzard)는 정리의 진술과 증명을 구분해야 한다고 지적했다. Lean으로 옮긴 정리의 진술이 맞고 증명 코드가 컴파일된다면 해당 진술의 증명이 맞다고 확신할 수 있지만, 그 사실만으로 PDF에 실린 자연어 증명이 옳다는 점까지 확인되는 것은 아니라는 설명이다. 버저드는 나비에-스토크스 문제가 올바르게 해결됐다고 확신하지만, PDF에 기술된 증명의 정확성에는 훨씬 덜 확신한다고 말했다.

연구팀의 주장은 논문 DOI에 공개돼 있다. 한센은 복잡하고 긴 증명에서는 두 버전을 세밀하게 대조하지 않으면 이런 차이를 알아채기 어렵다며, 신뢰할 수 있는 자동 형식화 기법을 더 개발해야 한다고 말했다.