딥마인드 알파프루프 넥서스: 50년 넘은 에르되시 난제 9개 해결과 토너먼트식 증명의 비결

핵심 메시지

• 딥마인드의 새 AI '알파프루프 넥서스'가 에르되시 미해결 난제 약 350개 중 9개를 한 문제당 수백 달러 비용으로 풀었다.
• 풀이는 사람이 Lean(형식 수학 언어)으로 문제와 답의 틀을 적고 증명만 비워 두면, AI가 그 증명을 채우는 방식이다.
• 핵심 혁신은 '심판 AI'로, 두 풀이를 읽고 더 나은 쪽을 골라 ELO 점수를 매기는 토너먼트를 돌린다.
• 가장 점수가 높은(덜 틀린) 풀이에서 다시 시작하길 반복해, 검증기가 통과시킬 때까지 형식 증명을 완성한다.
• 신뢰할 수 없는 AI를 반복 실행하고 거짓말 못 하는 심판으로 거르면, 신뢰할 수 있는 시스템을 만들 수 있다.

쉽게 이해하기

헝가리 수학자 폴 에르되시는 1000개가 넘는 미해결 문제를 세상에 남겼다. 딥마인드의 새 AI '알파프루프 넥서스'는 그중 약 350개에 도전해 9개를 풀었다. 실패율 95.7%라는 숫자만 보면 초라하지만, 수십 년간 누구도 풀지 못한 문제들이고 한 문제당 비용이 수백 달러 수준이라는 점에서 매우 놀라운 성과로 평가된다.

발표자는 4년 전 GPT-3는 덧셈도 못한다던 흐름을 떠올리며, '지금이 아니라 두 편의 논문 뒤를 보라'는 '논문 제1법칙'을 적용한다. 매년 'AI가 아직 이것도 못한다'던 기준이 빠르게 무너져 왔다는 것이다.

방법의 토대 자체는 새롭지 않다. 환각(거짓 풀이)을 막기 위해 형식 수학 언어 Lean으로 증명이 옳은지 기계적으로 검증하는데, 이는 이미 모두가 쓰는 방식이다. 새로운 점은 그 위에 얹은 절차다. 수학자가 Lean으로 문제와 해답의 틀을 적되 증명은 비워 두면, AI 에이전트가 풀이를 시도하고 다른 AI가 왜 부족한지 평가한다.

진짜 핵심은 값싼 '심판 AI'다. 이 심판은 두 풀이를 읽고 둘 다 틀렸더라도 조금이라도 더 나은 쪽을 고른다. 체스처럼 각 풀이에 ELO 점수를 매기고, 가장 점수가 높은 '나쁜 풀이'에서 다시 시작하는 토너먼트를 검증기가 통과시킬 때까지 반복한다. 결국 불안정한 AI를 거듭 돌리고 거짓말 못 하는 심판으로 거르면, 신뢰할 수 없는 부품으로 신뢰할 수 있는 시스템을 만들어낸다.

발표자는 AI 이야기의 흐름이 바뀌었다고 짚는다. 이제는 모델을 더 똑똑하게가 아니라 모델을 감싸는 하니스(루프)를 더 촘촘하게 만드는 것이 중요하다. 다만 한계도 있다. 형식화하기 쉬운 350개만 골랐다는 선택 편향이 있고, 작은 모델은 한 문제도 풀지 못해 코어에는 여전히 강력한 모델이 필요하다는 점이 드러났다.

주요 인사이트

• AI 발전의 무게중심이 '모델을 더 똑똑하게'에서 '모델을 감싸는 루프(하니스)를 더 촘촘하게'로 옮겨가고 있다.
• 거짓말(환각)을 막기 위해 정답을 기계적으로 검증할 수 있는 형식언어 Lean을 쓰는 것은 이제 표준에 가깝다.
• 진짜 새로움은 두 풀이의 우열만 가리는 값싼 심판 AI로, 둘 다 틀려도 더 나은 쪽을 골라 점진적으로 개선한다.
• 작은 모델은 한 문제도 못 풀었다는 점은, 벤치마크에서 근소해 보여도 코어에는 강력한 모델이 필요함을 시사한다.
• 형식화하기 쉬운 350개만 골랐다는 선택 편향이 있으나, 시작점으로서의 성과 자체는 충분히 의미가 크다.

자주 묻는 질문

관련 AI 소식