구글 딥마인드(Google DeepMind)가 형식적 수학 추론을 위한 새로운 강화학습 기반 시스템인 알파프루프(AlphaProof)와 기하학 문제를 해결하는 시스템인 알파지오메트리2(AlphaGeometry 2)를 발표했다. 또 이 두 시스템을 결합해 국제 수학 올림픽(IMO)에서 은메달 수준 점수를 획득할 수 있었다고 밝혔다.
국제 수학 올림픽에서는 6문제가 출제되며 각 문제는 7점 만점으로 채점된다. 모든 문제를 만점으로 맞추면 42점이 되는 시스템으로 상위부터 일정 비율로 금메달, 은메달, 동메달이 주어진다. 구글 딥마인드가 개발한 알파프루프는 대수 문제 2개와 정수론 문제 1개에서 만점을 획득했다. 또 알파지오메트리 2가 기하학 문제에서 만점을 획득해 총점은 28점이 됐다. 2024년 국제 수학 올림픽에서 금메달 기준이 29점이었기 때문에 아쉽게 금메달 획득에는 실패했다.
알파프루프는 알파제로(AlphaZero) 강화학습 알고리즘과 사전 학습된 언어 모델을 결합한 모델로 린(Lean)이라는 형식 언어로 수학적 문장을 증명하기 위해 자체 훈련을 수행한다. 형식 언어는 자연어에 비해 수학적 추론을 할 때 정확성을 형식적으로 검증할 수 있다는 장점이 있지만 훈련에 사용할 수 있는 데이터량이 압도적으로 적다는 단점이 있었다. 구글 딥마인드 측은 구글 AI 제미나이(Gemini)를 사용해 자연어 문제를 형식 언어로 자동 번역해 데이터량을 보완해 광범위한 난이도와 수학 주제 영역을 포괄하는 수백만 개 문제를 훈련에 사용할 수 있었다고 한다.
알파프루프 훈련 루프는 100만 개 자연어 문제가 형식화 네트워크에 의해 형식 언어로 변환되고 솔버 네트워크가 문제 증명 또는 반증을 검색한다. 검색에 성공하면 알파제로 알고리즘을 통해 솔버 네트워크가 훈련되어 더 어려운 문제를 해결할 수 있게 된다.
한편 알파지오메트리 2는 기하학 문제에 특화된 AI 모델. 전신인 알파지오메트리 단계에서도 기하학 문제에 한해서는 국제 수학 올림픽 금메달 획득 수준 점수를 얻었다.
알파지오메트리 2는 훨씬 더 많은 합성 데이터로 처음부터 훈련됐으며 국제 수학 올림픽에서 지난 25년간 출제된 기하학 문제에서 53%였던 알파지오메트리 정답률을 83%로 크게 개선했다. 2024년 국제 수학 올림픽 기하학 문제에서는 문제 형식화가 완료된 뒤 19초 만에 답변하는 데 성공했다.
구글 딥마인드 팀은 또 문제를 형식 언어로 번역하지 않고 답변할 수 있는 자연어 추론 시스템 실험도 수행해 유망한 결과를 얻었다고 한다. 또 알파프루프에 대한 기술적 세부 사항을 곧 공개할 예정이라고 밝혔다. 관련 내용은 이곳에서 확인할 수 있다.