Korean, Edit

Installing and Understanding AlphaGeometry

Recommended post: 【Algorithm】 Algorithm & Machine Learning Index

1. Overview

2. Installation Process

3. Syntax

a. IMO Geometry Problem Solving

b. Reconstruction and Solution of jgex_ag_231 Problem

c. Natural Language Processing and Large Language Models

1. Overview

⑴ Introduction

① AlphaGeometry: A language model submitted to a Nature publication that implements symbolic deduction, capable of solving geometry problems at the level of the International Mathematical Olympiad (IMO).

② Developed by Google DeepMind, it appears to be an advancement of the hypothesis-generating model FunSearch. (ref)

⑵ Principle

① Meaning of a symbol: The process of vectorizing each proposition and placing it on an embedding space.

② Symbolic deduction in geometry: Similar to “Euclid’s Elements,” it starts with axioms about lines, constructions, and concentric circles, leading to the creation of new propositions.

③ When given the conditions of a problem, it continuously searches for new true propositions within the search space to prove the given propositions.

④ This process can be likened to how a person might ponder a math problem for a long time before finally discovering the solution.

⑤ More specifically, 1) it represents the given geometry problem as points, lines, and surfaces, 2) creates a graph data structure, and then 3) operates by connecting the graph data structure with the theorem set.

