【머신러닝】 AlphaGeometry 설치 및 이해

AlphaGeometry 설치 및 이해

 

추천글 : 【알고리즘】 알고리즘·머신러닝 목차 

---

1. 개요 [본문]

2. 설치 과정 [본문]

3. 문법 [본문]

---

a. IMO 기하 문제 풀이

b. jgex_ag_231 문제 재구성 및 풀이

c. 자연어 처리와 거대 언어 모델 

---

 

1. 개요 [목차]

⑴ 서설

① AlphaGeometry : 네이처 논문에 투고된 언어 모델로서 symbolic deduction을 구현하여 IMO 수준의 기하 문제를 풀 수 있음

② Google DeepMind에서 만든 알고리즘으로, 가설을 생성하는 모델인 FunSearch에서 더 발전시켜 만든 것으로 보여짐 (ref)

⑵원리 

① symbol의 의미 : 각 명제를 벡터화(vectorization)하여 임베딩 스페이스 위에 올려놓는 것 

② 기하학에서의 symbolic deduction : 《유클리드 원론》처럼 직선, 작도, 동심원 등에 관한 공리에서 시작하여 새로운 명제를 만드는 것

③ 문제의 조건이 주어져 있을 때, 주어진 명제를 증명하기 위해 search space 안에서 계속 새로운 참인 명제들을 탐색하는 접근을 취함

④ 위 과정은 사람이 한 수학 문제를 오래 고민할 때 비로소 답을 찾아내는 것에 비유할 수 있음

⑤ 더 구체적으로는, 1) 주어진 수학 문제를 점, 선, 면으로 표현하고, 2) 그래프 자료 구조를 만든 뒤, 3) 그래프 자료 구조와 theorem set을 연결하는 식으로 작동한다고 할 수 있음 

○ 그렇다면 의료 데이터를 그래프 자료 구조로 표현하고, clinical information과 연결하여 logical inference 모델을 구현할 수 있는가? (`바이오 산업의 현재, 그리고 미래`)

⑶ 과정 

① AlphaGeometry는 그 중 각 추적(angle-chasing) 위주로 문제를 풂

○ 생각보다 많은 기하 문제가 각 추적으로 풀 수 있음. 예를 들어, 네 점이 한 원 위에 있다는 명제(cyclic preposition)는 밑변을 공유하는 두 삼각형의 원주각이 같다는 것과 필요충분조건

② 단계 1. DD+AR : 도형에서 순환 사각형과 유사 삼각형을 반복적으로 활용하는 것. AI라고 하기보다는 고전 알고리즘에 가까움 (ref)

③ 단계 2. alphageometry 모드 : LLM 기반 방식으로 새로운 점을 임의로 추가한 뒤 DD+AR을 수행 

○ 새로운 점을 추가하는 과정은 인간의 휴리스틱한 과정인데 트랜스포머 기반의 LLM이 등장함에 따라 그런 창의적인 시도도 가능해짐

⑷ 한계 

① 한계 1. 기하 문제는 확정적 명제를 바탕으로 새로운 논리적 결론을 만드는 모델이지만, real-world problem은 불확정적 명제를 바탕으로 결정을 내려야 하는 문제에 해당함

② 한계 2. 기하 문제는 보통 동등 문제가 많지만, 현실의 의사 결정에서는 비교 문제가 많음

○ 동등 문제의 예 : 한 원 위에 있다, M은 A와 B의 중점이다 등

○ 비교 문제의 예 : 유방암 환자에게 Gemcitabine을 처리하면 생존율이 증가할 것인가?

○ 삼각형의 내적 한계로 인해 동등 문제를 푸는 AIphaGeometry가 비교 문제를 풀 수 있는가?

③ 한계 3. 기하 문제는 양방향 명제관계(필요충분관계에 있는 두 명제)를 다루지만, 현실의 의사 결정에서는 단방향 명제관계가 많음

○ 즉, A → B가 성립한다면, 기하 문제는 B → A가 성립하는 반면 현실의 의사 결정은 B ⇏ A인 경우도 많음

○ 비슷하게 A → B가 성립한다면, 기하 문제는 ~A → ~B가 성립하는 반면 현실의 의사 결정은 ~A ⇏ ~B인 경우도 많음

⑸ 의의 

① 의의 1. 최초의 논리 추론 모델 (`가설을 생성하는 AI, 그 아이디어의 시작`)

② 의의 2. 대규모 명제에 대한 논리 추론 가능성 : IMO 풀이도 수십 개의 명제의 연결에 불과하다면, 인류는 1000개 이상의 명제를 연결하여 새로운 결론을 얻을 수 있는가? 그것이 AI를 통해 가능할 수도 있다 (`인지의 지평선과 AI라는 돌파구`)

