alphageometry
alphageometry copied to clipboard
google-deepmind
Am I formulating this problem correctly ?
Hi everyone, I'm having this geometry problem: Let ABCD be a square, let O be the intersection between AC and BD, let E be a point on the segment CD, let M be the intersection between AE and BC, let I be the intersection between OM and BE. Prove that the angle OIB is 45 degree. Here is my problem formulation which I added to examples.txt
a b c d = isquare a b c d; o = on_line a c, on_line b d; e = on_line c d; m = on_line a e, on_line b c; i = on_line o m, on_line b e ? s_angle o i b 45
I then run the code normally as explained in the README. However it keeps running and does not finish. So I think maybe the way I formulate the problem is wrong. Can anyone help me check ? Thank you very much.
Hi,
Are you running it in alphageometry mode? I was able to brute force a solution to your problem using only DDAR. It seems that the problem is with the goal and not the formulation of the diagram.
When you build a problem alphageometry assigns numerical values to the constructed points and repeats until it finds a configuration that can satisfy the goal predicate(numericals.check). It seems that the s_angle predicate doesn't have a corresponding check_s_angle function to do this. There is also the predicate aconst that works similarly to s_angle (aconst o i i b 1pi/4).
check_aconst IS implemented but it expects 6 arguments instead of 5 in the form "aconst o i i b 1 4", where 1 4 represents 1pi/4, which I assume is used internally with some conversions.
To solve your problem I disabled the numerical check in graph.build_problem
# args = list(map(lambda x: g.get(x, lambda: int(x)), pr.goal.args))
# check = nm.check(pr.goal.name, args)
# force true to debug
check = True
And reformulated the problem as
'a b c d = isquare a b c d; o = on_line a c, on_line b d; e = on_line c d; m = on_line a e, on_line b c; i = on_line o m, on_line b e ? aconst o i i b 1pi/4'
Running this in DDAR mode a few times(since we have numerical check disabled). I got the following solution and diagram.
==========================
* From theorem premises:
A B C D O E M I : Points
AB ⟂ BC [00]
AB = BC [01]
AD ∥ BC [02]
AB ∥ CD [03]
D,B,O are collinear [04]
O,C,A are collinear [05]
D,C,E are collinear [06]
B,M,C are collinear [07]
M,E,A are collinear [08]
I,M,O are collinear [09]
I,B,E are collinear [10]
* Auxiliary Constructions:
: Points
* Proof steps:
001. AB = BC [01] ⇒ ∠BAC = ∠ACB [11]
002. AB ⟂ BC [00] & ∠BAC = ∠ACB [11] (Angle chase)⇒ ∠ACB = 1_PI/4 [12]
003. BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠ADC = ∠CBA [13]
004. BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DCB = ∠CDA [14]
005. CD ∥ AB [03] ⇒ ∠ACD = ∠CAB [15]
006. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ BC:BA = DA:DC [16]
007. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ AD = CB [17]
008. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ CD = AB [18]
009. BC:BA = DA:DC [16] & AB = BC [01] ⇒ DA = DC [19]
010. AB = BC [01] & AD = CB [17] ⇒ AD = AB [20]
011. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DAB = ∠CDA [21]
012. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠ADC = ∠ABC [22]
013. DA = DC [19] & AD = AB [20] & ∠DAB = ∠CDA [21] (SAS)⇒ ∠DBA = ∠CAD [23]
014. DA = DC [19] & AD = AB [20] & ∠DAB = ∠CDA [21] (SAS)⇒ ∠ADC = ∠(BD-AC) [24]
015. AB ∥ CD [03] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ DO:BO = OC:OA [25]
016. AB ∥ CD [03] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ DC:BA = OD:OB [26]
017. D,C,E are collinear [06] & AB ∥ CD [03] ⇒ CE ∥ BA [27]
018. CE ∥ BA [27] & B,M,C are collinear [07] & M,E,A are collinear [08] ⇒ MC:BC = ME:EA [28]
019. CE ∥ BA [27] & B,M,C are collinear [07] & M,E,A are collinear [08] ⇒ MC:MB = CE:BA [29]
020. MC:MB = CE:BA [29] & AB = BC [01] ⇒ MC:BM = CE:BC [30]
021. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ BO:DO = OC:OA [31]
022. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ BO:DO = BC:DA [32]
023. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ OC:OA = BC:DA [33]
024. B,M,C are collinear [07] & AD ∥ BC [02] ⇒ MC ∥ AD [34]
025. MC ∥ AD [34] & M,E,A are collinear [08] & D,C,E are collinear [06] ⇒ ME:EA = CE:DE [35]
026. D,B,O are collinear [04] & O,C,A are collinear [05] & ∠(BD-AC) = ∠ADC [24] ⇒ ∠DOA = ∠ADC [36]
027. O,C,A are collinear [05] & ∠BCA = ∠CAB [11] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DAO = ∠ACD [37]
028. ∠DOA = ∠ADC [36] & ∠DAO = ∠ACD [37] (Similar Triangles)⇒ DO:DA = AD:AC [38]
029. ∠ADC = ∠ABC [22] ⇒ D,B,C,A are concyclic [39]
030. D,B,C,A are concyclic [39] & ∠DCB = ∠CDA [14] ⇒ DB = CA [40]
031. DO:DA = AD:AC [38] & DA = DC [19] & DB = CA [40] ⇒ DO:DC = DA:DB [41]
032. AB = BC [01] & DO:BO = OC:OA [25] & MC:BC = ME:EA [28] & MC:BM = CE:BC [30] & BO:DO = OC:OA [31] & BO:DO = BC:DA [32] & ME:EA = CE:DE [35] & DO:DC = DA:DB [41] (Ratio chase)⇒ BO:BM = DE:CA [42]
033. BO:BM = DE:CA [42] & DC:BA = OD:OB [26] & CD = AB [18] & DB = CA [40] ⇒ DE:DB = BO:BM [43]
034. OC:OA = BC:DA [33] & BA = DA [20] ⇒ OC:OA = BC:BA [44]
035. OC:OA = BC:BA [44] & O,C,A are collinear [05] ⇒ ∠CBO = ∠OBA [45]
036. D,C,E are collinear [06] & D,B,O are collinear [04] & B,M,C are collinear [07] & ∠CBO = ∠OBA [45] & AB ∥ CD [03] ⇒ ∠EDB = ∠OBM [46]
037. DE:DB = BO:BM [43] & ∠EDB = ∠OBM [46] (Similar Triangles)⇒ ∠DEB = ∠BOM [47]
038. I,M,O are collinear [09] & I,B,E are collinear [10] & ∠ACB = 1_PI/4 [12] & ∠DBA = ∠CAD [23] & AD ∥ BC [02] & ∠DEB = ∠BOM [47] & D,C,E are collinear [06] & D,B,O are collinear [04] & AB ∥ CD [03] ⇒ ∠OIB = 1_PI/4
==========================
I think both s_angle and aconst are not meant to be used as goals. You might be able to folmulate a better goal or find a way to make the numerical check work for aconst. Would love to hear if you make any progress.
Hi,
Are you running it in alphageometry mode? I was able to brute force a solution to your problem using only DDAR. It seems that the problem is with the goal and not the formulation of the diagram.
When you build a problem alphageometry assigns numerical values to the constructed points and repeats until it finds a configuration that can satisfy the goal predicate(numericals.check). It seems that the s_angle predicate doesn't have a corresponding check_s_angle function to do this. There is also the predicate aconst that works similarly to s_angle (aconst o i i b 1pi/4).
check_aconst IS implemented but it expects 6 arguments instead of 5 in the form "aconst o i i b 1 4", where 1 4 represents 1pi/4, which I assume is used internally with some conversions.
To solve your problem I disabled the numerical check in graph.build_problem
# args = list(map(lambda x: g.get(x, lambda: int(x)), pr.goal.args)) # check = nm.check(pr.goal.name, args) # force true to debug check = TrueAnd reformulated the problem as
'a b c d = isquare a b c d; o = on_line a c, on_line b d; e = on_line c d; m = on_line a e, on_line b c; i = on_line o m, on_line b e ? aconst o i i b 1pi/4'Running this in DDAR mode a few times(since we have numerical check disabled). I got the following solution and diagram.
========================== * From theorem premises: A B C D O E M I : Points AB ⟂ BC [00] AB = BC [01] AD ∥ BC [02] AB ∥ CD [03] D,B,O are collinear [04] O,C,A are collinear [05] D,C,E are collinear [06] B,M,C are collinear [07] M,E,A are collinear [08] I,M,O are collinear [09] I,B,E are collinear [10] * Auxiliary Constructions: : Points * Proof steps: 001. AB = BC [01] ⇒ ∠BAC = ∠ACB [11] 002. AB ⟂ BC [00] & ∠BAC = ∠ACB [11] (Angle chase)⇒ ∠ACB = 1_PI/4 [12] 003. BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠ADC = ∠CBA [13] 004. BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DCB = ∠CDA [14] 005. CD ∥ AB [03] ⇒ ∠ACD = ∠CAB [15] 006. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ BC:BA = DA:DC [16] 007. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ AD = CB [17] 008. ∠ADC = ∠CBA [13] & ∠ACD = ∠CAB [15] (Similar Triangles)⇒ CD = AB [18] 009. BC:BA = DA:DC [16] & AB = BC [01] ⇒ DA = DC [19] 010. AB = BC [01] & AD = CB [17] ⇒ AD = AB [20] 011. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DAB = ∠CDA [21] 012. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠ADC = ∠ABC [22] 013. DA = DC [19] & AD = AB [20] & ∠DAB = ∠CDA [21] (SAS)⇒ ∠DBA = ∠CAD [23] 014. DA = DC [19] & AD = AB [20] & ∠DAB = ∠CDA [21] (SAS)⇒ ∠ADC = ∠(BD-AC) [24] 015. AB ∥ CD [03] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ DO:BO = OC:OA [25] 016. AB ∥ CD [03] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ DC:BA = OD:OB [26] 017. D,C,E are collinear [06] & AB ∥ CD [03] ⇒ CE ∥ BA [27] 018. CE ∥ BA [27] & B,M,C are collinear [07] & M,E,A are collinear [08] ⇒ MC:BC = ME:EA [28] 019. CE ∥ BA [27] & B,M,C are collinear [07] & M,E,A are collinear [08] ⇒ MC:MB = CE:BA [29] 020. MC:MB = CE:BA [29] & AB = BC [01] ⇒ MC:BM = CE:BC [30] 021. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ BO:DO = OC:OA [31] 022. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ BO:DO = BC:DA [32] 023. AD ∥ BC [02] & D,B,O are collinear [04] & O,C,A are collinear [05] ⇒ OC:OA = BC:DA [33] 024. B,M,C are collinear [07] & AD ∥ BC [02] ⇒ MC ∥ AD [34] 025. MC ∥ AD [34] & M,E,A are collinear [08] & D,C,E are collinear [06] ⇒ ME:EA = CE:DE [35] 026. D,B,O are collinear [04] & O,C,A are collinear [05] & ∠(BD-AC) = ∠ADC [24] ⇒ ∠DOA = ∠ADC [36] 027. O,C,A are collinear [05] & ∠BCA = ∠CAB [11] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠DAO = ∠ACD [37] 028. ∠DOA = ∠ADC [36] & ∠DAO = ∠ACD [37] (Similar Triangles)⇒ DO:DA = AD:AC [38] 029. ∠ADC = ∠ABC [22] ⇒ D,B,C,A are concyclic [39] 030. D,B,C,A are concyclic [39] & ∠DCB = ∠CDA [14] ⇒ DB = CA [40] 031. DO:DA = AD:AC [38] & DA = DC [19] & DB = CA [40] ⇒ DO:DC = DA:DB [41] 032. AB = BC [01] & DO:BO = OC:OA [25] & MC:BC = ME:EA [28] & MC:BM = CE:BC [30] & BO:DO = OC:OA [31] & BO:DO = BC:DA [32] & ME:EA = CE:DE [35] & DO:DC = DA:DB [41] (Ratio chase)⇒ BO:BM = DE:CA [42] 033. BO:BM = DE:CA [42] & DC:BA = OD:OB [26] & CD = AB [18] & DB = CA [40] ⇒ DE:DB = BO:BM [43] 034. OC:OA = BC:DA [33] & BA = DA [20] ⇒ OC:OA = BC:BA [44] 035. OC:OA = BC:BA [44] & O,C,A are collinear [05] ⇒ ∠CBO = ∠OBA [45] 036. D,C,E are collinear [06] & D,B,O are collinear [04] & B,M,C are collinear [07] & ∠CBO = ∠OBA [45] & AB ∥ CD [03] ⇒ ∠EDB = ∠OBM [46] 037. DE:DB = BO:BM [43] & ∠EDB = ∠OBM [46] (Similar Triangles)⇒ ∠DEB = ∠BOM [47] 038. I,M,O are collinear [09] & I,B,E are collinear [10] & ∠ACB = 1_PI/4 [12] & ∠DBA = ∠CAD [23] & AD ∥ BC [02] & ∠DEB = ∠BOM [47] & D,C,E are collinear [06] & D,B,O are collinear [04] & AB ∥ CD [03] ⇒ ∠OIB = 1_PI/4 ==========================
I think both s_angle and aconst are not meant to be used as goals. You might be able to folmulate a better goal or find a way to make the numerical check work for aconst. Would love to hear if you make any progress.
Hi, yes I tried using Alphageometry. I have modified according to your post and it works using DDAR but when I run Alphageometry mode it fails. I am just utterly confused about the input format since there is no explanation. Do you know if it's possible to run in Alphageometry mode ?
Hi,
I was able to make it work in alphageometry mode in two different ways.
First I used a different formulation of the goal. eqangle b a b o b i i o Which is just a roundabout way of representing ∠oib = 45.
I was also able to use the aconst goal by updating the function that translates the pointnames to be in alphabetical order.
problem.Construction.translate
def translate(self, mapping: dict[str, str]) -> Construction:
args = [a if (isint(a) or 'pi/' in a) else mapping[a] for a in self.args]
return Construction(self.name, args)
which normally expects only integers or point names as args. The proof was still only using DDAR since no additional constructions are needed for this problem and i wasnt able to generate a different proof by lowering the max_level of the DDAR.
I agree that the input format is confusing and it seems that they only tested with a limited set of goal types. You could try playing around with JGEX, as the input language is based on it's construction definitions. Let me know if you end up finding a better solution.
Is there a way to just generate the diagram without having it solve anything?
I was trying a round about way to do it, but it doesn't seem to work:
a b c d = isquare a b c d ? perp b c d a
Ah shoot that must be the error. I have no idea how I mixed that up. Will attempt running it now.
