google-deepmind/alphageometry

alphageometry's Issues

translated_imo_2000_p6 error --beam_size=512 --search_depth=16

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

I0123 17:33:55.019012 140364354609664 alphageometry.py:575] Solving: "a b c = triangle a b c; d = orthocenter d a b c; e f g h = incenter2 e f g h a b c; i = foot i a b c; j = foot j b c a; k = foot k c a b; l = reflect l i e f; m = reflect m j e f; n = reflect n j f g; o = reflect o k f g; p = on_line p l m, on_line p n o; q = on_pline q h d j; r = on_tline r o h q; s = on_pline s r b k; t = on_pline t h a p ? cong h p h e"
I0123 17:33:55.019272 140364354609664 graph.py:498]
I0123 17:33:55.019343 140364354609664 graph.py:499] a b c = triangle a b c; d = orthocenter d a b c; e f g h = incenter2 e f g h a b c; i = foot i a b c; j = foot j b c a; k = foot k c a b; l = reflect l i e f; m = reflect m j e f; n = reflect n j f g; o = reflect o k f g; p = on_line p l m, on_line p n o; q = on_pline q h d j; r = on_tline r o h q; s = on_pline s r b k; t = on_pline t h a p ? cong h p h e
I0123 17:33:59.821569 140364354609664 ddar.py:60] Depth 1/1000 time = 4.660033226013184
I0123 17:34:09.393961 140364354609664 ddar.py:60] Depth 2/1000 time = 9.572181463241577
I0123 17:34:29.777756 140364354609664 ddar.py:60] Depth 3/1000 time = 20.383514881134033
I0123 17:34:54.024996 140364354609664 ddar.py:60] Depth 4/1000 time = 24.24697208404541
I0123 17:35:22.954921 140364354609664 ddar.py:60] Depth 5/1000 time = 28.929654598236084
I0123 17:35:58.104779 140364354609664 ddar.py:60] Depth 6/1000 time = 35.14947986602783
I0123 17:36:37.170787 140364354609664 ddar.py:60] Depth 7/1000 time = 39.06558275222778
I0123 17:37:15.608809 140364354609664 ddar.py:60] Depth 8/1000 time = 38.43768525123596
I0123 17:37:53.945445 140364354609664 ddar.py:60] Depth 9/1000 time = 38.2583749294281
I0123 17:38:32.010860 140364354609664 ddar.py:60] Depth 10/1000 time = 37.94137620925903
I0123 17:39:09.888117 140364354609664 ddar.py:60] Depth 11/1000 time = 37.75762915611267
I0123 17:39:48.012754 140364354609664 ddar.py:60] Depth 12/1000 time = 38.102089405059814
I0123 17:39:48.013067 140364354609664 alphageometry.py:221] DD+AR failed to solve the problem.
I0123 17:39:48.013614 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : T h q o r 27 ; x00 s : P b k o s 28 ; x00
I0123 17:41:16.852997 140364354609664 alphageometry.py:565] LM output (score=-2.145489): "t : P a p h t 29 ;"
I0123 17:41:16.853293 140364354609664 alphageometry.py:566] Translation: "t = on_pline t h a p"

I0123 17:41:16.853357 140364354609664 alphageometry.py:575] Solving: "a b c = triangle a b c; d = orthocenter d a b c; e f g h = incenter2 e f g h a b c; i = foot i a b c; j = foot j b c a; k = foot k c a b; l = reflect l i e f; m = reflect m j e f; n = reflect n j f g; o = reflect o k f g; p = on_line p l m, on_line p n o; q = on_pline q h d j; r = on_tline r o h q; s = on_pline s o b k; t = on_pline t h a p ? cong h p h e"
I0123 17:41:16.853657 140364354609664 graph.py:498]
I0123 17:41:16.853727 140364354609664 graph.py:499] a b c = triangle a b c; d = orthocenter d a b c; e f g h = incenter2 e f g h a b c; i = foot i a b c; j = foot j b c a; k = foot k c a b; l = reflect l i e f; m = reflect m j e f; n = reflect n j f g; o = reflect o k f g; p = on_line p l m, on_line p n o; q = on_pline q h d j; r = on_tline r o h q; s = on_pline s o b k; t = on_pline t h a p ? cong h p h e
I0123 17:41:21.049736 140364354609664 ddar.py:60] Depth 1/1000 time = 4.052072763442993
I0123 17:41:31.150290 140364354609664 ddar.py:60] Depth 2/1000 time = 10.100180625915527
I0123 17:41:54.827009 140364354609664 ddar.py:60] Depth 3/1000 time = 23.67641544342041
I0123 17:42:17.896517 140364354609664 ddar.py:60] Depth 4/1000 time = 23.0691339969635
I0123 17:42:47.415402 140364354609664 ddar.py:60] Depth 5/1000 time = 29.51862072944641
I0123 17:43:22.044816 140364354609664 ddar.py:60] Depth 6/1000 time = 34.629090547561646
I0123 17:43:57.311384 140364354609664 ddar.py:60] Depth 7/1000 time = 35.2661554813385
I0123 17:44:31.885226 140364354609664 ddar.py:60] Depth 8/1000 time = 34.5734806060791
I0123 17:45:08.239387 140364354609664 ddar.py:60] Depth 9/1000 time = 36.28346276283264
I0123 17:45:44.790218 140364354609664 ddar.py:60] Depth 10/1000 time = 36.43162727355957
I0123 17:46:20.261463 140364354609664 ddar.py:60] Depth 11/1000 time = 35.3604793548584
I0123 17:46:57.564343 140364354609664 ddar.py:60] Depth 12/1000 time = 37.28116488456726
I0123 17:46:57.564695 140364354609664 alphageometry.py:221] DD+AR failed to solve the problem.
I0123 17:46:57.565226 140364354609664 alphageometry.py:565] LM output (score=-2.740839): "t : D p p r t 29 D l t r t 30 ;"
I0123 17:46:57.565277 140364354609664 alphageometry.py:566] Translation: "ERROR: Invalid predicate D p p r t"

