search

google-deepmind / alphageometry

Apache License 2.0
4.19k stars 470 forks source link

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

Open robotzheng opened 10 months ago

robotzheng commented 10 months ago

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:

robotzheng commented 10 months ago

I0124 14:01:54.993820 140581835039232 alphageometry.py:565] LM output (score=-0.872653): "r : C d l r 28 D d r l r 29 ;" I0124 14:01:54.994065 140581835039232 alphageometry.py:566] Translation: "ERROR: Traceback (most recent call last): File "/home/notebook/code/personal/80306170/AGI/alphageometry/alphageometry.py", line 438, in try_translate_constrained_to_construct g.copy().add_clause(clause, 0, DEFINITIONS) File "/home/notebook/code/personal/80306170/AGI/alphageometry/graph.py", line 2635, in add_clause raise PointTooCloseError() graph.PointTooCloseError