AlphaGeometry: 국제 수학 올림피아드 수준 기하학 정리 증명 AI

안녕하세요. 오늘은 구글 딥마인드에서 개발한 기하학 문제 해결 AI 모델인 AlphaGeometry에 대해서 알아보겠습니다. AlphaGeometry는 합성된 데이터와 기계 학습을 활용하여 기하학적 문제를 해결하고, 이로부터 얻은 해결책을 인간이 이해할 수 있는 형태로 제시하는 컴퓨터 프로그램으로, 수학적 정리를 증명하는 데 사용됩니다. 이는 특히 국제 수학 올림피아드 수준의 어려운 문제들을 해결하는 것에 중점을 둔 프로그램입니다. 이 블로그에서는 AlphaGeometry의 구성요소와 동작원리, 문제 풀이과정, 성능평가 결과 등에 대해 확인하실 수 있습니다.   

AlphaGeometry: 국제 수학 올림피아드 수준 기하학 정리 증명 AI

"이 포스팅은 쿠팡 파트너스 활동의 일환으로, 이에 따른 일정액의 수수료를 제공받습니다."

논문 개요 및 목적

• 논문 제목: "Solving Olympiad Geometry Without Human Demonstrations" 
• 논문 저자: Google DeepMind 
• 논문 게재 사이트: https://www.nature.com/articles/s41586-023-06747-5
• 논문 게재일: 2024년 1월

Solving Olympiad Geometry Without Human Demonstrations - 논문 발췌

이 논문의 주요 목적은 수학적인 정리와 정리에 대한 증명을 자동으로 수행하는 AlphaGeometry 시스템을 소개하고 설명하는 것입니다. 특히, 이 시스템은 도형과 공간에 관련된 기하학적 수학문제를 해결하는 데 중점을 두며, 이를 위해 대규모의 합성 데이터를 생성하고 언어 모델 및 상징적 추론 엔진과 협력하여 증명을 수행합니다. 

반응형

논문의 연구내용 및 결과 

AlphaGeometry가 문제를 풀기 위한 구성요소는 크게 상징적 연역 엔진(Symbolic Deduction Engine)과 언어 모델(language model)의 두 가지 요소로 이루어져 있습니다.

상징적 연역 엔진 (Symbolic Deduction Engine)

상징적 연역 엔진(Symbolic Deduction Engine)이란 상징적인 기호 논리를 사용하여 논리적인 계산과 추론을 수행하는 소프트웨어 또는 시스템입니다. 이러한 엔진은 주로 수학적 증명이나 논리 문제를 다루는 데에 활용됩니다. "Symbolic"은 수학적 기호 및 심볼을 나타내며, "Deduction(연역)"은 논리학 및 수학에서 특정 전제로부터 논리적인 규칙을 사용하여 결론을 도출하는 과정을 의미합니다. 

• 연역적 추론 (Deductive Reasoning): AlphaGeometry의 상징적 엔진은 논리 기반의 연역적 추론을 수행합니다. 연역적 추론은 주어진 전제들로부터 논리적인 규칙을 사용하여 특정한 결론을 도출하는 추론 방법입니다. 연역적 추론의 예시는 다음과 같습니다. 1. 전제 1: 모든 사람은 죽을 것이다. (A라는 진술) 2. 전제 2: 영희는 사람이다. (B라는 진술) 이때, 이 전제들로부터 다음과 같은 결론을 얻을 수 있습니다: 3. 결론: 영희는 죽을 것이다. (A → B, A, 따라서 B) 이것은 연역적 추론의 한 예입니다. 만약 첫 번째 전제가 "모든 사람은 죽을 것이다."이라는 논리적 진술이 참이라면, 두 번째 전제로부터 "영희는 죽을 것이다."라는 결론을 논리적으로 도출할 수 있습니다. 이와 같이, 연역적 추론은 주어진 전제들로부터 논리적으로 타당한 방식으로 결론을 도출하는 것을 의미합니다. 
• 대수적 규칙 (Algebraic Rules): Symbolic Engine은 대수적 규칙을 활용하여 각종 삼각비, 거리 및 비율과 같은 기하학적 속성을 계산하고 관계를 정의합니다. 대수적 규칙은 대수학에서 사용되는 다양한 규칙이나 법칙을 나타냅니다. 이러한 규칙들은 수학적인 표현과 계산을 단순화하거나 특정한 패턴을 이해하는 데 도움을 줍니다. 다음은 몇 가지 기본적인 규칙입니다. 교환법칙 (a + b = b + a, ab = ba), 결합법칙 ((a + b) + c = a + (b + c), (ab)c = a(bc)), 분배법칙 (a(b + c) = ab + ac), 항등원 (a + 0 = a, (0은 항등원), a * 1 = a (1은 항등원)), 역원 (a + (-a) = 0 (-a는 역원), a * (1/a) = 1 (1/a는 역원)) 이러한 규칙들은 수의 덧셈과 곱셈에 대한 기본적인 속성을 나타내며, 수학에서 다양한 연산을 논리적으로 다루는 데 사용됩니다. 

