Solving olympiad geometry without human demonstrations
인간 시연 없이 올림피아드 기하 문제 풀기
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, et al. (2024)
LLM이 보조 구성을 생성하고 기호적 추론 엔진이 증명을 수행하는 신경-기호(neuro-symbolic) 시스템으로, 인간 시연 없이 올림피아드 수준 기하 문제를 풀어낸 논문.
배경
수학 올림피아드 기하 문제는 창의적 보조선 구성과 엄밀한 논리적 추론을 동시에 요구하는 극도로 어려운 과제이다. 기존 AI 시스템은 대수적 방법이나 좌표 기하로 일부 문제만 풀 수 있었으며, 순수 기하학적 증명에는 한계가 있었다. 특히 학습 데이터가 거의 없는 것이 큰 제약이었다.
핵심 아이디어
AlphaGeometry는 두 시스템의 시너지를 활용한다. 기호적 추론 엔진(DD+AR)은 기존 조건으로부터 연역적으로 도출 가능한 모든 사실을 빠르게 계산한다. 추론이 막히면 LLM이 새로운 보조점이나 보조선을 제안하여 추론 공간을 확장한다. 핵심 혁신은 합성 데이터 생성에 있는데, 무작위 기하 구성에서 역추론으로 1억 개 이상의 증명 데이터를 자동 생성하여 LLM을 학습시켰다. 이를 통해 인간이 만든 증명 데이터 없이도 효과적인 보조 구성 능력을 확보했다.
방법론
기호적 엔진이 현재 상태에서 도출 가능한 사실을 모두 찾고, 목표에 도달하지 못하면 LLM에 상태를 직렬화하여 보조 구성을 요청한다. LLM이 제안한 구성을 추가하고 기호적 추론을 재실행하는 루프를 반복한다. LLM은 합성 증명 데이터로 사전학습한 트랜스포머이다.
주요 결과
IMO(국제수학올림피아드) 기하 문제 30개 중 25개를 풀어, 은메달 수준의 성적을 달성했다. 이는 이전 최고 기록(10개)을 크게 앞서며, 기호적 엔진만으로는 14개, LLM만으로는 불가능한 성과이다.
임팩트
AI의 수학적 추론 능력에서 신경-기호적 접근의 강력한 가능성을 입증했다. 합성 데이터를 통한 수학 추론 학습이라는 새로운 패러다임을 제시했으며, AI가 인간 수준의 창의적 수학 문제 해결에 다가가고 있음을 보여주었다.