I0123 17:46:57.565348 140364354609664 alphageometry.py:539] Depth 4. There are 6 nodes to expand:
I0123 17:46:57.565388 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : T a h h q 26 ; x00 r : P a h d r 27 ; x00 s : P d r f s 28 ; x00 t : D p o p t 29 T o p p t 30 ; x00
I0123 17:46:57.565432 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : T a h h q 26 ; x00 r : P a h d r 27 ; x00 s : P d r f s 28 ; x00 t : P b k l t 29 ; x00
I0123 17:46:57.565474 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : P b k p r 27 ; x00 s : T h p k s 28 ; x00 t : P d j p t 29 ; x00
I0123 17:46:57.565506 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : P b k p r 27 ; x00 s : T h p k s 28 ; x00 t : P f h k t 29 ; x00
I0123 17:46:57.565536 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : T h q o r 27 ; x00 s : P b k r s 28 ; x00 t : P a p h t 29 ; x00
I0123 17:46:57.565564 140364354609664 alphageometry.py:543] {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : T h q o r 27 ; x00 s : P b k o s 28 ; x00 t : P a p h t 29 ; x00
I0123 17:46:57.565597 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : T a h h q 26 ; x00 r : P a h d r 27 ; x00 s : P d r f s 28 ; x00 t : D p o p t 29 T o p p t 30 ; x00
I0123 17:48:27.769340 140364354609664 alphageometry.py:565] LM output (score=-1.991182): "t : D o t q t 31 D t q t t 32 ;"
I0123 17:48:27.769631 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:48:27.769689 140364354609664 alphageometry.py:565] LM output (score=-2.223640): "t : D o t t q 31 P o t p q 32 ;"
I0123 17:48:27.769723 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:48:27.769765 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : T a h h q 26 ; x00 r : P a h d r 27 ; x00 s : P d r f s 28 ; x00 t : P b k l t 29 ; x00
I0123 17:49:56.579224 140364354609664 alphageometry.py:565] LM output (score=-1.483781): "t : T h t l p 30 ;"
I0123 17:49:56.579522 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:49:56.579582 140364354609664 alphageometry.py:565] LM output (score=-2.172772): "t : T h t l t 30 ;"
I0123 17:49:56.579637 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:49:56.579688 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : P b k p r 27 ; x00 s : T h p k s 28 ; x00 t : P d j p t 29 ; x00
I0123 17:51:20.869322 140364354609664 alphageometry.py:565] LM output (score=-1.789767): "t : C m p t 30 D m t p t 31 ;"
I0123 17:51:20.869608 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:51:20.869666 140364354609664 alphageometry.py:565] LM output (score=-2.044883): "t : D p t t v 30 D t v t v 31 ;"
I0123 17:51:20.869700 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:51:20.869751 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : P b k p r 27 ; x00 s : T h p k s 28 ; x00 t : P f h k t 29 ; x00
I0123 17:52:42.986307 140364354609664 alphageometry.py:565] LM output (score=-1.947909): "t : T o t q t 30 ;"
I0123 17:52:42.986606 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:52:42.986665 140364354609664 alphageometry.py:565] LM output (score=-2.242063): "t : T o t r t 30 ;"
I0123 17:52:42.986717 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:52:42.986768 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : T h q o r 27 ; x00 s : P b k r s 28 ; x00 t : P a p h t 29 ; x00
I0123 17:54:07.270756 140364354609664 alphageometry.py:565] LM output (score=-2.277915): "t : P a p l t 30 ;"
I0123 17:54:07.271036 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:54:07.271092 140364354609664 alphageometry.py:565] LM output (score=-2.518876): "t : P f h p t 30 ;"
I0123 17:54:07.271154 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:54:07.271223 140364354609664 alphageometry.py:548] Decoding from {S} a : ; b : ; c : ; d : T a c b d 00 T a d b c 01 ; e : C b c e 02 T b c e h 03 ; f : C a c f 04 T a c f h 05 ; g : C a b g 06 T a b g h 07 ; h : ^ a b a h a h a c 08 ^ c a c h c h c b 09 ; i : C b c i 10 T a i b c 11 ; j : C a c j 12 T a c b j 13 ; k : C a b k 14 T a b c k 15 ; l : D e i e l 16 D f i f l 17 ; m : D e j e m 18 D f j f m 19 ; n : D f j f n 20 D g j g n 21 ; o : D f k f o 22 D g k g o 23 ; p : C l m p 24 C n o p 25 ? D h p h e {F1} x00 q : P d j h q 26 ; x00 r : T h q o r 27 ; x00 s : P b k o s 28 ; x00 t : P a p h t 29 ; x00
I0123 17:55:24.188693 140364354609664 alphageometry.py:565] LM output (score=-2.121744): "t : P a p l t 30 ;"
I0123 17:55:24.188985 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:55:24.189042 140364354609664 alphageometry.py:565] LM output (score=-2.322381): "t : P a p k t 30 ;"
I0123 17:55:24.189095 140364354609664 alphageometry.py:566] Translation: "ERROR: point t already exists."

