AI가 수학 논문 722편 공개…증명은 얼마나 믿을 수 있나

오픈AI가 대형언어모델로 만든 수학 논문 722편을 공개했어요. 논문은 372개 연구 결과로 묶였고, 결과 하나를 도출하는 데 최첨단 AI 모델 가동 시간은 약 3시간이 들었어요. 하지만 8일 오후 2시20분 기준으로 결과 3개는 철회됐고, 십여 개 증명은 수정·보완됐어요.

이번 공개를 보는 시선은 성과의 규모와 검증의 방식에서 갈려요. 엄상일 기초과학연구원 이산수학그룹 CI는 오래된 유명 난제, 오랜 추측의 반례, 새로운 알고리즘이 제시됐다고 주장되는 점에 많은 수학자가 놀라는 것 같다고 말했어요. 백형렬 KAIST AI수학대학원장 겸 수리과학과 교수는 주요 결과들이 검증된다면 수학계가 받을 충격이 매우 클 것이라고 평가했어요.

검증의 핵심 도구로는 린 형식화가 거론돼요. 린은 사람이 쓴 수학 명제를 컴퓨터가 읽는 형식으로 옮겨 증명 과정을 점검하는 도구예요. 이번 논문 중 린 형식화가 연결된 비율은 42% 정도예요. 린은 자신이 읽을 수 있는 명제가 증명됐는지는 보증하지만, 그 명제가 논문이 내세운 주장과 같은지는 사람이 읽어 확인해야 해요.

엄상일 CI는 린 형식화가 연결되지 않은 논문에서는 오류 가능성을 배제할 수 없다고 봤어요. 백 교수도 AI가 증명을 많이 내놓는 것만으로는 부족하며, 기존 연구에서 무엇을 가져왔고 무엇을 새로 했는지를 분명히 밝히고 수학자 공동체의 지식으로 자리 잡아야 한다고 강조했어요.