구글 딥마인드, AI·Lean 검증으로 에르되시 미해결 문제 9건 해결

구글 딥마인드 연구진이 대형언어모델의 증명 탐색과 Lean 검증을 결합한 ‘알파프루프 넥서스(AlphaProof Nexus)’의 연구 결과를 공개했다. 8일 사이언스에 실린 논문에 따르면 미해결 에르되시 문제 353개 중 9개와 정수 수열 관련 추측 492개 중 44개를 해결했다.

알파프루프 넥서스는 AI가 증명 후보를 만들고 증명 보조 도구 Lean이 각 논리 단계를 검사하는 과정을 반복한다. 그럴듯한 수학적 설명을 내놓는 것과 검증을 통과한 증명을 얻는 것을 구분하는 방식이다.

연구진은 에르되시 미해결 문제 353개를 대상으로 탐색해 9개를 자율적으로 해결했다고 논문에서 밝혔다. 온라인 정수 수열 백과사전(OEIS)의 미해결 추측 492개 가운데 44개에 대해서도 증명을 얻었다. 두 결과는 각각 평가한 문제 집합 안에서의 성과로, 수학 난제를 전반적으로 해결한다는 뜻은 아니다.

논문은 같은 접근법을 조합론, 최적화, 그래프 이론, 대수기하학, 양자광학 연구에도 적용하고 있다고 설명했다. 대형언어모델의 생성과 Lean 검증을 번갈아 수행하는 기본적인 에이전트도 에르되시 문제에서 얻은 성과를 재현했다고 보고했다.

구글 딥마인드는 공식 GitHub 저장소에 Lean으로 형식화한 증명과 사람이 작성한 자연어 증명을 공개했다. 저장소에는 에르되시 문제와 OEIS 추측뿐 아니라 여러 수학 분야에서 연구자와 협업한 결과가 구분돼 있다. Lean 4 환경에서 증명을 다시 빌드하고 검증하는 절차도 안내했다.

공개 결과 저장소에는 성공한 문제만 담겨 있다. 연구진은 별도 자료에 시도한 에르되시 문제 목록을 두고, 풀지 못한 문제를 포함한 OEIS 평가 대상과 Lean 정리명 대응표도 연결했다. 성공 사례만으로 성능을 판단하지 않도록 평가 대상과 결과를 함께 살필 수 있게 한 것이다.

이번 연구의 핵심은 AI의 증명 탐색을 기계가 검사할 수 있는 결과와 연결했다는 데 있다. 검증 대상은 Lean으로 표현된 정리다. 자연어 설명을 읽는 것만으로 증명의 타당성을 판단하는 방식과 달리, 공개된 코드와 검증 절차로 논리적 결과를 확인할 수 있다.

출처: Science 연구 논문 https://www.science.org/doi/10.1126/science.aej2213 · Google DeepMind 공식 증명 저장소 https://github.com/google-deepmind/alphaproof-nexus-results