I0123 17:55:24.189214 140364354609664 alphageometry.py:539] Depth 5. There are 0 nodes to expand:
I0123 17:55:24.189252 140364354609664 alphageometry.py:539] Depth 6. There are 0 nodes to expand:
I0123 17:55:24.189283 140364354609664 alphageometry.py:539] Depth 7. There are 0 nodes to expand:
I0123 17:55:24.189312 140364354609664 alphageometry.py:539] Depth 8. There are 0 nodes to expand:
I0123 17:55:24.189340 140364354609664 alphageometry.py:539] Depth 9. There are 0 nodes to expand:
I0123 17:55:24.189370 140364354609664 alphageometry.py:539] Depth 10. There are 0 nodes to expand:
I0123 17:55:24.189400 140364354609664 alphageometry.py:539] Depth 11. There are 0 nodes to expand:
I0123 17:55:24.189428 140364354609664 alphageometry.py:539] Depth 12. There are 0 nodes to expand:
I0123 17:55:24.189482 140364354609664 alphageometry.py:539] Depth 13. There are 0 nodes to expand:
I0123 17:55:24.189512 140364354609664 alphageometry.py:539] Depth 14. There are 0 nodes to expand:
I0123 17:55:24.189540 140364354609664 alphageometry.py:539] Depth 15. There are 0 nodes to expand:

Tests not passed

I followed your instructions and got one test not passed. It says the following:

