수학계가 OpenAI가 공개한 719편의 AI 생성 수학 원고를 어디까지 믿을 수 있는지 근본적인 의문을 제기하고 있다. 최근 한 논문이 OpenAI가 앞서 발표한 나비에-스토크스 증명이 컴퓨터가 검증한 Lean 코드와 정확히 맞지 않는다고 지적하면서다.
핵심 포인트
- 부호(sign) 오류가 드러나면서 OpenAI의 AI 수학 원고는 722편에서 719편으로 줄었다.
- 영국 수학자 3인은 나비에-스토크스 증명에서 서면 증명과 Lean 코드가 어긋나는 지점을 두 곳 찾아냈다.
- 논문 저자들은 증명 자체가 틀렸다고 단정하진 않지만, 기계 검증만으로는 동료 평가(peer review)를 대체할 수 없다고 강조한다.
OpenAI의 AI 수학 공개
OpenAI는 10월 6일 대규모 수학 증명 모음을 공개했다. 이후 목요일에 나온 한 분석 보고서는, 이 작업이 독립 수학자 패널이 AI 연구소들을 위해 제시한 가이드라인에서 벗어난 부분이 있다고 지적했다. 최초 공개 당시 카탈로그에는 722편이 실려 있었지만, OpenAI는 그중 세 편에서 부호 오류가 발견돼 한 논리 전개가 붕괴되고, 그 논리에 의존한 추가 두 편까지 문제가 생기자 이들을 철회했다.
해당 가이드라인은 9인으로 구성된 Advisory Group on Mathematics and Artificial Intelligence가 9월 29일 발표했다. 첫 문장부터 연구소들에 “고급 수학 문제를 비공개 상용 모델로 시험하지 말 것”을 요구한다. 반면 OpenAI 저장소는 이번 논문들이 비공개 내부 모델을 미공개 연구 문제에 적용한 결과물이라고 밝히고 있다.
전체 결과 가운데 모델의 추론 과정을 요약한 설명이 붙어 있는 것은 10편에 불과하다. 최종 주요 결과 중 약 42%만 수학 증명을 기계가 검증할 수 있는 프로그래밍 언어인 Lean으로 형식화돼 있다.
함께 읽기: Anthropic CEO는 연 얼마나 벌까? IPO 서류가 밝힌 보상 패키지
나비에-스토크스 증명, 어디에서 어긋났나
런던 킹스칼리지의 **알렉산더 바스투니스(Alexander Bastounis)**와 케임브리지대의 파비안 치르첼리(Fabian Circelli), **안데르스 한센(Anders Hansen)**은 OpenAI가 지난 9월 ‘해결했다’고 발표한 나비에-스토크스 방정식 관련 증명을 면밀히 검토했다. 이들은 서면으로 작성된 논문과 Lean 코드가 서로 달라지는 지점을 두 곳 찾아냈는데, 그 중 하나에서는 Lean 코드가 논문이 주장하는 것보다 더 약한 형태의 추정식만을 증명하고 있는 것으로 드러났다.
저자들은 서면 증명이 옳은지 그른지에 대해선 판단을 유보했다. 쟁점은 더 좁다. Lean이 최종 정리 자체가 성립함을 확인해 줄 수는 있지만, 사람이 읽는 중간 단계 논증이 모두 타당한지까지 보증하지는 못한다는 것이다. 따라서 이런 유형의 AI 보조 증명 역시 결국 인간 동료 평가 과정을 거쳐야 한다고 강조한다.
필즈상 수상자인 **테렌스 타오(Terence Tao)**는 10월 6일, 글을 통해 현재 문제들이 “AI 프롬프터”들에 의해 풀리고 있지만, 이들이 결과를 충분히 이해하지 못해 질의응답이나 세미나 발표조차 제대로 수행하기 어려운 상황이라고 비판했다. 자문단 일원이자 하버드대 교수인 멜라니 매쳇 우드(Melanie Matchett Wood) 역시, 이런 결과들이 공개되는 시점에는 “아직 어느 누구도 전체를 이해하고 있지 못하며, 이제부터가 진짜 작업의 시작”이라고 말했다.
OpenAI 증명, 신뢰 공방으로
자문단은 OpenAI가 권고사항을 얼마나 따랐는지 최종 판단할 주체는 넓은 의미의 수학 커뮤니티 전체라고 선을 그은 상태다. 이번 검증 논란은 이미 긴장감이 고조된 한 달을 지나 맞이한 것이다.
OpenAI는 9월 8일 나비에-스토크스 결과를 발표했는데, 곧바로 뉴욕대 수학자 **트리스탄 버크마스터(Tristan Buckmaster)**와의 공로 배분 갈등으로 이어졌다. 발표 사흘 뒤에는 25명의 필즈상 수상자가 공동 선언문을 내고, 대량 생산되는 AI 수학 결과물이 학문 생태계에 해를 끼칠 수 있다고 경고하기도 했다.