언어 모델 (Language Model)

• 생성적 텍스트 모델링 (Generative Text Modeling): 언어 모델은 텍스트 생성 능력을 갖춘 딥 뉴럴 네트워크입니다. AlphaGeometry는 이 언어 모델을 활용하여 보조 구성물을 생성하고, 증명 과정에 새로운 설명을 추가합니다. 언어 모델은 문장, 단락 또는 전체 텍스트를 생성하는 데 사용됩니다. AlphaGeometry에서는 이 언어 모델이 문제의 특정 부분에 대한 자연어 설명을 생성하고, 이를 증명 과정에 통합하여 보조 구성물을 도출합니다. 이러한 생성적 텍스트 모델은 AI가 자연어로 표현된 지식을 이해하고 활용하는 데 중요한 역할을 합니다.
• 보조 구성물 (Auxiliary Constructions): 언어 모델은 상징적 엔진이 찾지 못한 부분에서 도움이 필요한 지점에 대해 자동으로 보조 구성물을 제안합니다. 이는 주로 각종 각도, 비율, 거리 등을 포함하는 보조적인 구조물을 의미합니다.  예를 들어, 삼각형의 각을 나누는 점, 중점, 높이 등이 될 수 있습니다. 이러한 보조 구성물은 기존에 존재하지 않던 새로운 구조를 도입하여 문제를 해결하거나 논증을 보다 간결하게 만듭니다. 언어 모델의 생성적인 특성은 문제 해결에 창의적인 요소를 더하며, 상징적 엔진이 한계에 부딪혔을 때 새로운 통찰력을 제공합니다. 따라서 AlphaGeometry는 언어 모델과 상징적 엔진이 협력하여 보조 구성물을 생성하고 증명 과정을 발전시키는 데에 활용됩니다.

AlphaGeometry의 문제 풀이과정

다음은 AlphaGeometry의 문제 풀이과정입니다. 이 과정은 위에서 설명한 상징적 연역 엔진(Symbolic Deduction Engine)과 언어 모델(Language Model)의 협력적인 작동으로 이루어져 있습니다. 아래는 그 과정을 설명한 것입니다: 

