수학 연구에 AI가 본격적으로 뛰어들 수 있다고 기대했던 존 로버(John Loeber)는 자동 정리 증명기를 직접 만들었지만, 기반 모델의 성능이 오르자 자신의 맞춤형 도구가 빠르게 의미를 잃었다고 말한다. 그는 수학의 주요 발견이 AI 중심으로 옮겨갈 가능성을 전망하면서도, 수학을 배우고 이해하는 즐거움은 여전히 남는다고 본다.
로버는 2013년부터 AI가 수학 연구를 맡게 될 것이라고 생각했다. 대형 언어 모델은 수학에 약했지만, 2024년 말 추론 모델이 등장한 뒤 시험 시점 연산을 늘려 수학적 논증을 이어가는 데 진전이 나타났다고 설명한다. 그는 추론 모델의 직관과 증명 능력을 정리 증명기 Lean과 결합하면 증명을 조금씩 만들어갈 수 있다고 봤다. 5월에는 오픈AI가 평면 단위 거리 문제의 증명을 공개했다.
로버는 증명 과정에서 오류를 바로잡기 위해 처음부터 Lean으로 작업하는 자동 정리 증명기를 만들었다. 기존 Lean4의 비공개 포크와 여러 하위 에이전트의 전략 생성·병렬 처리를 관리하는 자체 도구를 개발했고, 그래프 이론 문제에 집중했다. 또 직접적인 증명 전략을 반박할 사례를 찾는 C++ 프로그램을 생성하는 메타프로그램도 만들었다. 그는 분산 연산, 코어 활용, API 호출 제한, 보조 정리의 저장과 검색, 장기간 진행되는 증명 탐색의 상태 관리 등을 다뤘다.
그의 경험에 따르면 GPT-5.5로 새로운 정리를 증명하는 데 진전은 있었지만 속도가 느렸고, 부정확하거나 앞뒤가 맞지 않는 문장과 막다른 증명 전략이 자주 나왔다. GPT-5.6 Sol에서는 올바른 문장과 유용한 전략을 만드는 능력이 크게 나아졌다고 느꼈다. 로버는 무어 그래프 차수가 57인 문제와 하드위거 추측을 풀기 위해 Lean 코드를 수십만 줄 생성했다. 그러나 하드위거 추측의 증명을 마치지는 못했다. 이 모델 간 성능 차이에 대한 평가는 평가 지표로 수치화한 결과가 아니라 그의 인상에 근거한다. 공개 평가인 FrontierMath는 오염 가능성이 있다고 봤고, 비공개 평가도 만들지 않았다고 밝혔다.
GPT-6 Astra가 나온 뒤에는 증명 전략을 세우는 직관이 한층 좋아졌다고 로버는 평가했다. 며칠 뒤 나비에-스토크스 방정식의 존재성과 매끄러움 문제가 해결됐다는 발표가 나오자, 그는 자신의 작업을 중단했다. 약 4주 뒤 오픈AI는 공개되지 않은 새 프런티어 모델을 4,000개의 주요 문제에 적용했다. 문제당 평균 연산량은 ChatGPT-Pro-Thinking 기준 약 3.5시간이었다. 로버는 이를 문제당 최대 약 100달러 정도의 연산량으로 해석했다. 오픈AI가 공개한 수학 저장소는 수백 건의 주요 결과를 주장했으며, 그 가운데 하드위거 추측의 반증도 포함됐다.
로버는 이 변화에서 특히 기반 모델의 개선 속도와 자신이 만든 공학적 도구의 한계를 실감했다고 말한다. 모델을 보조하는 정교한 맞춤형 시스템도 기반 모델이 발전하면 밀려날 수 있다는 것이다. 그는 자신의 작업을 오픈소스로 공개하지 않았으며, 백만 줄의 Lean 정리나 전용 도구를 정리하는 일도 모델이 곧 더 나은 결과를 낼 수 있다고 생각해 무의미하게 느껴진다고 썼다.
그는 변화가 몇 달이나 몇 년에 걸쳐 천천히 진행될 것으로 예상했지만, 일정한 능력 수준을 넘자 주요 결과가 갑자기 쏟아졌다고 회고한다. 인간과 AI가 함께 수학을 연구하는 시기도 짧았다고 본다. 다만 AI가 공개한 증명 가운데 상당수가 먼저 일반 텍스트로 작성된 뒤 일부만 형식화됐다는 관찰은 확인되지 않은 추정이라고 덧붙였다. 그가 보기에는 복잡한 논증을 Lean으로 단계마다 검증해야 한다는 예상과 달리, 모델은 형식화 없이도 논증을 이어가고 나중에 일부를 형식화한 것으로 보인다.
이 글은 존 로버의 전망과 의견을 담고 있다. 그는 AI 이후 수학자의 주요 정리 증명 가능성이 사실상 사라질 수 있다고 보지만, 수학을 배우는 이유는 달라질 수 있다고 말한다. 이미 발견된 증명을 배우는 즐거움은 그대로 남고, 지식 발견의 범위는 크게 넓어질 수 있다는 것이다. 로버는 인간이 수학의 최전선을 직접 확장하는 경쟁과 특권을 잃는 대신, AI가 발견한 영역을 탐구할 수 있다고 본다. 이런 변화가 다른 분야에도 이어질 것으로 예상하면서, 궁극적으로는 긍정적인 전환이 될 수 있다고 전망한다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요