수학올림피아드가 갑자기 왜 나와요?
수학에서 정리를 증명한다는 것은 주어진 가정과 논리적인 규칙을 사용해 새로운 결론을 도출하는 과정이고, 이는 높은 문제 해결 능력을 가지고 있다는 것을 의미합니다. 1950년대 이후로 더 나은 정리 증명 능력을 추구하는 것은 AI 연구의 지속적인 초점이 되어 왔습니다. 또한 수학 올림피아드는 오랜 역사를 자랑하는 세계에서 가장 유명한 정리 증명 대회로, 문제 해결능력이 뛰어난 재능을 가진 인재를 발굴하는데 중요한 역할을 하고 있습니다. 그래서 올리피아드 수준에서 인간의 정리 증명 성과를 따라잡는 것이 AI 연구의 주요 이정표가 되었습니다.
그래서 보여줄게 뭔가요?
이 글에서 소개시켜 드릴 AlphaGeometry[1]는 AlphaGo[2]를 만든 DeepMind에서 제안한 기하학 정리 증명 모델로 세계적으로 유명한 저널인 nature에 2024년에 게제된 논문입니다.
그림에서 위의 행(a, b, c, d)은 간단한 문제를 AlphaGeometry가 해결하는 과정을 보여줍니다.
a. 간단한 예제와 다이어그램이 있습니다.
b. 기호 추론 엔진을 실행하여 증명 검색을 합니다. 이 엔진은 정리(theorem)가 증명되거나, 새로운 구문(statement)가 나오지 않을 때까지 계속 추론을 시도합니다.
c. 만약 기호 추론 엔진이 증명을 하지 못하면, 언어모델이 하나의 보조 점(auxiliary point)을 구성하여 증명에 구문을 추가합니다. 위 예시에서는 선분BC 사이에 중앙점D를 하나 추가했습니다.
d. 새롭게 주어진 구문을 이용해 다시 증명을 시도하여 증명에 성공합니다
아래 행(e, f)는 실제 수학올림피아드 IMO 2015에 나온 3번 문제 해결에 대한 예시입니다.
e. IMO 2015 P3의 문제와 다이어그램이 있습니다.
f. AlphaGeometry에서 새롭게 추가한 3개의 보조 점(auxiliary point)을 이용해 증명을 성공합니다.
AlphaGeometry가 어떤점이 다른가요?
AlphaGeometry이전에도 정리 증명을 하기 위한 많은 시도들이 있었습니다. 하지만 기존에는 학습에 사용할 증명 예제들을 사람이 제공했기 때문에, 데이터의 양의 한계가 있었습니다. AlphaGeometry는 합성 데이터를 사용해서 학습 데이터의 양을 늘리는 방법을 사용해, 1억개의 합성 정리와 그 증명을 추출했고 그 데이터를 이용해 학습을 했습니다.
위 그림은 AlphaGeometry에서 생성한 1억개의 합성 정리에 대한 증명 길이 별 분포 그래프입니다. 생성한 데이터 중 9%는 보조 점(auxiliary point)를 추가해 해결한 증명입니다. 전체 데이터 중 0.05% 만이 평균적인 IMO 증명길이보다 길었습니다. 가장 복잡한 합성 정리는 2개의 보조 구조(auxiliary constructions)가 있는 247개 길이의 증명이었습니다.
AlphaGeometry가 얼마나 잘하나요?
2000년부터 현재까지 공식 IMO문제를 이용해 테스트 벤치마크를 진행했습니다. (단, 이 논문에서 제시한 환경으로 표현이 가능한 문제들에 한해서 테스트를 했습니다.)
기계는 성공(1) or 실패(0)의 이분법적인 점수만 가지기 때문에 비교를 위해 기존 IMO에서 채점하는 0~7까지의 점수를 0~1로 조정하여 테스트를 진행했습니다. 총 30개의 문제에서 금메달리스트와 겨우 0.9점 차이로 평균적인 IMO 금메달리스트의 성능에 근접했습니다.
AlphaGeometry가 무슨 의미가 있나요?
유클리드 평면 기하학 정리를 증명하는데에 있어서 평균적인 IMO 참가자의 성능을 뛰어넘는 최초의 프로그램입니다. 또한 사람이 생성한 증명 예제나 사람이 선별한 문제 문장을 사용하지 않고, 처음부터 대규모 탐색을 통해 정리를 증명하는 접근법을 입증했습니다. 이로 인해 다른 수학 영역에서 직면한 데이터 부족 문제를 합성 데이터를 이용해 해결할 수 있다는 가이드라인을 제공했습니다. AlphaGeometry에서 입증한 합성 데이터를 이용한 학습 방법을 통해 다른 수학 영역에서도 많은 발전이 일어난다면, 지금보다 더 빠르게 문제를 해결할 실마리를 찾을 수 있을 것으로 기대됩니다.
Reference
- Trinh, T.H., Wu, Y., Le, Q.V. et al. Solving olympiad geometry without human demonstrations. Nature 625, 476–482 (2024). https://doi.org/10.1038/s41586-023-06747-5
- Silver, D., Huang, A., Maddison, C. et al. Mastering the game of Go with deep neural networks and tree search. Nature 529, 484–489 (2016). https://doi.org/10.1038/nature16961