• 1. 랜덤 정리 전제 샘플링(Random Theorem Premises Sampling): "정리 전제"란 어떤 기하학적 문제나 정리의 초기 조건이나 가정을 의미하며, 이 "랜덤 정리 전제 샘플링"은 무작위로 정리 전제를 선택하거나 생성하는 과정을 말합니다.  AlphaGeometry는 먼저 큰 집합에서 무작위로 정리 전제들을 샘플링합니다. 이 과정에서 다양한 조건과 성질을 가진 정리들을 선택하여 초기 문제 풀이의 기반이 될 데이터를 확보합니다.
• 2. 상징적 연역 엔진 실행(Symbolic Deduction Engine): 샘플링된 정리 전제를 기반으로 AlphaGeometry는 상징적 연역 엔진을 실행합니다. 이 엔진은 주어진 문제의 전제에서 새로운 진술을 체계적으로 도출할 때까지 끊임없이 연역을 수행합니다. 
• 3. 증명 탐색 루프(Proof Search Loop): 상징적 연역 엔진이 증명을 찾지 못하거나 새로운 진술을 더 이상 생성하지 못할 때까지 증명 탐색 루프가 계속됩니다. 이 루프에서는 번갈아가면서 상징적 연역 엔진과 언어 모델이 협력하여 문제 해결을 시도합니다.
• 4. 언어 모델 호출 및 보조 구성물 생성 (Auxiliary Constructions) : 증명 탐색 루프 중에 상징적 연역 엔진이 증명을 찾지 못할 경우, 언어 모델이 호출되어 보조적인 구성물을 생성합니다. 이는 주로 추가적인 각도, 비율, 거리 등을 포함하는 구조물로써 문제 해결을 위한 보조적인 정보를 제공합니다.
• 5. 반복 과정(Iterative Process): 상징적 연역 엔진과 언어 모델의 상호작용은 반복적으로 진행되며, 이러한 번갈아가는 과정이 증명이나 보조 구성물을 찾을 때까지 계속됩니다. 언어 모델이 생성한 정보는 상징적 연역 엔진에게 전달되어 추가적인 증명 탐색을 진행합니다. 
• 6. 최종 증명 완료: 증명이 완료되면 AlphaGeometry는 그 증명을 결과로 제시합니다. 이 과정을 통해 AlphaGeometry는 언어 모델의 창의성과 상징적 연역 엔진의 논리적인 연역 능력을 결합하여 기하학적 문제를 풀어냅니다.

이런 식으로 AlphaGeometry는 문제 해결에 있어서 기하학적인 연역 추론과 언어적인 텍스트 생성을 효과적으로 결합하여 보조 구성물을 활용한 합성문제와 새로운 증명을 찾아냅니다.

 

AlphaGeometry에서 사용되는 합성 데이터 생성 과정

위 그림은 AlphaGeometry에서 사용되는 합성문제와 새로운 증명의 생성 과정에 대한 설명입니다. 

• a. 랜덤 정리 전제 샘플링: 무작위로 정리 전제들을 샘플링합니다
• b. 상징적 연역 엔진을 이용한 증명 클로저 획득: "b"에서는 상징적 연역 엔진을 사용하여 증명 클로저(deduction closure)를 얻는 과정을 나타냅니다. 증명 클로저는 수학적인 증명을 표현하는 그래프로 주어진 정리나 문제에 대한 증명 과정을 구성하는 논리적인 단계들을 그림으로 나타낸 것입니다. 그림은 방향성이 있고 비순환적입니다. 
• b, c 최소 선행 조건 추적 및 해결책 형성: "b"에서 얻은 증명 클로저의 각 노드에 대해 해당 노드의 최소한의 선행 조건과 종속적인 추론을 추적(Traceback)합니다. 이를 통해 최소한의 선행 조건과 그에 해당하는 부분 그래프를 얻을 수 있습니다. "c"에서는 이 최소 선행 조건과 그에 해당하는 부분 그래프가 새로운 합성 문제와 그 해결책을 형성합니다. 이러한 합성 문제와 해결책은 샘플링된 무작위 정리 전제에 기반하여 만들어진 것이며, 언어 모델과 상징적 연역 엔진의 협력에 의해 생성됩니다. 

최소 선행 조건은 어떤 증명이나 문제를 해결하기 위해 필요한 가장 기본적이고 필수적인 전제나 조건을 나타냅니다. 즉, 어떤 명제를 증명하기 위해 반드시 알고 있어야 하는 최소한의 사실이나 조건들을 말합니다. 종속적인 추론은 어떤 주장이나 진술이 다른 진술에 종속되어 있는 경우를 나타냅니다. 한 진술이나 조건이 다른 진술이나 조건에 의존하여 성립하는 경우, 이를 종속적인 추론이라고 합니다. 종속적인 추론을 추적하는 것은 어떤 주장이 성립하기 위해 그 주장이 의존하는 최소한의 선행 조건을 찾아내는 것을 의미합니다.

• c. 보조 구성물과 언어 모델 학습: "c"에서는 언어 모델이 학습하는 과정 중에 나타나는 예시로, 부분 그래프에서는 HA와 BC의 생성에 불필요한 E와 D가 포함되어 있음을 나타냅니다. 이러한 불필요한 구성물이 언어 모델에 의해 학습되어, 추후에 언어 모델이 증명 생성 중에 유용한 보조 구성물을 자동으로 제안할 수 있도록 합니다.