③ 의의 3. 틀린 명제가 있어도, 이것이 최종 논리적 추론에 영향을 주지 않음 

 

 

2. 설치 과정 [목차]

⑴ 공식 문서에서와 같은 절차로 설치하면 오류가 나서 다음과 같은 절차를 따름 

⑵ 단계 1. Ubuntu 서버에서 다음을 실행 : 필자의 경우 Ubuntu 22.04.3 LTS (GNU/Linux 5.15.0-105-generic x86_64)를 사용

 

sudo apt install python3-virtualenv
conda create -n alphageometry python=3.10.9
conda activate alphageometry
git clone https://github.com/google-deepmind/alphageometry.git
cd alphageometry

 

⑶ 단계 2. 다음과 같은 패키지 설치 

 

pip install array-record==0.4.1 
pip install clu==0.0.7 
pip install seqio==0.0.18 
pip install seqio-nightly==0.0.17.dev20231013 
pip install t5==0.9.4 
pip install tensorflow-datasets==4.9.3 
pip install mesh-tensorflow[transformer]==0.1.21 
pip install tfds-nightly==4.9.2.dev202308090034
pip install matplotlib

 

⑷ 단계 3. 해당 디렉토리 내 run.sh를 다음 파일로 교체 (ref) 

 

run.sh

0.00MB

 

① 실제 페이퍼에서는 BATCH_SIZE=32, BEAM_SIZE=512, DEPTH=16를 사용했으므로 이를 반영

⑸ 단계 4. numericas.py의 matplotlib.use('TkAgg') 및 draw 함수를 적절히 주석 처리

① gui가 없는 서버에서 실행하다보니 matplotlib 관련 드로잉 함수 실행 시 다음 에러가 발생하기 때문 : ImportError: Cannot load backend 'TkAgg' which requires the 'tk' interactive framework, as 'headless' is currently running

⑹ 단계 5. bash run.sh 

⑺ ddar 모드로 AlphaGeometry 실행하기 : run.sh 파일 안에 있는 예제를 아래 코드로 대체하고 다시 설치

 

python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/imo_ag_30.txt \
--problem_name=translated_imo_2000_p1 \
--mode=ddar \
"./defs.txt"

 

⑻ alphageometry 모드로 AlphaGeometry 실행하기 : run.sh 파일 안에 있는 예제를 아래 코드로 대체하고 다시 설치

 

python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/imo_ag_30.txt \
--problem_name=translated_imo_2000_p6 \
--mode=alphageometry \
"./defs.txt" \
"${SEARCH_ARGS[@]}" \
"${LM_ARGS[@]}"

 

 

3. 문법 [목차]

⑴ 점, 선, 면 정의

① d = free 

○ y = free y 

② a b = segment a b : AB는 선분이다

○ b c = segment : BC는 선분이다

③ a b c = triangle : ABC는 삼각형이다 

④ d = eq_triangle d a b : DAB는 정삼각형이다 

⑤ s c p = iso_triangle s c p : SCP는 SC와 SP가 길이가 같은 이등변 삼각형이다

⑥ c a b = r_triangle c a b : CAB는 ∠C가 직각인 직각삼각형이다

⑦ c a b = risos c a b : AB = AC이고 AB와 AC가 수직한 직각삼각형 ABC가 주어져 있다

⑧ a b c d = quadrangle a b c d : ABCD는 사각형이다 

⑨ d e = square a c d e : DE는 정사각형 ACDE의 두 점이다

⑩ a b c d = rectangle a b c d : ABCD는 직사각형이다 

⑪ a b c d = trapezoid a b c d : ABCD는 AB와 CD가 평행한 사다리꼴이다

⑫ a b c d = eq_trapezoid a b c d : ABCD는 AB와 CD가 평행하고, AD = BC인 등변사다리꼴이다

⑬ a b c d = isquare a b c d

⑭ c = nsquare c b a

⑮ d = psquare d a b 

⑯ a b c d e = pentagon a b c d e : ABCDE는 오각형이다 

⑵ 특수한 점 정의

① o = midpoint o b c : O는 선분 BC의 중점이다 

② o = circle o a b c : O는 삼각형 ABC의 외심이다

○ o1 = circle a d c : O1은 삼각형 ADC의 외심이다 

○ o = circumcenter o b i c : O는 삼각형 BIC의 외심이다

③ i = incenter i a b c : I는 삼각형 ABC의 내심이다

④ t1 t2 t3 i = incenter2 t1 t2 t3 i a b c : 삼각형 ABC의 내접원 I는 BC, CA, AB와 각각 T1, T2, T3에서 만난다

⑤ h = orthocenter h a b c : H는 삼각형 ABC의 수심이다

⑥ t = mirror t r s : S는 RT의 중점이다

