AI가 수학 논문 722편을 썼습니다, 근데 검증은 누가 하죠?

 

깃허브 레포 하나 때문에 어제 타임라인이 시끄러웠습니다.

주소는 github.com/openai/math. 커밋은 딱 하나. 그 안에 수학 원고 722편이 들어 있습니다. 전부 사람이 아니라 OpenAI 내부 모델이 만든 거고요.

솔직히 저도 처음엔 "또 벤치마크 자랑이겠지" 했거든요. 근데 열어보니 좀 다릅니다.

숫자부터 체감해 보죠

모델한테 문제를 약 4,000개 던졌습니다. 거기서 나온 결과를 추려서 372개 묶음(family) 으로 정리했고, 그게 논문 722편이 됐어요. 한 묶음 안에 주 결과 하나, 그걸 뒷받침하는 논증, 다른 방식의 증명이 같이 들어갑니다.

4,000에서 372. 비율로 보면 10%가 채 안 됩니다. 던진 것 대부분은 쓸 만한 수준이 안 돼서 버려졌다는 뜻이죠.

연산량도 적혀 있습니다. 결과 하나당 평균 "ChatGPT Pro 사고 3시간" 분량. 372개면 단순 계산으로 1,100시간이 넘습니다. 한 대로 쭉 돌렸다면 46일 걸리는 양이에요. 물론 실제로는 병렬로 돌렸겠지만요.

여기까지만 보면 "AI가 수학자 됐네" 소리가 나옵니다.

openai math github repository

근데 README를 끝까지 읽으면

반전은 OpenAI가 직접 써둔 문장에 있습니다.

이 모음에는 검증 단계가 제각각인 결과들이 섞여 있다. 그리고 형식화되지 않은 결과 중 일부에는 문제가 있을 수 있다. 발견되면 빠르게 고치겠다.

자기 발표 자료에 이런 문장을 넣는 건 흔한 일이 아닙니다. 그만큼 722편이 전부 검증 끝난 결과는 아니라는 얘기예요.

여기서 "형식화"가 뭔지 짚고 가야 합니다.

Lean, 증명을 컴파일하는 언어

Lean은 수학 증명을 컴퓨터가 검사할 수 있게 적는 프로그래밍 언어입니다.

자바 짜다가 타입 안 맞으면 빌드 터지잖아요. Lean도 똑같습니다. 증명 논리에 구멍이 있으면 컴파일이 안 돼요. 사람이 읽다가 "음, 여기는 자명하니까" 하고 넘어가는 구간을 기계는 못 넘어갑니다.

그러니까 Lean 형식화가 붙은 논문은 빌드가 통과된 코드고, 안 붙은 논문은 아직 안 돌려본 코드인 셈이죠.

레포에는 "많은 원고가 형식화됐지만 전부는 아니다"라고 적혀 있습니다. 정확히 몇 편인지 숫자는 없고요. 이게 포인트예요. 722라는 숫자보다, 그중 빌드가 통과된 게 몇 편이냐가 훨씬 중요한 정보입니다.

Lean theorem prover code

병목이 생산에서 검증으로 넘어갔습니다

예전엔 수학 논문 한 편 나오는 데 사람이 몇 달, 길면 몇 년 걸렸습니다. 양이 자연스럽게 조절됐죠.

이제는 하루에 722편이 쏟아집니다.

검증은요? 여전히 사람이 합니다. 피어리뷰할 수 있는 수학자 숫자는 어제랑 오늘이 똑같아요.

OpenAI도 이걸 압니다. 공개 방식을 고등연구소(IAS)의 수학·AI 자문그룹과 상의해서 정했고, 결과를 이해하기 위한 워크숍과 학회를 지원하겠다고 밝혔어요. 논문을 던지는 것보다 소화시키는 게 더 어려운 문제라는 걸 인정한 거죠.

이 그림, 개발자는 이미 겪고 있잖아요

AI한테 코드 짜라고 시켜보면 압니다.

금방 나옵니다. PR이 쌓여요. 그런데 리뷰어는 여전히 저 혼자입니다.

생성 속도는 몇십 배 빨라졌는데 검토 속도는 그대로예요. 저도 요즘 이것 때문에 고생합니다. 커밋 수는 늘었는데 "이게 왜 이렇게 돌아가지?" 싶은 코드가 같이 늘어요. 돌아가긴 하니까 머지는 되고요. 그게 더 무섭습니다.

수학계가 지금 겪는 게 딱 이겁니다. 규모만 다를 뿐이에요.

그래서 Lean 같은 도구가 중요해지는 겁니다. 사람이 다 못 읽으면 기계가 먼저 거르는 수밖에 없어요. 테스트 없이 AI한테 리팩터링 맡기는 것과, 테스트 다 깔아놓고 맡기는 것의 차이. 똑같은 얘기입니다.

그래서 뭘 봐야 하냐면

결국 핵심은 숫자가 아니라 검증 비율입니다.

722편 중 Lean으로 검증된 비율이 올라가면 진짜 진전이고, 안 올라간 채 다음 공개가 1,500편으로 늘어나면 그건 그냥 쌓이는 거예요.

레포는 Apache-2.0으로 공개돼 있어서 누구나 받아볼 수 있습니다. 한 번 들어가서 lean/formalization.yaml만 열어봐도 분위기가 보일 겁니다. 리만 제타 함수 영점 자유 영역이나 CM 아벨 다양체에 대한 호지 추측처럼 따로 언급된 결과들이 있는데, 이것들은 공정이 달랐다고 명시돼 있어요.

다음 글에서는 AI 에이전트 얘기를 해볼까 합니다. 논문을 쓰는 AI보다, 내 서버에서 파일을 지우는 AI가 사실 더 급한 문제거든요.