이 과정을 통해 AlphaGeometry는 무작위 정리 전제에서 시작하여 상징적 연역 엔진과 언어 모델을 협력하여 최소 선행 조건을 추적하고, 이를 활용하여 합성 문제와 해결책을 생성하는 방식으로 새로운 증명을 자동으로 학습하고 생성합니다.

"이 포스팅은 쿠팡 파트너스 활동의 일환으로, 이에 따른 일정액의 수수료를 제공받습니다."

국제 수학 올림피아드 2015 문제 3번

다음 그림에서는 AlphaGeometry가 국제 수학 올림피아드 2015 문제 3번(IMO 2015 P3)을 어떻게 해결하는지에 대한 과정을 보여줍니다. 

국제 수학 올림피아드 2015 문제 3번 해결과정

e. IMO 2015 P3의 문제 설명과 그림

문제 설명: 삼각형 ABC가 AB ≤ AC인 삼각형이라고 가정합니다. Gamma를 그의 원주원, H를 그의 수직중심, F를 A에서의 수선의 발이라고 합시다. M은 BC의 중점이라고 하고, Q는 HQA = 90도가 되도록 하는 Gamma 상의 점이며, K는 HKQ = 90도가 되도록 하는 Gamma 상의 점입니다. A, B, C, K 및 Q가 모두 서로 다르며 이 순서대로 Gamma 상에 위치한다고 가정합니다. 삼각형 KQH와 FKM의 원주원이 서로 접한다는 것을 증명하세요.

f. IMO 2015 P3 문제의 해결책

이 문제의 해결책에서는 총 세 개의 보조 점(auxiliary points) D, G, E가 사용되었으며, 언어 모델의 출력(파란색)과 상징적 연역 엔진의 출력이 번갈아가며 표시되어 있습니다. 이렇게 번갈아가면서 나오는 출력은 해당 실행 순서를 반영하기 위함입니다. 그림에서 볼 수 있듯이, 언어 모델과 상징적 연역 엔진의 협력적 작업을 통해 IMO 2015 P3 문제가 해결되었습니다. 아래 더 보기를 클릭하시면 자세한 해결단계를 확인하실 수 있습니다. 

IMO 2015 P3 문제의 증명은 다음과 같은 단계로 이루어져 있습니다.

1. 보조 점 생성: 세 개의 보조 점 D, G, E를 생성합니다. 

2. 선 생성 및 수직관계 확인: B, C, M이 일직선이며 AH가 BC에 수직임으로부터 AH가 CM에도 수직임을 확인합니다. B, H, D가 일직선이며 AC가 BH에 수직임으로부터 AC가 HD에도 수직임을 확인합니다.

3. 각 관계 추론: 수직 각의 성질을 활용하여 여러 각의 크기를 유도합니다. 삼각형 내 각 관계를 활용하여 다양한 각의 크기를 등식으로 표현합니다.

4. 점 및 직선의 평행 관계 확인: 생성된 중점들을 이용하여 직선의 평행 관계를 확인합니다. 각 중점이 해당하는 변과 평행임을 보여줍니다.

5. 원의 성질 활용: 원의 성질을 이용하여 각 세 점에 대한 원의 중심을 구합니다. - 선분의 중점과 원의 중심을 이용하여 원의 성질을 보여줍니다.

6. 삼각형의 성질 및 원의 성질을 이용한 증명: 삼각형의 성질과 원의 성질을 결합하여 다양한 성질을 유도하고 등식을 도출합니다. 최종적으로 삼각형과 원이 서로 접한다는 결과를 도출합니다.

7. 점의 중심 및 선분의 중점 관련 성질 증명:삼각형의 성질을 통해 선분의 중점과 점의 중심을 연결하는 직선이 서로 일치함을 보여줍니다. 이를 통해 삼각형의 중심과 원의 중심이 일직선에 위치함을 확인합니다.

8. 다양한 각과 변에 대한 등식 증명: 다양한 각과 변에 대한 등식을 추론하여 삼각형과 원의 성질을 서로 연결 짓습니다. 이렇게 다양한 중간 단계를 거쳐 최종적으로 삼각형과 원의 성질을 이용하여 주어진 문제를 증명하고 있습니다.

