국제수학올림피아드에 도전한 AI 실력은 금메달리스트
수학은 더 이상 인간의 전유물이 아니다. 계산 능력은 이미 수십 년 전 컴퓨터에게 따라잡혔고 최근에는 고도의 논리력과 사고력을 요하는 수학의 증명까지 인공지능(AI)이 해내기 시작했다.
그중 가장 화제가 되는 것은 구글 딥마인드 연구팀이 개발한 기하 증명 AI '알파지오메트리'다. 알파지오메트리가 국제수학올림피아드(IMO)에 출전한다면 어떤 결과가 나올까.
"수학은 인간정신의 자유로운 창조물이다." - 리하르트 데데킨트
수학은 눈에 보이지 않는 것을 논리적으로 풀어나가는 추상적 사고와 전에 배운 적 없는 창의적 해결 방식이 필요한 학문이다. 그래서 아주 오래전부터 인간의 전유물로 여겨졌다. 하지만 더 이상은 아니다. 구글 딥마인드 연구팀이 개발한 기하 증명 인공지능(AI) '알파지오메트리'가 국제수학올림피아드(IMO) 출제 문제에 놀라운 해결력을 보였기 때문이다. 그 내용은 2024년 1월 17일 국제학술지 '네이처'에 공개됐다. (doi: 10.1038/s41586-023-06747-5)
● 기하 문제 30개 중 25개 해결... 금메달리스트급 실력
올림픽 정신을 따르는 IMO는 매년 7월 각나라에서 수학실력이 가장 뛰어난 고등학생들이 모여 수학 실력을 겨루는 대회다. 1959년부터 시작된 IMO는 국제과학올림피아드 가운데 가장 큰 규모와 오래된 역사를 자랑한다. 또한 학부 미만의 학생들을 대상으로 하는 수학경시대회 중위상이 가장 높다. IMO 금메달 수상자가 수학계 최고 영예의 상인 필즈상 수상자로 이어지는 경우도 많다는 점이 이를 방증한다.
세계 7대 난제로 선정된 밀레니엄 난제 '푸앵카레의 추측'을 해결해 필즈상 수상자로 선정됐지만 수상을 거절한 그리고리 페렐만, 역대 최연소 IMO 금메달리스트 테렌스 타오 등 역대 필즈상 수상자 64명 중 16명이 IMO 금메달리스트다.
걸출한 수학 실력을 갖춘 학생들이 겨루는 자리인 만큼 IMO의 문제는 어렵기로 유명하다. 단순한 암기나 기본적인 계산 능력을 넘어서 깊은 수학적 이해와 새로운 통찰력을 요하는 문제가 많다(수학을 전공하는 대학생들도 풀기 어렵다).
IMO는 대수, 조합, 기하, 정수 네 분야를 다루는 문제가 이틀에 걸쳐 3문제씩 총 6개 출제된다. 연구팀이 개발한 알파지오메트리는 네 분야 중 기하문제를 푸는데 특화된 AI이다. 연구팀은 알파지오메트리가 2000년부터 2022년까지 IMO에 출제된 30개의 기하문제 중 25개의 문제를 제한 시간내에 해결했다고 밝혔다.
사람과 비교하면 어떨까? IMO에 참가해 금메달을 딴 학생들은 같은 시간 동안 평균적으로 25.9개의 문제를 해결했다. 알파지오메트리가 IMO 금메달리스트에 버금가는 실력을 보인 셈이다.
2008년 IMO에 한국 국가대표로 출전했던 남경식 KAIST 수리과학과 교수는 “IMO의 기하 문제는 다른 분야의 문제보다 독창적인 보조선, 보조점들을 그어 해결해야 해 인간의 창의력이 더욱 요구된다”며 “대수, 조합, 기하, 정수 중 기하 문제를 잘 푸는 알파지오메트리는 정말 신기하다”고 놀라움을 표했다.
● 스스로 증명을 배우는 AI 등장
연구팀은 네이처에 게재된 논문에서 “기하 분야는 수학적 증 명을 컴퓨터가 이해하는 언어로 변환하기 어려워 여전히 AI 학습이 잘이뤄지지않는 분야”라며 기하문제에 도전한 이유를 밝혔다.
연구팀이 비교한 기존의 기하 증명 프로그램으로는 '우의 방법(Wu's method)'과 '그뢰브너 기저(Gröbner basis)'가 있다. 두 프로그램은 모두 기하 문제를 대수 문제로 변환해 증명 알고리즘으로, 다양한 문제에 적용이 어렵다.
그 외에 기계 학습을 사용한 수학증명 시도들은 거의 제대로 작동하지 못했다. 복잡한 인간의 풀이 데이터를 다시 컴퓨터가 이해할 언어로 변환하는데 큰 노력을 해야하므로 AI가 충분히 똑똑해질 만큼의 충분한 데이터를 구축하기 어렵기 때문이다.
연구팀은 이 문제를 해결하기 위해 기본적인 기하 정리들에 대한 수학 증명 데이터만을 넣어준 뒤 기하학적 상황을 무작위로 생성해 그 문제를 풀도록 했다. 이 과정을 통해 알파지 오메트리가 스스로 새로운 정리와 증명을 이끌어 내도록 했다.
2006년과 2007년 IMO 한국 국가대표로 참가했던 이석형 서울대 모듈과 공간의 양자구조 연구센터 연수연구원은 “수학을 공부하는 사람들 사이에도 수학을 제로베이스에서 배운다 는 것을 상상하기 어려운데 이를 알파지오메트리가 해냈다는 것이 굉장히 대단하다”며 "딥러닝 기술의 발전이 스스로 수학을 배우는 AI의 탄생을 이끌었다고 생각한다"고 말했다. 이어 "인간의 바둑 기보를 학습한 알파고에서 학습데이터 없이 스스로 바둑을 깨친 알파 제로로 발전하게 된 것과 비슷한 맥락으로 보인다"고 덧붙였다.
실제로 알파지오메트리는 기존 알고리즘인 우의 방법과 그뢰브너 기저 프로그램에 비해 월등히 뛰어난 실력을 보인다. 우의 방법은 30개 중 10개의 문제를 해결했고 그뢰브너 기저는 단 4문제만 풀었다. 이 연구원은 "2차원 기하는 이론적으로는 어떤 문제든 대수적으로 풀 수 있지만 그것을 계산해 답을 낼 수 있느냐는 전혀 다른 문제"라며 "기하문제를 대수적 방식으로 해결하는 우의 방법과 그뢰브너 기저가 (알파지오메트리에 비해) 약세를 보인 것은 이 때문일 것"이라고 설명했다.
● '보조선' 긋는 알파지오메트리의 풀이법
알파지오메트리는 연역적 데이터베이스(DD·Deductive Database)와 대수적 추론(AR·Algebraic Reasoning)으로 구성된 '심볼릭 추론 엔진'을 통해 새로운 증명을 진행한다. DD는 입력된 기하 정보를 토대로 논리적 추론을 내린다.
예를 들어 '모든 고양이는 포유류다' 명제와 '톰은 고양이다' 명제가 입력돼 있다면 '톰은 포유류다'라는 논리적 결론을 자동으로 추론 할 수 있다. AR은 수학적, 대수적 개념과 원리를 사용해 문제를 해결한다. 두점 사이의 거리를 계산하거나 각도의 크기를 결정하는 문제를 풀 수 있다. 알파지오메트리는 두 과정을 반복적으로 수행하며 기하 증명을 자동화한다.
여기에 생성 AI에 사용되는 언어모델을 활용하면 더 수준 높은 증명 자동화를 이뤄낼 수 있다. 언어모델은 문장을 새롭게 생성하는데 뛰어난 능력을 보인다. 알파지오메트리에서 언어모델은 기하문제에 필요한 보조선과 보조점등적절한 보조도구를 생성할 수 있다.
앞서 남 교수가 말한 것처럼 기하문제 풀이에서 '보조선'과 같은 창의적인 보조 도구는 증명을 이끄는 핵심 키일 수 있다. 알파지오메트리는 심볼릭 추론엔진을 통해 증명을 수행하다가 문제가 해결되지 않을 땐 언어모델로 보조도구를 생성한다.이후 다시 심볼릭 추론 엔진을 사용한다. 이 과정을 반복적으로 수행해 올바른 증명을 찾는 것이다. 간단한 기하 증명을 예로 살펴보자.
'임의의 ∆ABC에서 AB=AC라면 ∠ABC=∠BCA는 같다'를 증명하는 문제가 알파지오메트리에게 주어졌다고 가정하자. 알파지오메트리는 DD와 AR을 사용해 주어진 환경 속에서 증명을 도출 할 방법을 찾는다. 하지만 이 증명에꼭 필요한 것은 D라는 보조점이다. 보조점이 없으면 증명할 수 없기 때문에, 심볼릭 추론엔진은 해당 상황에서 증명을 도출 할 수 없다는 결론을 내린다.
이때 언어모델은 'BC의 중점 D를 보조점으로 추가한다'는 명령어를 생성한다. 알파지오메트리는 이제 새로운 조건에서 BD와 DC가 같다는 점, AD라는 선분을 ∆ABD, ∆ACD가 동시에 포함한다는 점을 근거로 ∆ABD, ∆ACD가 합동임을 보이면 ∠ABD=∠ACD임을 증명할 수 있다.
● 수학 연구에 유용할까? 수학자들 생각은
수학자들은 알파지오메트리를 어떻게 생각할까. 2002년 IMO에 출전한 김린기 인하대 수학과 교수는 "과거부터 예상만 해 온 수학 증명이 가능한 AI가 실제로 탄생했다는 사실이 매우 신기하다"고 말했다. 다만 "그 풀이의 형태가 매우 단순하고 일차원적이다"고 평가했다. 인간은 직관적 추론이 가능해 풀이에 적지 않는 수학 성질들을 알파지오메트리는 모두 풀이에 적어 전체 풀이가 매우 길었기 때문이다.
이연수 연구원 역시 “알파지오메트리는 오로지 논증법 방법만 사용했기 때문에 풀이가 길어지는 것이 당연한 결과였을 것”이라고 답했다. 그는 "IMO에 출제 문제 중 3번과 6번은 매년 그해 시험에서 가장 어려운 문제로 손꼽힌다"며 "알파지오메트리가 못 푼 문제 중 3번과 6번이 많다는 점에서 꽤 사람 다운 행동을 보이는 AI라는 생각이 들었다"고 밝혔다. 남 교수는 보조선이나 보조점 등의 보조도구를 적절하게 잘 생성하는 능력에 감탄했다.
그는 "저조차도 손도 못댈것 같은 문제들이 있는데 언어모델이 꽤 정확하게 보조도구를 생성해 푸는 것 이 신기했다"며 "이런 기술들은 연구 단계에서 기하 문제 풀이 시간을 단축하는 데 도움이 될 수 있겠다"고 말했다.
물론 당장 연구에 적용하기엔 시간이 걸리리라는 것이 인터뷰를 통해 만난 전문가들의 공통된의견이다. 문제를 푸는 것과 수학을 연구하는 것은 다른 영역이기 때문이다. 김교수는 "실제 연구에 쓰이는 프로그램들은 복잡한 연구에서 필요한 계산을 빠르게 처리해 주는 프로그램"이라며 "증명과 추론의 과정은 AI에게 맡기는 경우가 없다"고 설명했다.
고차원적인 수학 연구에 사용하기엔 아직 너무 단순한 기하 증명 AI라는 평가다. 이연수 연구원역시 "기하학 문제를 논증하는 것은 순수한 연구 목적보다 교육적 목적이 더 크다"며 "알파지오메트리가 좋은 결과를 냈지만 이를 이론 연구에 사용하기는 아직 어려울 것"이라고 예측했다.
※관련기사
과학동아 3월호, 국제수학올림피아드에 도전한 AI, 결과는?
[김미래 기자 futurekim93@donga.com]
Copyright © 동아사이언스. 무단전재 및 재배포 금지.