⑦ x1 = reflect x1 h1 t1 t2 : X1은 선분 T1T2에 대한 H1의 대칭점

⑧ w@6.9090049230038776_-1.3884003936987552 : (6.9090049230038776, -1.3884003936987552)에 있는 점 W

⑨ m l k j = excenter2 m l k j a b c : J는 삼각형 ABC의 내심이고, M, L, K는 각각 J에서 BC, AC, AB에 내린 수선의 발

⑶ 점이 특정 선 또는 원 위에 있다

① a = on_line a b q : A, B, Q가 한 선 상에 있다 (다만, 반드시 B가 AQ 사이에 있어야 하는 건 아니다)

○ a1 = on_line b c : A1이 선분 BC 위에 있다 

② m = on_circle m g1 a : M은 A를 지나는 원 G1 위에 있다

③ z = on_aline z a p a b x : ∠ZAP = ∠ABX이다

○ e = on_aline d a d c b : ∠EDA = ∠DCB이다

④ o = on_bline o r s : O는 RS의 수직이등분선 위에 있다

○ x = on_bline b c : X는 BC의 수직이등분선 위에 있다

⑤ c = on_pline c m a b : 선분 CM과 AB는 평행하다

○ q = on_pline p a b : 선분 PQ와 AB는 평행하다 

⑥ q = on_tline q m w m : 선분 QM과 WM은 수직하다 또는 Q는 선분 WM과 점 M에서 접하는 원이다 

○ h = on_tline b a c : 선분 HB와 AC는 수직하다 또는 H는 선분 AC와 점 B에서 접하는 원이다 

⑦ h1 = foot h1 a b c : H1은 A에서 BC 위로 수직선을 그었을 때의 교점이다

⑧ q = on_dia q a h : AQ와 HQ가 수직이다

⑨ d = eqdistance d a b c : AD = BC이다 

○ e = eqdistance d b c : ED = BC이다

⑩ x = parallelogram e a m x : X는 평행사변형 EAMX의 나머지 한 꼭짓점이다

⑪ q t p s = cc_tangent q t p s i1 f1 i2 f2 : I1을 중심으로 하고 F1을 지나는 원과 I2를 중심으로 하고 F2를 지나는 원이 있을 때, 두 원의 공통 접선이 각각 QT, PS이다

⑫ q = intersection_cc q a o p

⑬ f = intersection_lc f e d b

⑭ f = intersection_ll f b d c e 

⑮ f = intersection_lp f a c e c b 

⑯ d = intersection_pp d a b c c a b 

⑰ d = intersection_lt d c e a a o 

⑱ e = intersection_tt e b b o c c o 

⑲ f = shift f c a e 

⑳ r = lc_tangent r p a 

㉑ d x = trisegment d x c b 

㉒ d e = trisect d e b a c 

㉓ d e f = 3peq d e f c a b 

㉔ f g h i = 2l1c f g h i a b e d 

㉕ e g = e5128 e g a b c d 

⑷ 점이 특정 각도에 있다

① f = angle_bisector f b a z : F는 ∠BAZ의 이등분선 위에 있다 

○ d = angle_bisector b a c : D는 ∠BAC의 이등분선 위에 있다

② e = angle_mirror e c a d : ∠EAD와 ∠CAD는 같다 

③ a = eqangle2 b t e : ∠ABT와 ∠AET는 같다

④ p1 = eqangle3 p c a b c : ∠BAC와 ∠PP1C가 같다

⑤ c = s_angle b a c 60 : ∠BAC = 60°이다

⑸ 문제 정의

① ? cong o p o q : OP = OQ임을 보여라 

② ? coll x o a : X가 선분 OA 위에 있음을 보여라 

③ ? perp k t o1 t : 선분 KT가 선분 O1T와 수직함을 보여라

④ ? para d e f g : 선분 DE와 FG가 평행함을 보여라

⑤ ? eqangle e c e j e j e f : ∠CEJ = ∠JEF임을 보여라, 즉 EJ가 ∠CEF의 이등분선임을 보여라

○ ? eqangle e c c d d f f c : ∠ECD = ∠DFC임을 보여라

○ ? eqangle f g f b c f c b : ∠GFB = ∠FCB임을 보여라 

⑥ ? cyclic p q r m : P, Q, R, M이 한 원 위에 있음을 보여라 (내접사각형 증명; concyclic)

⑦ ? eqratio k k1 l l1 r q r p : KK1 / LL1 = RQ / RP임을 보여라 (단, AB는 선분 AB의 길이를 의미)

⑧ ? midp g a d : G는 AD의 중점임을 보여라 

⑨ ? simtri e f g e c b : ΔEFG는 ΔECB와 닮음인가?

⑩ ? contri e a b a b e 

 

입력: 2024.05.05 22:2