Advancing Mathematics Research with AI-Driven Formal Proof Search

Google DeepMind, Aarhus University 및 Google 연구진은 대규모 언어 모델을 Lean 증명 보조기와 통합하여 수학의 여러 미해결 연구 수준 문제를 자율적으로 해결한 AI 기반 형식 증명 탐색 프레임워크인 AlphaProof Nexus를 개발했다.

이 연구는 대규모 언어 모델이 만든 풀이를 Lean으로 검증하는 형식 증명 탐색이 실제 미해결 문제에도 통하는지 대규모로 평가했다. 가장 강한 에이전트는 에르되시 미해결 문제 353개 중 9개를 자율적으로 해결하고 OEIS 추측 492개 중 44개를 증명했다. 에르되시 문제 하나를 푸는 데 든 비용은 수백 달러 수준으로 보고되었다. 언어 모델의 생성과 Lean 검증을 번갈아 수행하는 기본 에이전트도 에르되시 문제에서 같은 성공을 재현했지만 어려운 문제일수록 비용이 더 많이 들었다. 결과는 조합론과 최적화 등 여러 수학 분야에서 형식 검증을 결합한 인공지능의 활용 가능성을 보여주는 동시에 비용과 에이전트 설계가 중요하다는 점을 드러낸다.

핵심 요약

• 보조정리 환각: 에이전트가 실제로는 틀린 보조정리를 문헌의 잘 알려진 결과라고 주장하는 경우가 가끔 있었다. 에이전트가 그 특정 보조정리를 형식적으로 증명하려 시도하지 않았기 때문에, 오류는 후반 단계에 이르러서야 발견되었다.
• 필터로서의 형식화: 형식 증명 보조기는 AI가 생성한 수학을 연구자에게 유용하게 만드는 기준 진실을 제공한다. 이는 인간이 기본적인 논리적 오류를 점검할 필요를 없애 준다.
• 전략 발견을 위한 AI: AI는 고수준 계획을 제안하거나 인간이 간과할 수 있는 후보 반례를 식별함으로써 수학자를 도울 수 있다.

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.