FAIL: test_lm_score_may_fail_numerically_for_external_meliad (__main__.LmInferenceTest)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/mnt/array50tb/projects/alphageometry/lm_inference_test.py", line 82, in test_lm_score_may_fail_numerically_for_external_meliad
    self.assertEqual(
AssertionError: Lists differ: [-1.1633697, -1.122621] != [-1.1860729455947876, -1.1022869348526]

First differing element 0:
-1.1633697
-1.1860729455947876

- [-1.1633697, -1.122621]
+ [-1.1860729455947876, -1.1022869348526]

----------------------------------------------------------------------
Ran 2 tests in 82.530s

FAILED (failures=1)
****

What could be causing it?

maybe a wrong rule?

the programm said, that in this case angle JIH = angle JKH

No module named 'absl'

Traceback (most recent call last):
File "e:\alphageometry-main\problem_test.py", line 19, in
from absl.testing import absltest
ModuleNotFoundError: No module named 'absl'
PS E:\alphageometry-main> python -u "e:\alphageometry-main\geometry_test.py"
Traceback (most recent call last):
File "e:\alphageometry-main\geometry_test.py", line 19, in
from absl.testing import absltest
ModuleNotFoundError: No module named 'absl'

I try to run some files but this error remains

check_cyclic crashes

This line

alphageometry/numericals.py

Line 705 in 1357929

(a, b, c), *ps = points

Should not contain the parentheses, like

  a, b, c, *ps = points 

Otherwise, it crashes on:

TypeError: cannot unpack non-iterable Point object

Hardware Requirements

Please provide hardware and OS recommendations.

• On which hardware did the author test this project?
• What is the range of setups that this has been tested on? e.g. Colab
• What are some known issues and workarounds with hardware? For example on my Sonoma M1 Max I had to install tensorflow-text with
  pip install tensorflow_text-2.15.0-cp310-cp310-macosx_11_0_arm64.whl

ERROR: No matching distribution found for jaxlib==0.4.6

When I was running the $ pip install --require-hashes -r requirements.txt, it suddenly encountered an error:
ERROR: Could not find a version that satisfies the requirement jaxlib==0.4.6 (from versions: 0.4.13, 0.4.14, 0.4.16, 0.4.17, 0.4.18, 0.4.19, 0.4.20, 0.4.21, 0.4.22, 0.4.23) ERROR: No matching distribution found for jaxlib==0.4.6

I also tried to install it individually but the same error still occured

Or perhaps I can install it from jaxlib-v0.4.6 github?

About the direct angle

The output ∠(QP-EA) is the direct angle, it commonly write as ∠(QP,EA). ∠(l,m) is the angle that line l clockwise rotate a specific angle to line m.

training set?

i can't happen to find example training set/code. do you have plans to release this?

also, how many gpu hours have you spent on training this model?

ModuleNotFoundError: No module named 'transformer' is reported

ModuleNotFoundError: No module named 'transformer' is reported. I reinstalled or upgraded transformers. But it keeps showing up this error:
from transformer import decoder_stack
ModuleNotFoundError: No module named 'transformer'

Download fails with "file/folder name cannot be extracted from: ag_ckpt_vocab"

Under WSL (Windows Subsystem for Linux) I get the error below.

Error

bash download.sh 
Retrieving folder list
Failed to retrieve folder contents:

        file/folder name cannot be extracted from: ag_ckpt_vocab – Google Disk

Solution

Manually navigate to Google Drive location of the weights and other files (link: https://drive.google.com/drive/u/0/folders/1ZLaZ2ajtOcILDWa5ePPLX1bmaf_BNRZV)

Copy that link and set it in download.sh file instead of using the https://bit.ly/alphageometry

gdown --folder https://drive.google.com/drive/u/0/folders/1ZLaZ2ajtOcILDWa5ePPLX1bmaf_BNRZV
export DATA=ag_ckpt_vocab

New project idea homework tonight 🕸️🧑‍💻👩‍💻🗝️💜

Blesss you guys and happy new year 🎊

what symbolic engine is AlphaGeometry using?

Consider hosting weights on huggingface.co :hugs:

Hey there 👋 I'm opening this issue to suggest moving the weights files from the GDrive to the Hugging Face Hub. The weights files would be publicly available, discoverable under the google deepmind organization, versioned and stored along their model card. At the moment, I've uploaded the files to Wauplin/alphageometry for a test but the idea would be to move the repo to a more appropriate organization (either google or deepmind?).

Once hosted on the Hub, you would just need to update the download.sh and run.sh scripts to use the huggingface-cli tool.
Instead of:

gdown --folder https://bit.ly/alphageometry
DATA=ag_ckpt_vocab 

you would have:

huggingface-cli download google-deepmind/alphageometry --local-dir ag_ckpt_vocab
DATA=ag_ckpt_vocab 

huggingface-cli is the CLI tool shipped with the huggingface_hub Python package. I saw that this is already a dependency of the project. I would suggest to update the pinned version (currently 0.17.3) to latest release (0.20.2) which include some bug fixes.

Please let me know what you think! 🤗

Disclaimer: I am myself working at Hugging Face as huggingface_hub's maintainer.

---

Note: not related, but I didn't manage to use gdown correctly (with gdown 4.7.3). I'm getting either

> gdown --folder https://bit.ly/alphageometry 
Retrieving folder contents
Error:

        file/folder name cannot be extracted from:
        ag_ckpt_vocab – Google Drive

To report issues, please visit https://github.com/wkentaro/gdown/issues.

or

gdown --folder https://drive.google.com/drive/u/0/folders/1ZLaZ2ajtOcILDWa5ePPLX1bmaf_BNRZV
Retrieving folder contents
(...)
Failed to retrieve file url:

        Too many users have viewed or downloaded this file recently. Please
        try accessing the file again later. If the file you are trying to
        access is particularly large or is shared with many people, it may
        take up to 24 hours to be able to view or download the file. If you
        still can't access a file after 24 hours, contact your domain
        administrator.

You may still be able to access the file from the browser:

        https://drive.google.com/uc?id=1qXkmmgoJ8oTYJdFV1xw0xGPpQj6SyOYA

but Gdown can't. Please check connections and permissions.

I run this on colab, everything is file until i run this

Requirements.txt - wrong versions

I have python 3.10.9 installed but in the requirements.txt files there are dependencies that require a different version of python. I am getting this error:

ERROR: Could not find a version that satisfies the requirement jaxlib==0.4.6 (from versions: 0.4.13, 0.4.14, 0.4.16, 0.4.17, 0.4.18, 0.4.19, 0.4.20, 0.4.21, 0.4.22, 0.4.23)      
ERROR: No matching distribution found for jaxlib==0.4.6

And if I change the version there are more wrong versions that trigger an error after that.
Should I use a different version of Python or manually configure the versions according to errors?

ModuleNotFoundError: No module named 'transformer'

When running "python alphageometry_test.py", I get the following error:

Traceback (most recent call last):
File "/content/alphageometry_test.py", line 21, in
import alphageometry
File "/content/alphageometry.py", line 28, in
import lm_inference as lm
File "/content/lm_inference.py", line 20, in
import models # pylint: disable=unused-import
File "/content/models.py", line 20, in
import decoder_stack
File "/content/decoder_stack.py", line 21, in
from transformer import decoder_stack
ModuleNotFoundError: No module named 'transformer'

The same happens with "python lm_inference_test.py --meliad_path=$MELIAD_PATH --data_path=$DATA"

Suggestion: Publish original text of jgex_ag_231.txt

I would like to finetune an LLM to automatically parse problem statements. With 300 examples I think it should be possible. If you publish the original statements I could try it and see how far I can get. My end goal is to build a simple web app that ingests natural language statements and outputs the geometry drawing solution. The first step is, of course, the parsing. So I would be very thankful if you published the original statements.

Tranformation from geogebra to the geometric Language

The geometric language is a real mess. Just a suggestion. Can someone code a geogebra code or chatgpt so thst you can tranform normal language or geogebra into the geometry Language.

Thank you

Cannot run on Colab

I ran this Colab file "https://colab.research.google.com/drive/1vyqbBzBDpgNhjGGuGsiVJb336-WDunOv?usp=sharing", and I performed the environment setup and setup process smoothly. However, when it came to the inference step, it encountered this error.

Traceback (most recent call last):
File "/usr/lib/python3.10/runpy.py", line 196, in _run_module_as_main
return _run_code(code, main_globals, None,
File "/usr/lib/python3.10/runpy.py", line 86, in _run_code
exec(code, run_globals)
File "/content/alphageometry/alphageometry.py", line 26, in
import ddar
File "/content/alphageometry/ddar.py", line 20, in
import dd
File "/content/alphageometry/dd.py", line 24, in
import graph as gh
File "/content/alphageometry/graph.py", line 31, in
import numericals as nm
File "/content/alphageometry/numericals.py", line 30, in
matplotlib.use('TkAgg')
File "/usr/local/lib/python3.10/dist-packages/matplotlib/cbook/deprecation.py", line 296, in wrapper
return func(*args, **kwargs)
File "/usr/local/lib/python3.10/dist-packages/matplotlib/cbook/deprecation.py", line 358, in wrapper
return func(*args, **kwargs)
File "/usr/local/lib/python3.10/dist-packages/matplotlib/init.py", line 1281, in use
plt.switch_backend(name)
File "/usr/local/lib/python3.10/dist-packages/matplotlib/pyplot.py", line 234, in switch_backend
raise ImportError(
ImportError: Cannot load backend 'TkAgg' which requires the 'tk' interactive framework, as 'headless' is currently running

Definitions clarification

In the defs.txt there are terms not defined neither on the article nor the references I searched. Could you please explain the syntaxis of this:

on_circle x o a
x : x o a
o a = diff o a
x : cong o x o a
circle o o a

What is diff there, and what is the : doing? And the final circle, that is not the syntax of circle(O, A, B, C) that means center O and passes through A, B, C. How many interpretations are for the circle predicate?

Thanks in advance.

CMO2023 Product of segements

According to study the grammer of the input of alphageometry, I can tranlated the power of point theorem as follows

a b c = triangle a b c; d = circle d a b c; e = on_circle e d a; f = intersection_ll f a e c b ? eqratio f e f b f c f a

And the output of alphageometry is

==========================
 * From theorem premises:
A B C D E F : Points
DA = DB [00]
DB = DC [01]
DE = DA [02]
E,A,F are collinear [03]
C,B,F are collinear [04]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DA = DB [00] & DE = DA [02] & DB = DC [01] ⇒  C,E,B,A are concyclic [05]
002. C,E,B,A are concyclic [05] ⇒  ∠CBE = ∠CAE [06]
003. E,A,F are collinear [03] & C,B,F are collinear [04] & ∠CAE = ∠CBE [06] ⇒  ∠CAF = ∠FBE [07]
004. C,B,F are collinear [04] & E,A,F are collinear [03] ⇒  ∠CFA = ∠BFE [08]
005. ∠CAF = ∠FBE [07] & ∠CFA = ∠BFE [08] (Similar Triangles)⇒  CF:AF = EF:BF
==========================

This is very easy.

But when I try to formalize a more complicated problem of CMO 2023, i realized it seems very hard to fromalized the conculusion involved three segements products. Can anyone else have a good idea? ( I translated the questions as follows)

In an acute-angled triangle ABC, B, C, K are collinear but K is outside the segments of BC, KP // AB, KQ // KC。 If BK=BP, CK=CQ, and cirmucircle of triangle intersect AK in T:
Please Proof:

1. $\angle BTC + \angle APB = \angle CQA$;
2. $AP\cdot BT \cdot CQ = AQ \cdot CT \cdot BP$

Nature link not working

As the title says, the nature url links to a nonexistent page.

what is the following error

i keep getting key error: a

Possibly wrong rule in the solver ruleset

The sample solution generated for the orthocentre problem by alhpageometry looks like this:

* From theorem premises:
A B C D : Points
BD ⟂ AC [00]
CD ⟂ AB [01]

 * Auxiliary Constructions:
E : Points
C,A,E are collinear [02]
B,D,E are collinear [03]

 * Proof steps:
001. E,C,A are collinear [02] & B,E,D are collinear [03] & BD ⟂ AC [00] ⇒  ∠CED = ∠BEA [04]
002. E,C,A are collinear [02] & B,E,D are collinear [03] & BD ⟂ AC [00] ⇒  ∠DEA = ∠CEB [05]
003. BD ⟂ AC [00] & CD ⟂ AB [01] ⇒  ∠BAC = ∠CDB [06]
004. B,D,E are collinear [03] & E,A,C are collinear [02] & ∠CDB = ∠BAC [06] ⇒  ∠CDE = ∠BAE [07]
005. ∠CED = ∠BEA [04] & ∠CDE = ∠BAE [07] (Similar Triangles)⇒  CE:BE = DE:EA [08]
006. CE:BE = DE:EA [08] & ∠DEA = ∠CEB [05] (Similar Triangles)⇒  ∠DAE = ∠CBE [09]
007. CE:BE = DE:EA [08] & ∠DEA = ∠CEB [05] (Similar Triangles)⇒  ∠EDA = ∠ECB [10]
008. ∠DAE = ∠CBE [09] & C,A,E are collinear [02] & B,D,E are collinear [03] & ∠EDA = ∠ECB [10] ⇒  AD ⟂ BC
==========================

I0118 18:44:43.041623 139894856428416 alphageometry.py:575] Solved.

As far as I understand, step 003 is wrong: the statement is correct for the angles between two straight lines, not for angles BAC and CDB. Does that mean the network has generated the wrong text? Or it just used a rule from the set, and the rule is wrong?

about the max_decode_len in model.py

Recently, I want to test alphageometry could solve a probelm in USA TSTST 2016, it can be translated into input as:

a b c = triangle a b c; d = incenter d a b c; e = foot e d b c; f = foot f d a c; g = foot g d a b; h = foot h e f g; i = circle i a d b; j = circle j a d c; k = on_circle k i a, on_circle k d e; l = intersection_cc l d i k; m = on_circle m j a, on_circle m d e; n = intersection_cc n d j m; o = circle o b m n; p = circle p c k l; q = on_circle q o b, on_circle q p c; r = intersection_cc r o p q; s = intersection_ll s q r h e; x = midpoint x f g; y = midpoint y g e; z = midpoint e f; w = on_line w a e, on_line w b f ? cong s h s e

This was included A-W points, however, alphageometry can't generate new auxilary point to this problem, I guess, it may be due to max_decode limit.
Thus I wonder, whethter the max_decode_len influence this, but it seems doesn't work.

['u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 'u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 'u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 'u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 'u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 'u : P d v e u 40 T g u u u 41 ? C d h q {B*} * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ;',
 't : P d t l p 40 ;',
 't : P n t p t 40 ;']

and the this corresponds as follows:

ERROR: point u already exists.
ERROR: point u already exists.
ERROR: point u already exists.
ERROR: point u already exists.
ERROR: point u already exists.
ERROR: point u already exists.
ERROR: point t already exists.
ERROR: point t already exists.

about checkpoint_10999999

How to train this model? Is it the best super parameters？ more alignment，such as SFT
or RLHF, maybe more solved？

sketch_cc_tangent0 is missing

I was trying to solve a problem that involved defining the tangent of two circles and found myself needing cc_tangent0 which just outputs two points of tangency. However, cc_tangent0 has no numerical counterpart. Only cc_tangent which returns four points.

ModuleNotFoundError: No module named 'tensorflow.python'

I had tried to run the command in Ubuntu with python3.10:

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

then I got the below issue:

/home/vikisu/alphageometry/lib/python3.10/site-packages/flax/struct.py:132: FutureWarning: jax.tree_util.register_keypaths is deprecated, and will be removed in a future release. Please use register_pytree_with_keys() instead.
jax.tree_util.register_keypaths(data_clz, keypaths)
/home/vikisu/alphageometry/lib/python3.10/site-packages/flax/struct.py:132: FutureWarning: jax.tree_util.register_keypaths is deprecated, and will be removed in a future release. Please use register_pytree_with_keys() instead.
jax.tree_util.register_keypaths(data_clz, keypaths)
/home/vikisu/alphageometry/lib/python3.10/site-packages/flax/struct.py:132: FutureWarning: jax.tree_util.register_keypaths is deprecated, and will be removed in a future release. Please use register_pytree_with_keys() instead.
jax.tree_util.register_keypaths(data_clz, keypaths)
Traceback (most recent call last):
File "/usr/lib/python3.10/runpy.py", line 196, in _run_module_as_main
return _run_code(code, main_globals, None,
File "/usr/lib/python3.10/runpy.py", line 86, in _run_code
exec(code, run_globals)
File "/home/vikisu/alphageometry/alphageometry.py", line 28, in
import lm_inference as lm
File "/home/vikisu/alphageometry/lm_inference.py", line 20, in
import models # pylint: disable=unused-import
File "/home/vikisu/alphageometry/models.py", line 24, in
from transformer import models
File "/home/vikisu/alphageometry/meliad_lib/meliad/transformer/models.py", line 25, in
import metrics_summary
File "/home/vikisu/alphageometry/meliad_lib/meliad/metrics_summary.py", line 20, in
from clu import metric_writers
File "/home/vikisu/alphageometry/lib/python3.10/site-packages/clu/metric_writers/init.py", line 52, in
from clu.metric_writers.summary_writer import SummaryWriter
File "/home/vikisu/alphageometry/lib/python3.10/site-packages/clu/metric_writers/summary_writer.py", line 27, in
import tensorflow as tf
File "/home/vikisu/alphageometry/lib/python3.10/site-packages/tensorflow/init.py", line 38, in
from tensorflow.python.tools import module_util as _module_util
ModuleNotFoundError: No module named 'tensorflow.python'

.#

.

Does the model give wrong results?

check cyclic error

I tried with translated_imo_2008_p1a in imo_ag_30.txt and get error:

numericals.py", line 705, in check_cyclic
(a, b, c), *ps = points
TypeError: cannot unpack non-iterable Point object

How to fix it?

etils error

Collecting etils[epath]
ERROR: In --require-hashes mode, all requirements must have their versions pinned with ==. These do not:
etils[epath] from https://files.pythonhosted.org/packages/cf/10/55adb8074b0211f8cfad76e73da86d4306e45567a5e6a905b4444fd7a751/etils-1.6.0-py3-none-any.whl#sha256=3da192b057929f2511f9ef713cee7d9c498e741740f8b2a9c0f6392d787201d4 (from array-record==0.4.1->-r requirements.txt (line 28))

ModuleNotFoundError: No module named 'absl'

I run mode ddar:
python -m alphageometry
--alsologtostderr
--problems_file=$(pwd)/imo_ag_30.txt
--problem_name=translated_imo_2000_p1
--mode=ddar
"${DDAR_ARGS[@]}"

and get error:

File "/home/technical/alphageometry/alphageometry.py", line 23, in
from absl import app
ModuleNotFoundError: No module named 'absl'

How to fix it?

prove of the simple problem of Fig. 1

I have tried the simple problem of Fig. 1, and it can be proved.

Is there anything wrong?

test
a b c = eq2_triangle a b c ? eqangle b c b a c a c b

where eq2_triangle is defined as:

eq2_triangle a b c
c : a b
 =
a : ; b : ; c : cong a b a c
eq2_triangle

def sketch_eq2_triangle(args: tuple[gm.Point, ...]) -> tuple[Point, ...]:
  b = Point(0.0, 0.0)
  c = Point(np.random.uniform(0.5, 1.0), 0)
  a = Point((b.x + c.x) / 2, np.random.uniform(0.5, 10.0))
  return a, b, c

An easy way to generate the correponding figure according to the problem sentence

According to the author's update ref. 82364a7, I found an easy to way to generate the figure according to the sentence:

import unittest
from absl.testing import absltest
import dd
import graph as gh
import problem as pr

txt = 'f g h i j = pentagon f g h i j; a = intersection_ll a f j g h; b = intersection_ll b f g h i; c = intersection_ll c g h i j; d = intersection_ll d h i f j; e = intersection_ll e f g i j; o1 = circle o1 a f g; o2 = circle o2 b g h; o3 = circle o3 c h i; o4 = circle o4 d j i; o5 = circle o5 e j f; k = intersection_cc k o5 o1 f; l = intersection_cc l o1 o2 g; m = intersection_cc m o2 o3 h; n = intersection_cc n o3 o4 i; o = intersection_cc o o4 o5 j; ox = circle k l m ? cyclic k l m n'
defs = pr.Definition.from_txt_file('defs.txt', to_dict=True)
p = pr.Problem.from_txt(txt,translate=False)
g, _ = gh.Graph.build_problem(p, defs)
goal_args = g.names2nodes(p.goal.args)
gh.nm.draw(
      g.type2nodes[gh.Point],
      g.type2nodes[gh.Line],
      g.type2nodes[gh.Circle],
      g.type2nodes[gh.Segment])

Published proof of IMO 2015 P3 is incorrect because ∠GMD != ∠GO2D

There's an error in the proof of IMO P3, in Fig1.f 1 and Step 26. of the full proof in supplimentary material2, which it states that ∠GMD = ∠GO2D, which is incorrect. It should be ∠GMD + ∠GO2D = π. I am trying to follow its logic but I cannot parse what it is trying to do at Step 25. It has the right idea of O2 being on the nine point circle though.

Where is the definition of the geometry description language?

Can't run in colab.

• [ ]

collecting etils[epath]

I'm getting this error during install, bash run.sh:

Collecting etils[epath]
ERROR: In --require-hashes mode, all requirements must have their versions pinned with ==. These do not:
    etils[epath] from https://files.pythonhosted.org/packages/cf/10/55adb8074b0211f8cfad76e73da86d4306e45567a5e6a905b4444fd7a751/etils-1.6.0-py3-none-any.whl (from array-record==0.4.1->-r requirements.txt (line 28))

Mw

alphageometry/numericals_test.py

Line 108 in 6661d02

d, _ = line_circle_intersection(line, Circle(b, radius=1))

The input language question

I'm trying to write my own problem for testing. How do I express AB=CD for already defined points A, B, C, D?

Can you also define problems like:

Given a parrallelogramm abcd such that...

run.sh fails (permission error on gdrive folder)

In run.sh, this line fails:

gdown --folder https://bit.ly/alphageometry

Maybe a perms fail on the gdrive folder?

(.venv) (base) ubuntu@cog1:~/pi/alphageometry$ ./run.sh 
+ . .venv/bin/activate
++ deactivate nondestructive
++ '[' -n '' ']'
++ '[' -n '' ']'
++ '[' -n /bin/bash -o -n '' ']'
++ hash -r
++ '[' -n '' ']'
++ unset VIRTUAL_ENV
++ unset VIRTUAL_ENV_PROMPT
++ '[' '!' nondestructive = nondestructive ']'
++ VIRTUAL_ENV=/home/ubuntu/pi/alphageometry/.venv
++ export VIRTUAL_ENV
++ _OLD_VIRTUAL_PATH=/home/ubuntu/.vscode-server/extensions/ms-python.python-2023.22.1/pythonFiles/deactivate/bash:/home/ubuntu/pi/.venv/bin:/home/ubuntu/.vscode-server/bin/0ee08df0cf4527e40edc9aa28f4b5bd38bbff2b2/bin/remote-cli:/home/ubuntu/miniforge3/bin:/home/ubuntu/miniforge3/condabin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
++ PATH=/home/ubuntu/pi/alphageometry/.venv/bin:/home/ubuntu/.vscode-server/extensions/ms-python.python-2023.22.1/pythonFiles/deactivate/bash:/home/ubuntu/pi/.venv/bin:/home/ubuntu/.vscode-server/bin/0ee08df0cf4527e40edc9aa28f4b5bd38bbff2b2/bin/remote-cli:/home/ubuntu/miniforge3/bin:/home/ubuntu/miniforge3/condabin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
++ export PATH
++ '[' -n '' ']'
++ '[' -z '' ']'
++ _OLD_VIRTUAL_PS1=
++ PS1='(.venv) '
++ export PS1
++ VIRTUAL_ENV_PROMPT='(.venv) '
++ export VIRTUAL_ENV_PROMPT
++ '[' -n /bin/bash -o -n '' ']'
++ hash -r
+ gdown --folder https://bit.ly/alphageometry
Retrieving folder list
Processing file 1qXkmmgoJ8oTYJdFV1xw0xGPpQj6SyOYA checkpoint_10999999
Processing file 1t-r3KfU8aDbS1UHpdyM3LH21rwSCIXTz geometry.757.model
Processing file 1mRd6J0UkeWoFUjeVB7BQi5lVNLvPBe31 geometry.757.vocab
Retrieving folder list completed
Building directory structure
Building directory structure completed
Access denied with the following error:

        Cannot retrieve the public link of the file. You may need to change
        the permission to 'Anyone with the link', or have had many accesses. 

You may still be able to access the file from the browser:

         https://drive.google.com/uc?id=1qXkmmgoJ8oTYJdFV1xw0xGPpQj6SyOYA 

Download ended unsuccessfully

Enabling multithreading

In the AlphaGeometry Nature paper, the authors use up to 250 CPU workers to run AlphaGeometry. However, when I run AlphaGeometry, only one thread is used.

How can I use multiple threads? It seems like DD-AR is often a bottleneck, rather than the LLM, when a GPU is used.

No matching distribution found for tensorflow-text==2.13.0

Running run.sh, I got this error:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 2.4/2.4 MB 47.2 MB/s eta 0:00:00 Collecting tensorflow-metadata==1.14.0 (from -r requirements.txt (line 1777)) Downloading tensorflow_metadata-1.14.0-py3-none-any.whl (28 kB) ERROR: Ignored the following versions that require a different python version: 0.28.0 Requires-Python >=3.7, <3.11; 0.5.0 Requires-Python >=2.7,<3; 0.6.0 Requires-Python >=2.7,<=3.7; 0.9.0 Requires-Python >=2.7,<=3.7; 1.21.2 Requires-Python >=3.7,<3.11; 1.21.3 Requires-Python >=3.7,<3.11; 1.21.4 Requires-Python >=3.7,<3.11; 1.21.5 Requires-Python >=3.7,<3.11; 1.21.6 Requires-Python >=3.7,<3.11; 1.6.2 Requires-Python >=3.7,<3.10; 1.6.3 Requires-Python >=3.7,<3.10; 1.7.0 Requires-Python >=3.7,<3.10; 1.7.1 Requires-Python >=3.7,<3.10; 1.7.2 Requires-Python >=3.7,<3.11; 1.7.3 Requires-Python >=3.7,<3.11; 1.8.0 Requires-Python >=3.8,<3.11; 1.8.0rc1 Requires-Python >=3.8,<3.11; 1.8.0rc2 Requires-Python >=3.8,<3.11; 1.8.0rc3 Requires-Python >=3.8,<3.11; 1.8.0rc4 Requires-Python >=3.8,<3.11; 1.8.1 Requires-Python >=3.8,<3.11 ERROR: Could not find a version that satisfies the requirement tensorflow-text==2.13.0 (from versions: 2.12.0rc0, 2.12.0, 2.12.1, 2.13.0rc0, 2.14.0rc0, 2.14.0, 2.15.0rc0, 2.15.0) ERROR: No matching distribution found for tensorflow-text==2.13.0

I have python 3.11:

$ ls /usr/bin | grep python dh_python3-ply idle-python3.11 python3 python3.11 python3.11-config python3-config x86_64-linux-gnu-python3.11-config x86_64-linux-gnu-python3-config

Is tensorflow-text supposed to be installed through pip?

AttributeError: "DecoderOnlyLanguageModel" object has no attribute "num_heads" when I use "alphageometry" mode?

How to fix this problem when I use alphageometry mode?
Traceback (most recent call last):
File "/usr/lib/python3.10/runpy.py", line 196, in _run_module_as_main
return _run_code(code, main_globals, None,
File "/usr/lib/python3.10/runpy.py", line 86, in _run_code
exec(code, run_globals)
File "/content/alphageometry/alphageometry.py", line 645, in
app.run(main)
File "/usr/local/lib/python3.10/dist-packages/absl/app.py", line 308, in run
_run_main(main, args)
File "/usr/local/lib/python3.10/dist-packages/absl/app.py", line 254, in _run_main
sys.exit(main(argv))
File "/content/alphageometry/alphageometry.py", line 631, in main
model = get_lm(_CKPT_PATH.value, _VOCAB_PATH.value)
File "/content/alphageometry/alphageometry.py", line 203, in get_lm
return lm.LanguageModelInference(vocab_path, ckpt_init, mode='beam_search')
File "/content/alphageometry/lm_inference.py", line 66, in init
self.n = imodel.num_heads
File "/usr/local/lib/python3.10/dist-packages/flax/linen/module.py", line 718, in getattr
raise AttributeError(
AttributeError: "DecoderOnlyLanguageModel" object has no attribute "num_heads"

flax error: no working directory specified

I run all the command at 1st time successfully.
When I run below command for 2nd time:

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

Then error occur:

I0124 21:39:21.281035 139724541399040 nn_components.py:261] mlp: residual
I0124 21:39:21.281769 139724541399040 transformer_base.py:450] tbase: ys = Traced<ShapedArray(bfloat16[2,1,1024])>with<DynamicJaxprTrace(level=2/0)>
I0124 21:39:21.281977 139724541399040 decoder_stack.py:344] dstack: Final layernorm.
I0124 21:39:21.286813 139724541399040 decoder_stack.py:365] dstack: logits = Traced<ShapedArray(float32[2,1,1024])>with<DynamicJaxprTrace(level=2/0)>
I0124 21:39:45.593152 139724541399040 optimizer_config.py:74] Using Flax Adafactor Optimizer. lr=1.000000, b1=0.900000
/home/vikisu/Desktop/alphageometry/lib/python3.10/site-packages/flax/optim/base.py:49: DeprecationWarning: Use optax instead of flax.optim. Refer to the update guide https://flax.readthedocs.io/en/latest/howtos/optax_update_guide.html for detailed instructions.
warnings.warn(
I0124 21:39:47.651232 139724541399040 training_loop.py:409] No working directory specified.
I0124 21:39:47.652373 139724541399040 training_loop.py:431] Loading pre-trained model from ag_ckpt_vocab:
I0124 21:39:47.762608 139724541399040 checkpoints.py:429] Restoring checkpoint from ag_ckpt_vocab/checkpoint_10999999
Killed