○ In that case, is it possible to represent medical data as a graph data structure, connect it with clinical information, and implement a logical inference model? ([The Present and Future of the Bio Industry](https://jb243.github.io/pages/2411))

⑶ Process

① AlphaGeometry primarily solves problems through angle chasing.

○ Many geometry problems can be solved by angle chasing. For example, the proposition that four points lie on a circle (cyclic proposition) is equivalent to the condition that the circumferential angles of two triangles sharing the same base are equal.

② Step 1. DD+AR: Repeated use of cyclic quadrilaterals and similar triangles in geometry, more akin to classical algorithms than to AI (ref).

③ Step 2. AlphaGeometry mode: Adds new points randomly and then performs DD+AR, using an LLM-based approach.

○ The addition of new points is a heuristic process in humans, now made possible creatively with the advent of transformer-based LLMs.

⑷ Limitations

① Limitation 1. While geometric problems are based on definitive propositions leading to logical conclusions, real-world problems often depend on indeterminate propositions for decision-making.

② Limitation 2. Geometric problems often involve equivalence issues, whereas real-world decision-making frequently involves comparative issues.

○ Example of equivalence issue: Being on the same circle, M is the midpoint of A and B, etc.

○ Example of comparative issue: Will treating a breast cancer patient with Gemcitabine increase survival rates?

○ Can AlphaGeometry, which solves equality problems, solve comparison problems given the intrinsic limitations of triangles?

③ Limitations 3. Geometric problems deal with bidirectional propositional relationships (where two propositions are necessary and sufficient conditions for each other), but in real-world decision-making, there are many unidirectional propositional relationships.

○ In other words, if A → B holds, then in geometric problems B → A also holds. However, in real-world decision-making, it is often the case that B ⇏ A.

○ Similarly, if A → B holds, then in geometric problems ~A → ~B also holds. However, in real-world decision-making, it is often the case that ~A ⇏ ~B.

⑸ Significance

① Significance 1. The first model for logical reasoning. ([AI That Generates Hypotheses: The Beginning of the Idea](https://jb243.github.io/pages/2379))

② Significance 2. Possibility for logical reasoning on a large scale: If solving an IMO problem involves linking dozens of propositions, could humanity connect over a thousand propositions to derive new conclusions through AI? This may be possible through AI, marking a breakthrough in the horizons of cognition. ([The Horizon of Cognition and the Breakthrough Called AI](https://jb243.github.io/pages/2410))

③ Significance 3. Even if there is an incorrect proposition, it does not affect the final logical reasoning.

2. Installation Process

⑴ Since installing according to the official documentation results in an error, I followed the procedure below.

⑵ Step 1: Run the following command on an Ubuntu server.

① In my case, I used 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

⑶ Step 2: Install the following packages.

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

⑷ Step 3: Replace run.sh in the corresponding directory with the following file (ref).

① Note: The original paper uses BATCH_SIZE=32, BEAM_SIZE=512, and DEPTH=16, so these values are reflected.

⑸ Step 4: Properly comment out matplotlib.use('TkAgg') and the draw function in numericas.py.

① Reason: Since the script is running on a headless server without a GUI, executing a drawing function related to matplotlib results in the following error:

ImportError: Cannot load backend 'TkAgg' which requires the 'tk' interactive framework, as 'headless' is currently running

⑹ Step 5: Run the following command:

bash run.sh

⑺ Run AlphaGeometry in ddar mode: Replace the example in the run.sh file with the code below and reinstall.

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

⑻ Run AlphaGeometry in alphageometry mode: Replace the example in the run.sh file with the code below and reinstall.

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. Syntax

⑴ Definition of points, lines, and planes

① d = free

○ y = free y

② a b = segment a b: AB is a line segment

○ b c = segment: BC is a line segment

③ a b c = triangle: ABC is a triangle

④ d = eq_triangle d a b: DAB is an equilateral triangle

⑤ s c p = iso_triangle s c p: SCP is an isosceles triangle with SC and SP being equal in length

⑥ c a b = r_triangle c a b: CAB is a right triangle with ∠C being a right angle

⑦ c a b = risos c a b: Given a right triangle ABC where AB is equal to AC and AB is perpendicular to AC

⑧ a b c d = quadrangle a b c d: ABCD is a quadrangle

⑨ d e = square a c d e: DE is two points of the square ACDE

⑩ a b c d = rectangle a b c d: ABCD is a rectangle

⑪ a b c d = trapezoid a b c d: ABCD is a trapezoid with AB and CD parallel to each other.

⑫ a b c d = eq_trapezoid a b c d: ABCD is an isosceles trapezoid with AB and CD parallel, and AD equal to 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 is a pentagon

⑵ Definition of special points

① o = midpoint o b c: O is the midpoint of segment BC

② o = circle o a b c: O is the circumcenter of triangle ABC

○ o1 = circle a d c: O1 is the circumcenter of triangle ADC

○ o = circumcenter o b i c: O is the circumcenter of triangle BIC

③ i = incenter i a b c: I is the incenter of triangle ABC

④ t1 t2 t3 i = incenter2 t1 t2 t3 i a b c: The incircle I of triangle ABC touches BC, CA, and AB at T1, T2, and T3, respectively

⑤ h = orthocenter h a b c: H is the orthocenter of triangle ABC

⑥ t = mirror t r s: S is the midpoint of RT

⑦ x1 = reflect x1 h1 t1 t2: X1 is the reflection of H1 over line segment T1T2

⑧ w@6.9090049230038776_-1.3884003936987552: W is the point at (6.9090049230038776, -1.3884003936987552)

⑨ m l k j = excenter2 m l k j a b c: J is the excenter of triangle ABC, and M, L, K are the feet of the perpendiculars from J to BC, AC, and AB, respectively

⑶ A point is on a specific line or circle

① a = on_line a b q: A, B, and Q are collinear (B does not necessarily lie between A and Q)

○ a1 = on_line b c: A1 is on the line segment BC

② m = on_circle m g1 a: M is on the circle G1 passing through A

③ 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 is on the perpendicular bisector of RS

○ x = on_bline b c: X is on the perpendicular bisector of BC

⑤ c = on_pline c m a b: Line segment CM is parallel to AB

○ q = on_pline p a b: Line segment PQ is parallel to AB

⑥ q = on_tline q m w m: Line segments QM and WM are perpendicular or Q is on the circle tangent to WM at point M

○ ` h = on_tline b a c`: The line segment HB is perpendicular to AC, or H is the point where a circle tangent to line segment AC passes through point B.

⑦ h1 = foot h1 a b c: H1 is the foot of the perpendicular from A to BC

⑧ q = on_dia q a h: AQ is perpendicular to HQ

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

○ e = eqdistance d b c: ED = BC

⑩ x = parallelogram e a m x: X is the remaining vertex of parallelogram EAMX

⑪ q t p s = cc_tangent q t p s i1 f1 i2 f2: When there are circles centered at I1 passing through F1 and at I2 passing through F2, the common tangents of the two circles are QT and 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

⑷ A point is at a specific angle

① f = angle_bisector f b a z: F is on the angle bisector of ∠BAZ

○ d = angle_bisector b a c: D is on the angle bisector of ∠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 = ∠P1PC

⑤ c = s_angle b a c 60

⑸ Definition of problems

① ? cong o p o q: Show that OP = OQ

② ? coll x o a: Show that X is on segment OA

③ ? perp k t o1 t: Show that segment KT is perpendicular to segment O1T

④ ? para d e f g: Show that segment DE is parallel to FG

⑤ ? eqangle e c e j e j e f: Show that ∠CEJ = ∠JEF, i.e., EJ bisects ∠CEF

○ ? eqangle e c c d d f f c: Show that ∠ECD = ∠DFC

○ ? eqangle f g f b c f c b: Show that ∠GFB = ∠FCB

⑥ ? cyclic p q r m: Show that P, Q, R, and M lie on the same circle (cyclic quadrilateral proof)

⑦ ? eqratio k k1 l l1 r q r p: Show that KK1 / LL1 = RQ / RP (where AB denotes the length of segment AB)

⑧ ? midp g a d : Show that G is the midpoint of AD

⑨ ? simtri e f g e c b : Show that ΔEFG is similar to ΔECB

⑩ ? contri e a b a b e

Input: 2024.05.05 22:23