google-deepmind / alphageometry

Solving Olympiad Geometry without Human Demonstrations This repository contains the code necessary to reproduce DDAR and AlphaGeometry, the two geometry theorem provers introduced in the Nature 2024 paper: • "Solving Olympiad Geometry without Human Demonstrations". * **Update (Jan 2026):** AlphaGeometry2 is published, its code for DDAR is released at alphageometry2. Dependencies For the instructions presented below, we use Python 3.10.9, and dependencies with their exact version numbers listed in . Our code depends on , which is not a registered package with . See instructions below for how to manually install . Note that one can still run the DDAR solver without the and dependencies. Run the instructions All instructions in this can be run in one go by: Below, we explain these instructions step-by-step. Install dependencies, download weights and vocabulary. Installation is done in a virtual environment: Download weights and vocabulary: Finally, install separately as it is not registered with : Set up common flags Before running the python scripts, let us first prepare some commonly used flags. The symbolic engine needs definitions and deduction rules to operate. These definitions and rules are provided in two text files and . Next, we define the flags relevant to the proof search. To reproduce the simple examples below, we use lightweight values for the proof search parameters: NOTE: The results in our paper can be obtained by setting , , as described in section Methods. To stay under IMO time limits, 4 V100-GPUs and 250 CPU workers are needed as shown in Extended Data - Figure 1. Note that we also strip away other memory/speed optimizations due to internal dependencies and to promote code clarity. Assume the downloaded checkpoint and vocabulary is placed in , and the installed source code is at . We make use of the library to manage model configurations, following conventions. We now define the flags relevant to the language model: TIP: Note that you can still run the DDAR solver without defining and . In such case, simply disable the import of the module inside . Run DDAR The script loads a problem by reading a list of problems from a text file and solves the specific problem in the list according to its name. We pass these two pieces of information through the flags and . We use to indicate that we want to use the DDAR solver. Below we showed this solver solving IMO 2000 P1: Expect the following output 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. TIP: Additionally passing the flag will write the proof to a text file. Running on all problems in will yield solutions to 14 of them, as reported in Table 1 in our paper. Run AlphaGeometry: As a simple example, we load from . This time, we pass to use the AlphaGeometry solver and pass the and flags. Expect the following output: NOTE: Point is automatically renamed to , as the LM is trained on synthetic problems where the points are named alphabetically, and so it expects the same during test time. NOTE: In this implementation of AlphaGeometry, we removed all optimizations that are dependent on internal infrastructure, e.g., parallelized model inference on multi GPUs, parallelized DDAR on multiple CPUs, parallel execution of LM and DDAR, shared pool of CPU workers across different problems, etc. We also removed some memory/speed optimizations and code abstractions in favor of code clarity. As can be seen in the output, initially DDAR failed to solve the problem. The LM proposes two auxiliary constructions (because ): • , i.e., construct as the intersection of circle (center=C, radius=AB) and circle (center=B, radius=AC). This construction has a score of . • , i.e., is the intersection of and . This construction has a higher score ( ) than the previous. Since the second construction has a higher score, DDAR attempted the second construction first and found the solution right away. The proof search therefore terminates and there is no second iteration. Results Before attempting to reproduce the AlphaGeometry numbers in our paper, please make sure to pass all tests in the prepared test suite: NOTE: Issues#14 reports that although the top beam decodes are still the same, the LM is not giving the same score for different users. Then, pass the corresponding values for (column) and (row), and iterate on all problems to obtain the following results: Number of solved problems: | | | | |----------|------------------|-------------------| | | 14 | 198 | | | 25 | 228 | Source code description Files in this repository include python modules/scripts to run the solvers and resource files necessary for the script to execute. We listed below each of them and their description. | File name | Description | |------------------------|------------------------------------------------------------------------------------| | | Implements nodes (Point, Line, Circle, etc) in the proof state graph. | | | Implements the numerical engine in the dynamic geometry environment. | | | Implements utilities for the proof state graph. | | | Implements the proof state graph. | | | Implements the classes that represent the problem premises, conclusion, DAG nodes. | | | Implements DD and its traceback. | | | Implements AR and its traceback. | | | Implements the recursive traceback and dependency difference algorithm. | | | Implements the combination DD+AR. | | | Implements beam decoding of a language model in JAX. | | | Implements the transformer model. | | | Implements the transformer layer. | | | Implements the transformer decoder stack. | | | Implements an interface to a trained LM to perform decoding. | | | Main script that loads problems, calls DD+AR or AlphaGeometry solver, and prints solutions. | | | Pretty formating the solutions…