Search code, repositories, users, issues, pull requests...
This repository contains the code necessary to reproduce DDAR and AlphaGeometry, the two geometry theorem provers introduced in the Nature 2024 paper:
The output first includes a list of relevant premises that it uses, and then proof steps that gradually build up the proof. All predicates are numbered to track how they are derived from the premises, and to show that the proof is fully justified.
As a simple example, we load --problem_name=orthocenter from --problem_file=examples.txt. This time, we pass --mode=alphageometry to use the AlphaGeometry solver.
NOTE: Point H is automatically renamed to D, as the LM is trained on synthetic problems where the points are named alphabetically, and so it expects the same during test time.
As can be seen in the output, initially DDAR failed to solve the problem. The LM proposes one auxiliary constructions (Note: Beam search not implemented yet):
DDAR attempted the construction and found the solution right away. The proof search therefore terminates and there is no second iteration.
