영상: IMO 기하학 문제를 해결한 AI | @Aleph0의 게스트 영상
채널: 3Blue1Brown
길이: 13분 30초
출처: 자막 (수동, 영문)
스크립트:
[criblate.com에서 자막 수정을 제출하세요] 2024년 1월, Google DeepMind는 국제 수학 올림피아드(International Mathematical Olympiad, IMO)의 기하학 문제를 해결할 수 있는 Alpha Geometry라는 AI 모델을 출시했습니다. IMO는 고등학교 수준에서 열리는 가장 높은 단계의 경쟁 수학 대회입니다. 매년 100개국 이상의 국가들이 대회를 대표하기 위해 6명의 십 대들을 보냅니다. 각 국가는 6명의 대표를 선발하기 위해 자체적인 정교한 대회 시스템을 갖추고 있습니다. Alpha Geometry를 30개의 기하학 문제 데이터베이스로 테스트했을 때, 이 모델은 그중 25개를 해결했습니다.

이는 은메달리스트의 성적보다 더 나은 결과입니다. 이는 당연하게도 많은 화제를 불러일으켰습니다. 하지만 여기서 아무도 이야기하지 않는 사실이 있습니다. 저에게 가장 놀라운 부분은 AI가 이 문제들을 해결해냈다는 사실이 아니라, AI가 등장하기 전에도 이미 일어났던 일입니다. AI를 전혀 사용하지 않고 오직 논리(logic)와 순수 방정식 풀이(equation solving)만을 사용한 25년 된 기술이 이미 25개 문제 중 18개를 해결할 수 있었습니다. 이는 이미 IMO에서 동메달 수준입니다. 그리고 나서 모델은 벽에 부딪혔습니다. 이 독창적인 논리 모델조차 해결할 수 없는 문제들이 있었습니다.

그리고 바로 그 지점에서 AI가 등장합니다. 하지만 모든 것을 AI에 맡기는 대신, DeepMind 팀은 30개 중 25개라는 놀라운 결과에 도달하기 위해 논리 모델을 AI 구성 요소와 매우 영리하게 통합했습니다. 그래서 이 영상에서, 네, 저는 AI와 기하학에 대해 이야기하고 싶습니다. 하지만 그전에, 비(non)-AI 모델이 어떻게 이미 대다수의 인간보다 기하학을 더 잘할 수 있었는지에 대해서도 이야기하고 싶습니다. 그럼 시작해 보겠습니다. 오늘의 과제는 간단합니다. IMO 기하학 문제를 풀 수 있는 봇을 만드는 것입니다.

하지만 문제를 조금 더 어렵게 만들기 위해 한 가지 주의 사항을 덧붙이겠습니다. AI를 사용하지 않고 IMO 문제를 해결하는 봇을 만드세요. 이 문제에 접근하기 위해, 우리는 기하학 문제에 관한 잘 알려지지 않은 비밀을 이용할 것입니다. 몇 가지 핵심 사실만 알아도 아주 멀리까지 나아갈 수 있습니다. 예를 들어, 여기 기하학의 두 가지 중요한 사실이 있습니다. 첫째, 두 직선이 교차할 때 맞꼭지각 (opposite angles)은 같습니다. 둘째, 만약 이 두 수평선이 평행 (parallel)하다면, 여기 파란색으로 표시된 Z 모양을 보았을 때 Z의 안쪽에 있는 각들은 같습니다. 이 두 가지 사실만으로도 우리는 이미 사소하지 않은 정리 (non-trivial theorem)를 증명할 수 있습니다.

이 도식에서 두 개의 주황색 각 $\alpha$는 같습니다. 우리의 두 가지 사실을 차례대로 적용하면, 우리의 정리가 증명됩니다. 자, 이것이 두 가지 사실에서 시작했을 때 우리가 도달할 수 있는 지점입니다. 이제 우리가 10가지 사실, 50가지 사실, 또는 100가지 사실에서 시작한다면 얼마나 멀리 갈 수 있을지 상상해 보세요. 우리가 증명할 수 있는 정리의 공간은 점점 더 커질 것입니다. 2000년 10월, 연구자 Tu, Gao, Zhang은 정확히 이 작업을 수행한 논문을 발표했습니다. 그들은 논문에서 75개의 기하학 규칙 데이터베이스를 만들었습니다. 연구자들은 이 사실들을 다양한 조합으로 적용하여 매우 어려운 기하학 문제들을 해결할 수 있었습니다.

