AI, IMO 난제 해결하고 새 해법까지…수학 연구의 경계 넓어진다

• 알파프루프: IMO 난제 해결, 형식 증명 자동화
• 알파이볼브: 최적화 문제에서 새로운 해법 도출
• 수학 연구 전반에서 AI 활용 확대

인공지능이 국제수학올림피아드(IMO) 문제를 풀고 새로운 수학적 전략을 도출하는 수준에 도달했다. 형식 증명을 자동화하는 모델과 최적화 문제에서 새로운 해법을 찾는 모델이 공개되면서 수학 연구 현장에서 AI의 역할이 빠르게 커지고 있다.

구글 딥마인드는 AI 알파프루프가 수학 정리를 컴퓨터가 이해하는 논리 언어로 변환해 스스로 증명하는 성과를 네이처에 발표했다. 알파프루프는 지난해 IMO 6개 문제 중 4개를 해결했고, 참가자 609명 중 5명만 풀었던 최고난도 문제도 풀었다. 이 모델은 형식 증명 도구 린을 통해 증명을 코드 형태로 구성하고 단계적으로 검증한다. 연구팀은 약 8000만 개의 명제를 린 데이터로 구축해 모델을 훈련했으며, 강화학습을 적용해 스스로 문제를 생성하고 해결하며 전략을 익히도록 했다.

딥마인드는 올해 IMO 문제를 범용 추론 모델인 제미나이 딥 싱크로도 풀었다. 이 모델은 수학 전용이 아님에도 6문제 중 5문제를 해결했다. 형식 증명 방식처럼 모든 증명을 처음부터 다시 만들 필요가 없어 더 빠르게 접근할 수 있다는 점이 차이로 꼽힌다.

필즈상 수상자 테런스 타오 UCLA 교수가 참여한 연구팀은 또 다른 AI 모델 알파이볼브를 아카이브에 공개했다. 알파이볼브는 다양한 해법을 만들어낸 뒤 성능이 높은 일부만 반복 학습시키는 방식으로 작동하며, 기존 기록보다 효율적인 해법을 확보했다. 연구팀은 해석학, 기하학, 조합론, 정수론 등 67개 문제에서 기존 최적 해법을 재발견했고, 일부 문제에서는 새로운 전략을 제시했다. 특히 니코딤 문제와 산술 카케야 문제에서 얻은 결과는 후속 연구로 이어지고 있다.

수학 연구 현장에서는 형식 증명 자동화, 반례 탐색, 문헌 조사 등 다양한 영역에서 AI 활용이 확대되고 있다. 이준경 연세대 수학과 교수는 AI가 반례 탐색과 보조정리 검증 등 연구 효율을 높이는 도구가 될 수 있다고 말했다. 동시에 과도한 의존은 학생 연구자의 사고력과 훈련 기회를 약화시킬 수 있어 교육 현장에서 활용 기준과 윤리 논의가 필요하다고 강조했다.

손동민 기자/ hello@sciencewave.kr

관련 기사: ‘지치지도 않고 1000회 실험’…AI·로봇, 화학 실험실서 열일한다