기존의 기하학 정리 증명 프로그램과 달리 AlphaGeometry는 1억 개 이상의 새로운 문제를 인공적으로 생성한 학습 데이터로 학습합니다. 이로써 인공지능은 다양한 상황에서의 새로운 증명 방법을 학습하게 됩니다. 

AlphaGeometry의 성능 및 결과

AlphaGeometry는 국제 수학 올림피아드(IMO)의 고난도 문제에 대해 우수한 성과를 보입니다. 30문제 중 25문제를 해결하여, 이 분야에서 이전까지의 최고 수준을 뛰어넘었습니다. AlphaGeometry는 IMO 골드 메달 수준의 성능을 보이며, 기존의 최고 수준인 "Wu의 방법"을 크게 능가합니다. 아래 그림에서 확인할 수 있듯이 AlphaGeometry는 30개의 클래식 기하 문제 중 25개를 해결하여 선두를 달성했습니다.

AlphaGeometry의 성능 및 결과

https://fornewchallenge.tistory.com/

"이 포스팅은 쿠팡 파트너스 활동의 일환으로, 이에 따른 일정액의 수수료를 제공받습니다."

논문의 결론 및 전망

AlphaGeometry는 기하학 정리를 증명하는 데 있어서 국제수학올림피아드(IMO) 참가자들의 평균 성적을 초과하는 최초의 컴퓨터 프로그램입니다. 이 프로그램은 강력한 컴퓨터 대수학(Algebra) 및 검색 수준을 뛰어넘었습니다. 특히, "신경-기호합성" 접근방식을 통해  독립적으로 학습하고 증명을 생성하는 데 있어서 인간의 도움 없이도 뛰어난 성능을 보여주었습니다. 이러한 성과의 핵심은 다음과 같습니다.

• 문제해결 능력: AlphaGeometry는 IMO 참가자의 평균 성적을 초과하는 성과를 보여주었습니다. 이는 고급 컴퓨터 대수학 및 검색 수준을 뛰어넘는 것으로 기하학 문제를 해결할 수 있는 능력을 강조합니다.
• 신경-기호합성 접근: 논문에서 제시된 방법은 주석이나 인간의 도움 없이도 합성 데이터에서 증명을 생성하는 신경-기호합성 접근을 소개합니다. 이는 기하학적 정리 증명에 있어서 인간의 감독 없이도 기계가 학습하고 성공적으로 증명을 생성할 수 있다는 것을 시사합니다.
• 합성 데이터의 활용: 인공지능 모델을 학습시키기 위해 합성 데이터를 생성하고 활용하는 방법은 데이터 부족 문제에 대한 일반적인 해결책을 제시합니다. 특히, 수학적 도메인에서 데이터가 부족한 경우에도 합성 데이터를 통해 효과적인 학습이 가능합니다.

이러한 결과들은 AlphaGeometry가 수학 증명의 자동화 분야에서 혁신적인 발전을 이루어냄으로써, 향후 더 광범위한 수학 분야에도 확장될 수 있다는 가능성을 제시합니다.

 

이번 블로그에서는 구글 딥마인드에서 개발한 AlphaGeometry의 합성 데이터 생성과정, 문제 해결 과정, 그리고 국제 수학 올림피아드 2015 문제 3번의 해결책에 대한 상세한 내용을 다루었습니다. AlphaGeometry는 인공 신경망(neural network)과 기호적(symbolic) 추론을 통합하여 지능적인 의사 결정을 내리는 Neuro-symbolic 접근 방식을 통해 수학적 이론 증명의 자동화에 중요한 전환점을 제공합니다.

 

앞으로의 연구에서는 AlphaGeometry의 성능 향상을 위한 노력과 함께, 이러한 Neuro-symbolic 접근 방식을 다른 수학 분야나 현실 세계 문제 해결에 적용하는 연구가 나오기를 기대하면서 저는 다음에 더 유익한 자료를 가지고 다시 찾아뵙겠습니다. 감사합니다. 

 

 

2024.01.14 - [AI 논문 분석] - [AI 논문 분석] 트랜스포머 모델의 핵심기술, 어텐션 메커니즘

[AI 논문 분석] 트랜스포머 모델의 핵심기술, 어텐션 메커니즘