구글 딥마인드의 수학 증명 시스템 AlphaProof Nexus가 Science에 정식으로 실렸다. 논문의 제1저자는 Tsoukalas이며, 연구팀은 모두 딥마인드 소속이다. 이 연구는 5월 말 프리프린트로 먼저 공개됐고, 이번에 동료 심사를 거친 학술지 버전이 나왔다.
성적표는 그대로다. 시스템은 아직 풀리지 않은 에르되시 문제 353개에 도전해 9개를 풀었고, 그중 2개는 56년 동안 미해결로 남아 있던 문제다. 정수열 데이터베이스 OEIS의 열린 추측 492개 중에서는 44개를 증명했다. 이와 별도로 대수기하학에서 힐베르트 함수와 관련해 약 15년간 풀리지 않던 문제에 답했고, min-max 최적화의 기존 경계도 개선했다.
Gemini 하나, Lean 컴파일러 하나
시스템의 기반은 Gemini 3.1 Pro다. 모델이 형식 언어 Lean으로 증명을 초안하면, Lean 컴파일러가 한 단계가 바뀔 때마다 검사하고 오류 메시지를 다음 시도에 그대로 되먹인다. 이 과정에서 사람은 마지막에 결과만 확인한다.
논문은 네 가지 버전을 구분한다.
- A 버전: 가장 소박한 '생성-검증' 루프로, 대형 모델이 쓰고 컴파일러가 판정한다.
- B 버전: A에 딥마인드의 기존 증명기 AlphaProof를 붙여 증명에서 빠진 조각을 보충하게 한다.
- C 버전: 진화 메커니즘을 더해, 여러 서브 에이전트가 증명 초안 풀을 공유하고 Elo 점수로 순위를 매긴다.
- D 버전: 위의 모든 것을 합친 것으로, 에르되시 문제를 공략하는 데 쓰였다.
결과에서 가장 흥미로운 대목은 A 버전도 에르되시 문제 9개를 모두 독자적으로 증명했다는 점이다. 다만 가장 어려운 몇 개에서는 비용이 더 들었다. The Decoder가 인용한 추론 비용은 문제당 수백 달러다. 저자들은 논문에서 이렇게 썼다.
"power of compiler feedback in grounding LLM reasoning"
(컴파일러 피드백은 대형 모델의 추론을 현실에 단단히 붙들어 매는 힘이 있다.)
스페인 학자들의 몇 가지 유보
스페인 과학미디어센터는 논문이 공개된 날 현지 학자 몇 명에게 논평을 받았고, 의견은 둘로 갈렸다.
UAM 연구원 Pablo Haya Coll은 이 방식이 의미 있는 수학적 발견을 체계적으로 만들어 낼 수 있다고 본다. UOC의 Josep Curto는 "a dazzling display of technical capability marred by significant methodological inconsistencies"라고 평가했다. 기술적으로는 눈부시지만 방법론에는 뚜렷한 불일치가 있다는 뜻이다. 그는 세 가지를 짚었다. A 버전과 D 버전이 같은 문제를 풀었다는 점은 프레임워크의 복잡도가 발견 능력을 좌우하지 않을 수 있음을 보여 준다. 비용은 성공한 실행만 계산했고, B 버전과 D 버전의 계산에도 AlphaProof 자체의 추론 비용은 들어 있지 않다. 그리고 Lean이 보장하는 것은 증명이 '적어 놓은 명제'에 대해 성립한다는 것뿐이며, 그 명제가 원래 문제를 충실히 옮겼는지는 여전히 수학자가 직접 대조해야 한다. 논문도 형식화 오류가 있었음을 인정한다.
ICMAT 소장 Javier Aramayona가 우려하는 것은 다른 점이다. '참인 줄은 알지만 아무도 완전히 이해하지 못한' 결과가 대량으로 쏟아지기 시작하면, 수학 연구에서 이해라는 고리와 젊은 연구자의 훈련 과정이 약해질 수 있다는 것이다. 바야돌리드대학의 Teodoro Calonge는 더 직설적으로 이 분야에는 개선할 여지가 상당히 남아 있다고 말했다.
저자들도 적용 범위를 분명히 적었다. 에르되시 문제에서 AI의 전체 성공률은 약 1~2%이고, 푼 문제는 상대적으로 쉬운 것이 많으며, Mathlib 라이브러리의 축적이 두텁고 문제를 하위 목표로 쪼개기 쉬운 조합론, 볼록 최적화, 정수론에 몰려 있다. 대량의 새로운 이론을 만들어 내야 하는 문제에는 시스템이 거의 손을 대지 못한다.
올해의 일들을 이어서 보면
5월에 본지는 OpenAI 모델이 80년 된 에르되시 추측을 풀었다고 보도했다. 9월에는 수학자들과 OpenAI 사이에 공로 표기를 둘러싼 다툼이 일었다. 10월 6일 OpenAI는 GitHub에 AI가 생성한 수학 원고 722편을 한꺼번에 올렸다. 학술지를 거치지 않고 Apache 2.0 라이선스의 오픈소스 저장소를 쓴 방식이었다. The Decoder 보도에 따르면, 이후 테렌스 타오가 이끄는 수학자 단체가 이런 방식에 대한 보이콧을 촉구했다.
두 회사의 경로 차이가 여기서 분명하게 드러난다. OpenAI는 물량이 많고 공개적인 방식을 택해 걸러 내는 일을 커뮤니티에 맡겼다. 딥마인드는 훨씬 적은 수를 택했지만, 하나하나가 Lean 컴파일러를 통과했고 학술지 심사도 거쳤다. 후자는 논문에서 Lean의 위상도 절제해서 규정했는데, 원문 표현으로 형식 검증은 "can serve as a filter for determining which proofs merit human review", 즉 어떤 증명이 사람이 볼 가치가 있는지를 가려내는 필터라는 것이다.
대략 계산해 보자. 문제당 수백 달러라면 에르되시 문제 9개의 추론 비용은 박사후연구원 한 명의 한 달 월급에 훨씬 못 미친다. 하지만 Curto가 짚은 기준대로 실패한 실행과 AlphaProof 호출까지 더하면 장부상 금액이 얼마나 늘어날지, 논문은 아직 수치를 내놓지 않았다. 딥마인드는 증명과 일부 설명을 GitHub의 alphaproof-nexus-results 저장소에 올려 두었고, 외부 수학자들이 하나씩 대조해 볼 수 있다.
참고 출처: Science 학술지 논문, The Decoder, CocoLoop, 스페인 과학미디어센터 전문가 논평. 논문 본문에서 에르되시 문제 353개 중 9개 해결, OEIS 추측 492개 중 44개 증명, 네 가지 에이전트 버전의 역할 분담을 확인했다.