Please help about this

Inconsistencies in Auxiliary Construction Predictions

Dear Authors,

I hope this message finds you well. I am reaching out to discuss a rather intriguing aspect of the AlphaGeometry solver that I've encountered while exploring the remarkable capabilities of your software, as described in the repository.

Whilst the solver has demonstrated profound proficiency in deducing geometric proofs, I've observed some inconsistencies in the predictions of auxiliary constructions during the problem-solving process. Specifically, there appears to be a variation in the quality and relevance of the auxiliary points or lines proposed by the language model, which occasionally leads to suboptimal proof paths or, in some cases, an inability to reach a conclusion within the stipulated time frame.

I am particularly interested in understanding the underlying factors that contribute to these disparities. Is it a consequence of the inherent stochastic nature of the language model, or could it be attributed to the training data and the model's exposure to a diverse range of geometric configurations during its learning phase?

Moreover, I am curious about the potential strategies one might employ to enhance the consistency and reliability of the auxiliary construction predictions. Would augmenting the training dataset with a broader spectrum of problems or incorporating additional fine-tuning stages be a viable approach to address this issue?

Your insights into these questions would be incredibly valuable, not only for the advancement of automated theorem proving but also for the broader AI and machine learning community's understanding of model predictability and performance optimisation.

Thank you for your time and the impressive work you've shared with the community.

Best regards,
yihong1120

JGEX ciation seems wrong

In the nature paper, JGEX citation is
Ye, Z., Chou, S. C. & Gao, X. S. in Proc. Automated Deduction in Geometry: 7th International
Workshop, ADG 2008 (eds Sturm, T. & Zengler, C.) 189–195 (Springer, 2011).
But I searched, it seems the corresponding article is this;
https://dl.acm.org/doi/10.5555/2008257.2008268
So the citation should like
Zheng Ye, Shang-Ching Chou, and Xiao-Shan Gao. 2008. An introduction to java geometry expert. In Proceedings of the 7th international conference on Automated deduction in geometry (ADG'08). Springer-Verlag, Berlin, Heidelberg, 189–195.

but this is can be ignored, never mind