이 규칙들은 제가 화면에 쓴 것들처럼 단순하게 시작합니다. 하지만 진행할수록 화면 하단의 규칙처럼 점점 더 복잡해집니다. 그런데 이 모든 도식들을 어떻게 컴퓨터에 입력할까요? 음, 가장 단순한 방법은 명시적 방정식 (explicit equations)을 사용하여 Desmos에 모든 것을 그리는 것이겠지만, 우리 둘 다 그것이 너무 번거롭다는 점에는 동의할 것입니다. 또 다른 대안은 정리 증명 (theorem proving)을 위해 특별히 설계된 언어를 사용하는 것입니다. 이 분야에서 지배적인 언어는 Lean이라고 불립니다.

Lean은 대수학 (algebra)이나 부등식 (inequalities) 같은 분야에는 정말 훌륭하지만, 현재로서는 유클리드 기하학 (Euclidean geometry)에는 그리 적합하지 않습니다. 이를 해결하기 위해 저자들은 기하학을 위해 특별히 설계된 더 니치(niche)한 언어를 사용했습니다. 제가 알기로 이 언어는 아직 공식적인 이름이 없으며 연구 논문에서만 설명되고 있습니다. 다음과 같은 모습입니다. 예를 들어, 두 변의 길이가 같은 삼각형은 두 각의 크기도 같다는 이 문제를 컴퓨터에 표현하고 싶다고 가정해 봅시다.

[IMG:1]

특화된 기계 언어 (machine language)에서는 다음과 같이 작성합니다. ABC points는 세 점 A, B, C가 존재함을 의미합니다. AB equals AC는 변 AB와 AC의 길이가 같음을 의미합니다. Goal, angle ABC, equals angle BCA는 목표가 이 두 각이 같음을 보이는 것임을 의미합니다. 연구진은 이 방법을 연역적 데이터베이스 (deductive database), 줄여서 DD라고 불렀습니다. '데이터베이스 (database)'라는 단어는 핵심 사실들의 데이터베이스에서 시작한다는 것을 암시하며, '연역적 (deductive)'이라는 말은 그 핵심 사실들로부터 새로운 정리 (theorems)를 연역해낸다는 것을 의미합니다.

그렇다면 성능은 어떠했을까요? IMO 기하학 문제 30개 중 7개를 해결했습니다. 이를 바라보는 두 가지 관점이 있습니다. 한편으로는 30개 중 7개는 그리 많지 않습니다. IMO에서는 언급될 수준조차 되지 않습니다. 하지만 다른 한편으로는, 브루트 포스 (brute force) 방식이 IMO 문제 중 단 하나라도 해결할 수 있다는 사실은 믿기 힘들 정도로 인상적입니다. IMO 문제는 매우 어렵기 때문입니다. 그렇다면 어떻게 점수를 높일 수 있을까요? 한편으로는 그냥 손을 들고 '좋아, AI가 성능을 개선해야 해'라고 말할 수도 있습니다. 하지만 그것은 완전히 정확한 말은 아닙니다. 왜냐하면 DD에는 우리가 아직 다루지 않은 근본적인 한계가 있기 때문입니다.

