알파지오메트리 원리 해설: 규칙 데이터베이스와 언어 모델이 IMO 기하 문제를 함께 푸는 방법

핵심 메시지

• 2024년 1월 공개된 알파지오메트리는 국제수학올림피아드 기하 문제 30개 중 25개를 풀어 은메달리스트를 웃도는 성적을 냈다.
• 그 전에 이미 규칙 기반 연역 엔진과 선형방정식 풀이만으로 18문제를 풀 수 있었다. AI가 처음부터 다 한 것이 아니다.
• 규칙 엔진이 막히는 지점은 보조선을 그어야 하는 문제였고, 언어 모델은 오직 그 보조선을 제안하는 역할만 맡았다.
• 학습 데이터가 부족하다는 문제는 무작위 도형에서 정리를 연역한 뒤 일부를 지워 문제로 되돌리는 방식으로 수억 건의 합성 증명을 만들어 해결했다.
• 창의적인 착상과 엄밀한 연역을 분리해 결합한 이 구조는 기하에만 쓸 수 있는 것이 아니라 다른 문제 해결 영역으로도 이어질 수 있다.

쉽게 이해하기

국제수학올림피아드는 고등학생 수준 수학 경시의 최상위 무대다. 해마다 100개가 넘는 나라가 저마다 복잡한 선발 과정을 거쳐 여섯 명씩 대표를 보낸다. 2024년 1월 구글 딥마인드가 공개한 알파지오메트리가 이 대회의 기하 문제 30개를 모아둔 데이터베이스에서 25개를 풀어냈다는 소식은 그래서 큰 화제가 됐다. 은메달리스트보다 나은 성적이었다.

그런데 덜 알려진 사실이 있다. AI가 등장하기 전에 이미 순수한 논리와 방정식 풀이만으로 25문제 중 18문제를 풀 수 있는 기법이 존재했다는 점이다. 출발점은 2000년 10월 투, 가오, 장 세 연구자가 발표한 논문이다. 이들은 기하 규칙 75개를 데이터베이스로 만들고 이를 조합해 정리를 연역했다. 맞꼭지각은 같다, 평행선 사이의 엇각은 같다 같은 단순한 사실 두 개만으로도 자명하지 않은 정리를 증명할 수 있는데, 규칙이 75개가 되면 도달할 수 있는 정리의 범위가 크게 넓어진다. 이 방식은 연역 데이터베이스(DD)라고 불리며 30문제 중 7개를 풀었다.

DD에는 방정식을 풀지 못한다는 한계가 있었다. 반원에 내접하는 각이 직각이라는 탈레스 정리만 해도 두 이등변삼각형의 밑각을 알파와 베타로 두고 2알파 더하기 2베타는 180도라는 식을 세워 양변을 2로 나누는 과정이 필요하다. 선형방정식 풀이는 컴퓨터가 잘하는 일이므로 딥마인드 연구진은 이를 대수적 추론(AR) 모듈로 구현하고, DD가 멈추면 AR을 돌리고 다시 DD를 돌리는 식으로 번갈아 실행했다. 이 DD 더하기 AR 조합은 14문제를 풀었고, 사람이 손으로 짠 휴리스틱을 더하자 18문제까지 올라갔다. 동메달에 근접하는 성적이다.

그럼에도 넘지 못한 벽이 보조선이었다. 삼각형 내각의 합이 180도임을 보이려면 위아래에 평행선을 그어야 하듯, 어려운 기하 문제는 원래 그림에 없던 점이나 선을 새로 그려야 풀린다. 올림피아드 문제는 이런 보조 작도를 여러 번 요구하는 경우가 많은데, 기계 입장에서는 매 단계마다 무한한 탐색 공간이 열리는 셈이다. 그래서 딥마인드는 오직 보조 작도만 제안하는 언어 모델을 따로 만들었다. 문제 진술과 지금까지의 증명 단계를 입력받아 다음에 그을 점이나 선 하나를 내놓는 것이 이 모델의 전부다.

전체 흐름은 이렇게 돌아간다. 언어 모델이 보조선을 하나 제안하면 DD와 AR이 거기서 뽑아낼 수 있는 사실을 모두 연역하고, 그 결과를 다시 언어 모델에 넘겨 또 다른 보조선을 받는다. 문제가 풀리거나 시간이 다할 때까지 이 과정을 반복한다. 언어 모델이 창의적인 뇌라면 DD와 AR은 논리적인 뇌인 셈이다. 학습 데이터가 없다는 문제는 스스로 만들어 해결했다. 평면에 점과 선을 무작위로 찍고 DD와 AR로 도출 가능한 사실을 모두 연역한 뒤, 그림의 일부를 지워 문제로 되돌리는 방식이다. 지워진 부분을 되살리는 일이 곧 보조 작도가 된다. 이렇게 만든 합성 증명이 수억 건이고, 그중 900만 건은 보조 작도가 최소 한 번 필요했다. 가장 복잡한 증명은 247단계에 보조 작도 두 개를 담고 있었다.

주요 인사이트

• 화제가 된 숫자는 25 대 30이지만, 그 안을 뜯어보면 7에서 14로, 다시 18로 올라간 계단은 전부 AI가 아닌 고전적 기법의 몫이었다. 새 기술의 성과를 읽을 때 기존 방법이 어디까지 도달해 있었는지를 함께 보는 일이 중요하다는 사례다.
• 알파지오메트리의 언어 모델은 문제를 푸는 주체가 아니라 탐색 공간을 좁히는 제안자에 가깝다. 검증은 엄밀한 연역 엔진이 맡기 때문에, 언어 모델이 틀린 착상을 내놓아도 잘못된 증명이 통과되지 않는다.
• 정리 증명 언어로는 린(Lean)이 대표적이지만 유클리드 기하에는 잘 맞지 않아, 연구진은 기하 전용으로 설계된 별도의 언어를 사용했다. 문제 영역에 맞는 표현 방식을 고르는 일이 성능의 전제 조건이었던 셈이다.
• 데이터가 없으면 만들어 쓴다는 발상도 눈여겨볼 만하다. 정답을 먼저 연역해두고 문제를 거꾸로 만들어내는 방식은 정답이 보장된 학습 데이터를 대량으로 확보하는 방법이었다.
• 영상 말미에 따르면 알파지오메트리 이후 여러 연구 그룹이 기하뿐 아니라 올림피아드 전 문제에서 금메달 수준의 성적을 냈고, 그중 구글 딥마인드와 오픈AI는 기하 전용 언어나 린 같은 수학 전용 언어 없이 자연어만으로 해냈다고 알려졌다.

자주 묻는 질문

관련 AI 소식