google-deepmind / google-deepmind/alphageometry

Possibly wrong rule in the solver ruleset

Open
#17 12 comments 1 reaction 0 assignees View on GitHub
Dominant language
Python
Stars
4.9k
Forks
572
PR merge metrics
No merged PRs in 30d

Description

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?

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.