DD는 방정식을 풀 수 없습니다. 이것은 문제입니다. 왜 그런지 알아보기 위해, Thales의 정리 (Thales's theorem)라고 불리는 정리에 대해 말씀드리겠습니다. 여기 반원에서의 각도는 항상 직각입니다. 방정식을 사용한 짧은 증명은 다음과 같습니다. 세 번째 점을 중심과 연결하는 세 번째 선을 그립니다. 그러면 제가 여기서 표시하고 있는 세 선은 모두 원의 반지름 (radii)이므로, 모두 길이가 같습니다. 따라서 두 개의 작은 삼각형은 모두 이등변 삼각형 (isosceles triangles)입니다. 그들의 대각 (opposite angles)은 같습니다. 큰 삼각형 ABC의 각의 합은 180도이므로, 2 alpha plus 2 beta equals 180 degrees가 됩니다.

양변을 2로 나누면, alpha plus beta equals 90 degrees가 됩니다. 그런데 alpha plus beta는 각 ABC이므로, 정리 증명이 완료되었습니다. 선형 방정식 (linear equations)을 푸는 것은 컴퓨터가 선형 대수 (linear algebra)를 사용하여 매우 잘 수행할 수 있는 일입니다. 그래서 DeepMind 연구진은 이를 모델에 구현하였고, 이를 대수적 추론 (algebraic reasoning), 줄여서 AR이라고 불렀습니다. 요약하자면, 지금까지 우리는 두 개의 모듈을 가지고 있습니다. 연역적 데이터베이스 (Deductive database), 즉 DD는 기하학적 규칙들의 하드코딩된 리스트입니다. 대수적 추론 (Algebraic reasoning), 즉 AR은 선형 방정식 시스템 (systems of linear equations)을 풀 수 있는 능력입니다.

DeepMind 팀은 이 두 모델을 교대로 사용했습니다. 즉, 먼저 DD가 멈출 때까지 실행했습니다. 그런 다음 AR이 멈출 때까지 실행했고, 그다음 다시 DD, 그다음 AR 순으로 진행했습니다. 그리고 문제가 해결되거나 시간이 다 될 때까지 이 과정을 반복했습니다. 이 절차를 통칭하여 DD plus AR이라고 불렀습니다. 이것은 매우 잘 작동합니다. 예를 들어, 그들의 논문에 나온 아래 문제를 보면, DD 모듈이 처음 두 줄을 연역해냈습니다. 그러면 AR 모듈이 결과로 나온 방정식 시스템을 가져와서 그것들을 풀었습니다. 이제 IMO 기하학 문제에 대한 결과들을 살펴보겠습니다.

DD 단독으로는 30문제 중 7문제를 해결했습니다. DD와 AR을 결합했을 때는 30문제 중 14문제를 해결했습니다. DeepMind 연구진은 이른바 인간이 코딩한 휴리스틱 (human-coded heuristics)을 추가함으로써 이를 30문제 중 18문제까지 더 끌어올렸습니다. 이는 IMO에서 거의 동메달 수준에 해당합니다. 저에게는 DD와 AR의 결합이 이토록 뛰어난 성과를 냈다는 점이 정말 놀랍습니다. 왜냐하면 IMO 기하학 문제들은 정말 정말 어렵기 때문에, 무차별 대입 방식 (brute force approach)이 이 정도 단계까지 도달할 수 있다는 사실 자체가 매우 놀랍기 때문입니다. 그리고 AI 없이도 이 정도까지 도달했다는 점을 고려하면, 애초에 왜 AI를 추가하려 하는지 질문해 볼 가치가 있습니다.

우리의 모델에는 근본적인 약점이 있기 때문입니다. 모델은 이른바 보조선 (auxiliary constructions)을 긋는 데 어려움을 겪습니다. 많은 어려운 기하학 문제를 풀기 위해서는 이미 도표에 있는 것이 아닌 추가적인 선이나 도형을 그려 넣어야 합니다. 예를 들어, 삼각형 내각의 합이 180도임을 증명하고 싶다고 가정해 봅시다. 여기 아주 매끄러운 방법이 있습니다. 삼각형의 위쪽과 아래쪽에 두 개의 평행선을 그립니다. 이것이 보조선 (auxiliary construction)입니다. Z자 모양 안쪽에 표시된 $\alpha$ 각도들은 서로 같습니다.

마찬가지로 이쪽에 표시된 $\beta$ 각도들도 같습니다. 이제 삼각형의 나머지 각을 $\gamma$라고 부릅시다. 그러면 이제 방정식만 풀면 됩니다. 우리는 맨 위의 보라색 선이 직선이기 때문에 $\alpha + \gamma + \beta$가 180도라는 것을 알고 있습니다. 그런데 $\alpha, \beta, \gamma$는 또한 삼각형의 각도이기도 하므로, 그 합은 180도가 됩니다. 이제 끝났습니다. 여기서 핵심 단계는 위아래에 두 선을 그리는 것이었습니다. 일단 그것을 수행하고 나면, 우리는 이미 알고 있는 사실들로부터 정리를 도출할 수 있었습니다. 어떤 의미에서, 이것이 바로 기하학 문제를 매우 재미있게 만드는 요소입니다.

이 분야의 진정한 보석들은 항상 적절한 아이디어를 추가하는 것이 마치 전혀 예상치 못한 곳에서 갑자기 튀어나온 것처럼 느껴집니다. IMO 기하학 문제에서는 일반적으로 도식에 단 하나가 아니라 여러 개의 보조선 (auxiliary constructions)을 추가해야 합니다. 이는 기계에게는 나쁜 소식인데, 매 단계마다 무한한 탐색 공간 (search space)이 존재함을 의미하기 때문입니다. 바로 이 지점에서 AI가 등장합니다. DeepMind 팀은 오직 보조선 (auxiliary constructions)을 생성하는 것만을 유일한 임무로 하는 언어 모델 (language model)을 구축했습니다. 이 언어 모델의 입력값은 문제 설명과 지금까지 생성된 증명 단계들이었습니다.

지금은 제가 영어로 쓰고 있지만, 이전에 언급했던 기하학 코딩 언어를 사용하여 입력해야 한다는 점을 명심하세요. 언어 모델의 출력값은 보조선 (auxiliary construction)이 될 것입니다. 즉, 도식 위에 추가되는 점이나 도형입니다. 이를 바탕으로 AlphaGeometry가 전체적으로 어떻게 작동하는지 설명하겠습니다. 첫째, 문제 설명을 언어 모델에 입력합니다. 그러면 모델이 보조선 (auxiliary construction)을 반환할 것입니다. 둘째, 이 새로운 도식을 DD plus AR에 제공합니다. 그러면 종료될 때까지 일련의 단계들을 출력할 것입니다.

이 출력값을 다시 언어 모델에 입력합니다. 그러면 모델은 또 다른 보조선 (auxiliary construction)을 생성할 것입니다. 이 새로운 출력값을 다시 DD plus AR에 입력합니다. 문제가 해결되거나 시간이 다 될 때까지 이 절차를 반복합니다. 간단히 말해서, 언어 모델은 영리한 보조선 (auxiliary constructions)을 생각해내는 창의적인 두뇌 (creative brain)입니다. 반면에 DD plus AR은 순수 논리를 사용하여 알려진 사실로부터 새로운 사실을 도출하는 논리적인 두뇌 (logical brain)입니다. 즉, 창의적인 두뇌가 영리한 아이디어를 생각하면, 논리적인 두뇌가 그로부터 사실들을 도출해내는 것입니다.

창의적인 두뇌가 또 다른 아이디어를 생각하면, 논리적인 두뇌 (logical brain)는 그로부터 훨씬 더 많은 것들을 도출해냅니다. 이런 식으로 계속해서 반복됩니다. 지금까지 우리는 이 언어 모델 (language model)에 대해 이야기해 왔고, 그것은 아주 좋지만, 우리가 아직 논의하지 않은 한 가지가 있습니다. 바로 이 모델들이 훈련 데이터 (training data)를 어디에서 얻느냐는 것입니다. 왜냐하면 온라인상에는 풀이가 포함된 IMO 기하학 문제들이 그리 많지 않기 때문입니다. 따라서 다른 무언가를 해야만 합니다. Alpha Geometry 팀은 매우 흥미로운 방식을 통해 이 문제를 우회했습니다. 그들은 자신들만의 훈련 데이터를 직접 생성했습니다.

훈련 데이터를 위한 샘플 문제와 풀이를 생성하는 방법은 다음과 같습니다. 평면 위에 수많은 점과 선을 무작위로 배치합니다. 그런 다음 DD plus AR을 사용하여 도출할 수 있는 모든 것을 도출합니다. 예를 들어, 여러 각도가 같다거나, 여러 선이 평행하다는 것 등을 찾아냅니다. 예를 들어, 삼각형의 세 내각의 합이 180도라는 결론을 내릴 수도 있습니다. 이제 역순으로 진행합니다. 도표의 일부 부분을 지웁니다. 이제 우리는 문제를 제시할 수 있습니다. '이 삼각형에서 각의 합이 180도임을 보이시오'와 같은 식입니다. 이를 해결하기 위해서는 우리가 지웠던 선들을 다시 그려야 하는데, 이것이 바로 보조선 (auxiliary constructions)이 됩니다.

이런 식으로 Alpha Geometry는 새로운 훈련 데이터를 생성했습니다. 그들은 평면에 수많은 선과 점을 무작위로 배치했습니다. 그리고 DD plus AR을 사용하여 그로부터 수많은 알려진 정리 (theorems)들을 도출했습니다. 그러고 나서 도표의 일부를 지웠습니다. 따라서 만약 당신이 스스로 그 정리에 도달하고자 한다면, 보조선 (auxiliary construction)을 사용하여 해당 부분들을 다시 그려 넣어야만 합니다. 실제로 그들은 수억 개의 합성 증명 (synthetic proof) 예시를 생성했습니다. 그중 총 900만 개는 적어도 하나 이상의 보조선 (auxiliary construction)을 필요로 했습니다.

이 과정에서 생성된 매우 복잡한 도식(diagrams)의 몇 가지 예시가 여기 있습니다. 가장 복잡한 합성 증명 (synthetic proof)은 두 개의 보조선 (auxiliary constructions)을 포함하여 247단계라는 인상적인 길이를 가졌습니다. 이 모든 데이터를 사용하여 그들은 언어 모델 (language model)을 학습시킬 수 있었습니다. 그렇다면 이 전체 모델의 성능은 어떠했을까요? DD가 30문제 중 7문제를 해결했다는 점을 상기해 보십시오. DD에 AR과 인간의 사각형 측정법 (human quadratureistics)을 더했을 때는 30문제 중 18문제를 해결했습니다. 만약 DD와 AR을 약간의 미세 조정 (fine tuning)을 거친 언어 모델과 결합한다면, 30문제 중 25문제를 해결할 수 있었습니다.