구글 딥마인드, 에르되시 미해결 9문제 푼 AlphaProof Nexus 공개

구글 딥마인드가 LLM과 증명 보조 도구를 결합한 수학 AI '알파프루프 넥서스(AlphaProof Nexus)'로 미해결로 남아 있던 에르되시(Erdős) 문제 9개를 자율적으로 풀었다고 더 런다운 AI가 전했다.

발표는 OpenAI가 80년 된 에르되시 추측 하나를 반증했다고 알린 바로 다음 날 이뤄졌다. 더 런다운 AI는 OpenAI가 한 문제를 푼 데 비해 딥마인드는 그보다 여덟 개 많은 아홉 개 문제를 풀어 답했다고 표현했다.

AlphaProof Nexus는 LLM에 증명 보조기 Lean을 짝지어 기계 검증 가능한 증명을 만든다. 시스템이 증명 후보를 만들면 Lean이 검증하고, 통과할 때까지 이 과정을 반복하는 구조다.

풀어낸 9개 문제는 조합론과 그래프 이론에 걸쳐 있고, 그중 두 문제는 56년 동안 미해결로 남아 있던 난제다. 한 문제를 푸는 데 드는 비용은 수백 달러 수준이라고 회사는 밝혔다.

같은 AI는 정수 수열의 온라인 백과사전(Online Encyclopedia of Integer Sequences)에 올라 있던 열린 추측 44개도 추가로 증명했다.

한계도 있었다. 더 단순한 형태의 에이전트도 같은 결과를 냈지만 비용이 더 컸고, 새로운 수학적 구조를 만들어야 풀리는 문제는 여전히 사정거리 밖이었다.

같은 분야에서 OpenAI는 지난주 80년 된 에르되시 추측 하나를 반증했다고 발표했지만, 그 몇 달 전에는 10개의 새 문제를 풀었다는 주장을 거둬들인 바 있다고 더 런다운 AI는 짚었다.

더 런다운 AI는 형식 검증이 결합된 이 방식이 시간이 지날수록 연구자들이 기계 속도로 새로운 발견을 해내도록 도울 것이라고 평가했다.