AlphaGeometry 체험 후기

 

https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/

AlphaGeometry: An Olympiad-level AI system for geometry

최근 구글 딥마인드에서 mo 기하 문제를 푸는 AI를 발표했다길래 궁금해져서 직접 설치하고 실행해봤다. https://github.com/google-deepmind/alphageometry 에서 설치할 수 있다.

 

AlphaGeometry로 문제를 풀기 위해서는 문제를 번역해야 하는데 문법 관련 문서를 찾아볼 수 없어서 예제와 imo 문제를 통해 문법을 직접 유추해서 번역했다. 예시로 KMO 2022 고등부 5번 문제를 번역해봤다.

kmo_2022_5
a b c = triangle a b c;
d e f i = incenter2 d e f i a b c;
p = on_line p a i, on_line p d f;
q = on_line q b i, on_line q e f
? cong p q c d

이등변삼각형이 아닌 예각삼각형이라는 조건이 빠져있긴 하지만 다른 imo 문제 번역도 빠져있는 걸로 봐서 별 상관 없는 것 같다. 그림을 그려보면 다음과 같다.

AlphaGeometry는 이 문제를 5초 이내에 해결한다. BATCH_SIZE=2, BEAM_SIZE=2, DEPTH=2로 하고 cpu 1개로 돌린 결과이므로 논문에 나온 세팅에서 돌리면 1초도 안 걸릴 것 같다.  단순 각돌리기로 풀리는 문제라 매우 빠르게 해결하는 것을 확인할 수 있다. AlphaGeometry의 풀이는 다음과 같다.

==========================
 * From theorem premises:
A B C G D E F H I : Points
∠GCA = ∠BCG [00]
∠BAG = ∠GAC [01]
D,C,B are collinear [02]
DG ⟂ BC [03]
A,C,E are collinear [04]
EG ⟂ AC [05]
F,A,B are collinear [06]
FG ⟂ AB [07]
A,G,H are collinear [08]
D,F,H are collinear [09]
F,E,I are collinear [10]
I,G,B are collinear [11]
 * Auxiliary Constructions:
: Points
 * Proof steps:
001. F,A,B are collinear [06] & D,C,B are collinear [02] & DG ⟂ BC [03] & FG ⟂ AB [07] ⇒  ∠GFB = ∠GDB [12]
002. ∠GFB = ∠GDB [12] ⇒  D,F,G,B are concyclic [13]
003. D,F,G,B are concyclic [13] ⇒  ∠DFB = ∠DGB [14]
004. E,C,A are collinear [04] & D,C,B are collinear [02] & DG ⟂ BC [03] & EG ⟂ AC [05] ⇒  ∠GEC = ∠CDG [15]
005. E,C,A are collinear [04] & D,C,B are collinear [02] & ∠GCA = ∠BCG [00] ⇒  ∠GCE = ∠DCG [16]
006. ∠GEC = ∠CDG [15] & ∠GCE = ∠DCG [16] (Similar Triangles)⇒  GE = GD [17]
007. E,C,A are collinear [04] & F,A,B are collinear [06] & FG ⟂ AB [07] & EG ⟂ AC [05] ⇒  ∠GEA = ∠AFG [18]
008. A,C,E are collinear [04] & F,A,B are collinear [06] & ∠GAC = ∠BAG [01] ⇒  ∠GAE = ∠FAG [19]
009. ∠GEA = ∠AFG [18] & ∠GAE = ∠FAG [19] (Similar Triangles)⇒  GE = GF [20]
010. ∠GEA = ∠AFG [18] & ∠GAE = ∠FAG [19] (Similar Triangles)⇒  AE = AF [21]
011. GE = GD [17] & GE = GF [20] ⇒  G is the circumcenter of \Delta DEF [22]
012. F,A,B are collinear [06] & AB ⟂ FG [07] ⇒  FA ⟂ FG [23]
013. G is the circumcenter of \Delta DEF [22] & FA ⟂ FG [23] ⇒  ∠AFD = ∠FED [24]
014. F,E,I are collinear [10] & G,I,B are collinear [11] & ∠DFB = ∠DGB [14] & F,A,B are collinear [06] & ∠AFD = ∠FED [24] ⇒  ∠IED = ∠IGD [25]
015. ∠IED = ∠IGD [25] ⇒  D,E,G,I are concyclic [26]
016. E,C,A are collinear [04] & D,C,B are collinear [02] & DG ⟂ BC [03] & EG ⟂ AC [05] ⇒  ∠GEC = ∠GDC [27]
017. ∠GEC = ∠GDC [27] ⇒  D,E,C,G are concyclic [28]
018. E,C,A are collinear [04] & F,A,B are collinear [06] & FG ⟂ AB [07] & EG ⟂ AC [05] ⇒  ∠GEA = ∠GFA [29]
019. ∠GEA = ∠GFA [29] ⇒  F,A,G,E are concyclic [30]
020. F,A,G,E are concyclic [30] ⇒  ∠FAG = ∠FEG [31]
021. A,G,H are collinear [08] & D,F,H are collinear [09] & ∠AFD = ∠FED [24] & F,A,B are collinear [06] & ∠FAG = ∠FEG [31] ⇒  ∠EGH = ∠EDH [32]
022. ∠EGH = ∠EDH [32] ⇒  D,E,G,H are concyclic [33]
023. D,E,G,I are concyclic [26] & D,E,C,G are concyclic [28] & D,E,G,H are concyclic [33] ⇒  E,I,D,C,H are concyclic [34]
024. F,A,B are collinear [06] & ∠AFD = ∠FED [24] ⇒  ∠EDF = ∠EFA [35]
025. F,A,B are collinear [06] & A,G,H are collinear [08] & A,C,E are collinear [04] & ∠BAG = ∠GAC [01] ⇒  ∠FAH = ∠HAE [36]
026. AE = AF [21] & ∠FAH = ∠HAE [36] (SAS)⇒  ∠AFH = ∠HEA [37]
027. F,A,B are collinear [06] & ∠AFH = ∠HEA [37] & D,F,H are collinear [09] & A,C,E are collinear [04] ⇒  ∠(DF-AC) = ∠(FA-EH) [38]
028. ∠EDF = ∠EFA [35] & ∠(DF-AC) = ∠(FA-EH) [38] ⇒  ∠(DE-AC) = ∠FEH [39]
029. F,E,I are collinear [10] & E,C,A are collinear [04] & ∠FEH = ∠(DE-AC) [39] ⇒  ∠IEH = ∠DEC [40]
030. E,I,D,C,H are concyclic [34] & ∠IEH = ∠DEC [40] ⇒  IH = DC
==========================

 

 

AlphaGeometry의 풀이를 읽어보면 C, I, E, G, D, H가 concyclic임을 증명하고 각 IEH와 DEC의 크기가 같다는 것을 보이는 방식으로 문제를 해결한다. 어려운 문제에서는 AlphaGeometry가 여러 보조선이나 점을 새로 잡은 후 점수가 높은 것부터 차례로 시도해보는 방식으로 해결한다고 한다.

 

논증기하는 풀이에 쓰이는 테크닉을 정형화하는 것이 상대적으로 쉬운 분야라 가능한 것 같다. 내 생각에 AI로 정수론, 조합론 문제를 푸는 건 훨씬 어려울 것 같다.

 

추가) KMO 2014 고등부 3번 문제를 BATCH_SIZE=4, BEAM_SIZE=4, DEPTH=4로 하고 로컬에서 돌려봤는데 8시간 실행 후 풀지 못한 채로 종료되었다.

 

추가2) FKMO 2022 4번 문제를 풀게 해봤다. 이 문제도 dd+ar 1회 실행으로 풀렸다. (보조선이나 점을 잡지 않고 풀었다.)

fkmo_2022_4
a b c = triangle a b c; f e d i = incenter2 f e d i a b c; h1 = foot h1 a b c; l = on_circle l i d, on_line l a h1; y = on_circle y i d, on_line y a h1; o1 = circumcenter o1 a b c; m = on_circle m o1 a, on_line m a i; o = circumcenter o b d e; n = on_circle n o l, on_line n a l; x = on_line x l d, on_line x m b; o2 = circumcenter o2 l n e ? cong o2 l o2 x
==========================
 * From theorem premises:
A B C G E F H I K L M N O P : Points
∠BAG = ∠GAC [00]
∠GCA = ∠BCG [01]
E,C,A are collinear [02]
EG ⟂ AC [03]
B,A,F are collinear [04]
FG ⟂ AB [05]
BC ⟂ HA [06]
I,H,A are collinear [07]
GI = GF [08]
KB = KC [09]
KA = KB [10]
L,A,G are collinear [11]
KL = KA [12]
MF = ME [13]
MB = MF [14]
MN = MI [15]
I,A,N are collinear [16]
B,O,L are collinear [17]
O,I,F are collinear [18]
PI = PN [19]
PN = PE [20]
 * Auxiliary Constructions:
D : Points
DG ⟂ BC [21]
D,B,C are collinear [22]
 * Proof steps:
001. E,C,A are collinear [02] & B,A,F are collinear [04] & FG ⟂ AB [05] & EG ⟂ AC [03] ⇒  ∠GEA = ∠AFG [23]
002. E,C,A are collinear [02] & B,A,F are collinear [04] & ∠GAC = ∠BAG [00] ⇒  ∠GAE = ∠FAG [24]
003. ∠GEA = ∠AFG [23] & ∠GAE = ∠FAG [24] (Similar Triangles)⇒  GE = GF [25]
004. ∠GEA = ∠AFG [23] & ∠GAE = ∠FAG [24] (Similar Triangles)⇒  AE = AF [26]
005. ∠GEA = ∠AFG [23] & ∠GAE = ∠FAG [24] (Similar Triangles)⇒  ∠EGA = ∠AGF [27]
006. GE = GF [25] & AE = AF [26] ⇒  EF ⟂ GA [28]
007. GE = GF [25] & MF = ME [13] ⇒  EF ⟂ GM [29]
008. G,A,L are collinear [11] & E,C,A are collinear [02] & ∠BAG = ∠GAC [00] ⇒  ∠BAL = ∠(LA-EC) [30]
009. KB = KC [09] & KA = KB [10] & KL = KA [12] ⇒  B,C,A,L are concyclic [31]
010. B,C,A,L are concyclic [31] ⇒  ∠BCA = ∠BLA [32]
011. B,C,A,L are concyclic [31] ⇒  ∠ABL = ∠ACL [33]
012. MN = MI [15] & PI = PN [19] ⇒  NI ⟂ MP [34]
013. G,A,L are collinear [11] & B,L,O are collinear [17] & E,C,A are collinear [02] & ∠BCA = ∠BLA [32] & NI ⟂ MP [34] & DG ⟂ BC [21] & I,A,N are collinear [16] & I,H,A are collinear [07] & BC ⟂ HA [06] ⇒  ∠(LA-BO) = ∠(EC-MP) [35]
014. ∠BAL = ∠(LA-EC) [30] & ∠(LA-BO) = ∠(EC-MP) [35] ⇒  ∠ABO = ∠(LA-MP) [36]
015. EF ⟂ GA [28] & EF ⟂ GM [29] & B,A,F are collinear [04] & B,L,O are collinear [17] & ∠ABO = ∠(LA-MP) [36] & L,A,G are collinear [11] ⇒  ∠GMP = ∠FBO [37]
016. GE = GF [25] & GI = GF [08] ⇒  GI = GE [38]
017. GE = GF [25] & GI = GF [08] ⇒  G is the circumcenter of \Delta EIF [39]
018. PN = PE [20] & PI = PN [19] ⇒  PI = PE [40]
019. GI = GE [38] & PI = PE [40] ⇒  EI ⟂ GP [41]
020. G,A,L are collinear [11] & ∠BAG = ∠GAC [00] ⇒  ∠BAL = ∠LAC [42]
021. B,C,A,L are concyclic [31] & ∠BAL = ∠LAC [42] ⇒  BL = LC [43]
022. KB = KC [09] & BL = LC [43] ⇒  BC ⟂ KL [44]
023. DG ⟂ BC [21] & EI ⟂ GP [41] & NI ⟂ MP [34] & I,A,N are collinear [16] & I,H,A are collinear [07] & BC ⟂ HA [06] & BC ⟂ KL [44] ⇒  ∠(PG-EI) = ∠(MP-KL) [45]
024. E,C,A are collinear [02] & EG ⟂ AC [03] ⇒  EG ⟂ EC [46]
025. D,B,C are collinear [22] & DG ⟂ BC [21] ⇒  DG ⟂ DB [47]
026. EG ⟂ EC [46] & DG ⟂ DB [47] ⇒  ∠EGD = ∠(EC-DB) [48]
027. B,L,O are collinear [17] & G,A,L are collinear [11] & ∠BCA = ∠BLA [32] & ∠EGD = ∠(EC-DB) [48] & E,C,A are collinear [02] & D,B,C are collinear [22] ⇒  ∠DGE = ∠(BO-LA) [49]
028. G,A,L are collinear [11] & ∠EGA = ∠AGF [27] ⇒  ∠(EG-LA) = ∠(LA-GF) [50]
029. ∠DGE = ∠(BO-LA) [49] & ∠(EG-LA) = ∠(LA-GF) [50] ⇒  ∠(DG-LA) = ∠(BO-GF) [51]
030. E,C,A are collinear [02] & B,A,F are collinear [04] & FG ⟂ AB [05] & EG ⟂ AC [03] ⇒  ∠GEA = ∠GFA [52]
031. ∠GEA = ∠GFA [52] ⇒  E,G,A,F are concyclic [53]
032. E,G,A,F are concyclic [53] ⇒  ∠EAG = ∠EFG [54]
033. E,G,A,F are concyclic [53] ⇒  ∠EGA = ∠EFA [55]
034. G is the circumcenter of \Delta EIF [39] & EG ⟂ EC [46] ⇒  ∠CEI = ∠EFI [56]
035. O,I,F are collinear [18] & B,L,O are collinear [17] & ∠(DG-LA) = ∠(BO-GF) [51] & L,A,G are collinear [11] & ∠EAG = ∠EFG [54] & E,C,A are collinear [02] & ∠CEI = ∠EFI [56] & BC ⟂ KL [44] & DG ⟂ BC [21] ⇒  ∠EIO = ∠(KL-BO) [57]
036. ∠(PG-EI) = ∠(MP-KL) [45] & ∠EIO = ∠(KL-BO) [57] ⇒  ∠(PG-OI) = ∠(MP-BO) [58]
037. O,I,F are collinear [18] & O,B,L are collinear [17] & ∠(PG-OI) = ∠(MP-BO) [58] ⇒  ∠GPM = ∠FOB [59]
038. ∠GMP = ∠FBO [37] & ∠GPM = ∠FOB [59] (Similar Triangles)⇒  MG:MP = BF:BO [60]
039. B,A,F are collinear [04] & D,B,C are collinear [22] & DG ⟂ BC [21] & FG ⟂ AB [05] ⇒  ∠BFG = ∠BDG [61]
040. ∠BFG = ∠BDG [61] ⇒  D,B,G,F are concyclic [62]
041. E,C,A are collinear [02] & D,B,C are collinear [22] & DG ⟂ BC [21] & EG ⟂ AC [03] ⇒  ∠GEC = ∠CDG [63]
042. E,C,A are collinear [02] & D,B,C are collinear [22] & ∠GCA = ∠BCG [01] ⇒  ∠GCE = ∠DCG [64]
043. ∠GEC = ∠CDG [63] & ∠GCE = ∠DCG [64] (Similar Triangles)⇒  GE = GD [65]
044. GI = GF [08] & GE = GF [25] & GE = GD [65] ⇒  G is the circumcenter of \Delta DIF [66]
045. G is the circumcenter of \Delta DIF [66] & DG ⟂ DB [47] ⇒  ∠BDI = ∠DFI [67]
046. B,A,F are collinear [04] & FG ⟂ AB [05] ⇒  GF ⟂ FB [68]
047. G is the circumcenter of \Delta DIF [66] & GF ⟂ FB [68] ⇒  ∠BFI = ∠FDI [69]
048. D,B,G,F are concyclic [62] ⇒  ∠DGB = ∠DFB [70]
049. D,B,C are collinear [22] & ∠BDI = ∠DFI [67] & ∠BFI = ∠FDI [69] & B,A,F are collinear [04] & ∠DGB = ∠DFB [70] ⇒  ∠DGB = ∠BDF [71]
050. D,B,G,F are concyclic [62] & ∠DGB = ∠BDF [71] ⇒  DB = BF [72]
051. MG:MP = BF:BO [60] & DB = BF [72] ⇒  MG:MP = DB:BO [73]
052. B,A,F are collinear [04] & EF ⟂ GA [28] & EF ⟂ GM [29] & ∠EGA = ∠EFA [55] ⇒  ∠EFB = ∠EGM [74]
053. MF = ME [13] & AE = AF [26] (SSS)⇒  ∠MEA = ∠AFM [75]
054. MB = MF [14] ⇒  ∠MFB = ∠FBM [76]
055. E,C,A are collinear [02] & ∠MEA = ∠AFM [75] & B,A,F are collinear [04] & ∠MFB = ∠FBM [76] ⇒  ∠ABM = ∠AEM [77]
056. ∠ABM = ∠AEM [77] ⇒  B,M,E,A are concyclic [78]
057. B,M,E,A are concyclic [78] ⇒  ∠BEM = ∠BAM [79]
058. B,A,F are collinear [04] & EF ⟂ GA [28] & EF ⟂ GM [29] & ∠BEM = ∠BAM [79] ⇒  ∠EBF = ∠EMG [80]
059. ∠EFB = ∠EGM [74] & ∠EBF = ∠EMG [80] (Similar Triangles)⇒  BE:BF = ME:MG [81]
060. BE:BF = ME:MG [81] & DB = BF [72] & MF = ME [13] ⇒  MG:EM = DB:BE [82]
061. MG:MP = DB:BO [73] & MG:EM = DB:BE [82] ⇒  BO:BE = MP:EM [83]
062. MB = MF [14] & MF = ME [13] ⇒  ME = MB [84]
063. ME = MB [84] & LB = LC [43] ⇒  ME:MB = LB:LC [85]
064. E,C,A are collinear [02] & ∠MEA = ∠AFM [75] & B,A,F are collinear [04] & ∠MFB = ∠FBM [76] ⇒  ∠CEM = ∠ABM [86]
065. E,C,A are collinear [02] & B,L,O are collinear [17] & ∠ACL = ∠ABL [33] ⇒  ∠ECL = ∠ABO [87]
066. ∠CEM = ∠ABM [86] & ∠ECL = ∠ABO [87] ⇒  ∠(EM-CL) = ∠MBO [88]
067. ∠(EM-CL) = ∠MBO [88] & B,O,L are collinear [17] ⇒  ∠EMB = ∠CLB [89]
068. ME:MB = LB:LC [85] & ∠EMB = ∠CLB [89] (Similar Triangles)⇒  ∠(BC-EM) = ∠LBE [90]
069. B,L,O are collinear [17] & ∠LBE = ∠(BC-EM) [90] & NI ⟂ MP [34] & DG ⟂ BC [21] & I,A,N are collinear [16] & I,H,A are collinear [07] & BC ⟂ HA [06] ⇒  ∠OBE = ∠PME [91]
070. MP:EM = BO:BE [83] & ∠OBE = ∠PME [91] (Similar Triangles)⇒  EO:EP = EB:EM [92]
071. MP:EM = BO:BE [83] & ∠OBE = ∠PME [91] (Similar Triangles)⇒  ∠OEP = ∠BEM [93]
072. EO:EP = EB:EM [92] & PN = PE [20] & MF = ME [13] & BM = MF [14] ⇒  BM:BE = EP:EO [94]
073. ME = MB [84] ⇒  ∠BEM = ∠MBE [95]
074. ∠OEP = ∠BEM [93] & ∠BEM = ∠MBE [95] ⇒  ∠MBE = ∠OEP [96]
075. BM:BE = EP:EO [94] & ∠MBE = ∠OEP [96] (Similar Triangles)⇒  MB:ME = PE:PO [97]
076. MB:ME = PE:PO [97] & ME = MB [84] & EP = IP [40] ⇒  PI = PO
==========================