DOCSEARCHbyAlgolia
Submit Docs

AlphaGeometry Documentation

repository·main·Indexed 26 days ago

https://github.com/google-deepmind/alphageometry

AlphaGeometry is a geometry theorem prover that combines a neural language model with a symbolic deduction engine to solve Olympiad-level geometry problems. It includes the DDAR (Deductive Data-driven Automated Reasoning) solver and a combined AlphaGeometry solver, utilizing a transformer model and a symbolic engine to generate geometric proofs.

Tokens
1.5K
Snippets
5
Records
7
Agent score
39%

What's inside AlphaGeometry

  1. Overview of AlphaGeometry source code and resources

    main

    The AlphaGeometry repository contains Python modules for running geometric solvers and resource files for execution.

    Core Python Modules:

    • alphageometry.py: The main entry point for loading problems, invoking the DD+AR or AlphaGeometry solvers, and printing solutions.
    • dd.py, ar.py, ddar.py: Implementations of Deduction (DD), Autoregressive (AR), and their combination (DD+AR).
    • geometry.py, graph.py, problem.py: Handle the geometric proof state graph, nodes (Point, Line, etc.), and problem premises.
    • models.py, beam_search.py, lm_inference.py: Implement the transformer model, beam decoding in JAX, and the LM interface.
    • numericals.py: Implements the numerical engine.
    • trace_back.py: Implements recursive traceback and dependency difference algorithms.
    • pretty.py: Formats solver output.
    • run.sh: Script to execute the instructions provided in the README.
    • run_tests.sh: Script to execute the test suite.

    Resource Files:

    • defs.txt: Geometric construction action definitions.
    • rules.txt: Deduction rules for DD.
    • geometry_150M_generate.gin: Gin configuration for the LM.
    • imo_ag_30.txt & jgex_ag_231.txt: Problem datasets.

  2. Install AlphaGeometry dependencies and weights

    main

    To set up the environment, create a virtual environment, install the required Python packages from requirements.txt, and download the necessary weights and vocabulary using the provided scripts. Note that meliad must be installed manually as it is not a registered pip package.

    1. Setup Virtual Environment and Install Pip Dependencies:
    virtualenv -p python3 .
source ./bin/activate
pip install --require-hashes -r requirements.txt
    1. Download Weights and Vocabulary:
    bash download.sh
# The downloaded data is stored in the directory: ag_ckpt_vocab
    1. Manually Install meliad:
    MELIAD_PATH=meliad_lib/meliad
mkdir -p $MELIAD_PATH
git clone https://github.com/google-research/meliad $MELIAD_PATH
export PYTHONPATH=$PYTHONPATH:$MELIAD_PATH
    virtualenv -p python3 .
source ./bin/activate
pip install --require-hashes -r requirements.txt

  6. Run the AlphaGeometry solver

    main

    The AlphaGeometry solver combines DDAR with a language model (LM). To run it, use --mode=alphageometry and provide the necessary arguments for the symbolic engine (DDAR_ARGS), the proof search (SEARCH_ARGS), and the language model (LM_ARGS).

    Required Arguments:

    • --mode=alphageometry
    • --problems_file: Path to the problem list.
    • --problem_name: Name of the problem to solve.
    • --defs_file & --rules_file: Symbolic engine definitions and rules.
    • --beam_size & --search_depth: Proof search parameters.
    • --ckpt_path & --vocab_path: LM checkpoint and vocabulary paths.
    • --gin_file & --gin_param: Configuration files and parameters for the LM (using the gin library).
    python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/examples.txt \
--problem_name=orthocenter \
--mode=alphageometry \
--defs_file=$(pwd)/defs.txt \
--rules_file=$(pwd)/rules.txt \
--beam_size=2 \
--search_depth=2 \
--ckpt_path=ag_ckpt_vocab \
--vocab_path=ag_ckpt_vocab/geometry.757.model \
--gin_search_paths=meliad_lib/meliad/transformer/configs,$(pwd) \
--gin_file=base_htrans.gin \
--gin_file=size/medium_150M.gin \
--gin_file=options/positions_t5.gin \
--gin_file=options/lr_cosine_decay.gin \
--gin_file=options/seq_1024_nocache.gin \
--gin_file=geometry_150M_generate.gin \
--gin_param=DecoderOnlyLanguageModelGenerate.output_token_losses=True \
--gin_param=TransformerTaskConfig.batch_size=2 \
--gin_param=TransformerTaskConfig.sequence_length=128 \
--gin_param=Trainer.restore_state_variables=False

  7. Run the DDAR solver

    main

    The DDAR (Deductive Data-driven Automated Reasoning) solver can be run using the alphageometry module. You must specify the --mode=ddar flag, a --problems_file containing the list of problems, and a --problem_name to identify the specific problem to solve. The symbolic engine requires --defs_file and --rules_file to operate.

    To save the proof to a file, use the --out_file flag.

    python -m alphageometry \
--alsologtostderr \
--problems_file=$(pwd)/imo_ag_30.txt \
--problem_name=translated_imo_2000_p1 \
--mode=ddar \
--defs_file=$(pwd)/defs.txt \
--rules_file=$(pwd)/rules.txt