Goal-Conditionally Learning Formal Mathematics From Intrinsic Motivation

This repository implements a first approach to goal-conditioned self-improvement. We extend the minimo repository with goal-conditioning and show that our approach to goal-conditioning leads to meaningfully faster convergence to solutions to human-input problems. We will soon publish an accompanying blog post on our blog.

The upstream minimo repository is based on the following paper:

@article{poesia2024learning,
  title={Learning Formal Mathematics From Intrinsic Motivation},
  author={Poesia, Gabriel and Broman, David and Haber, Nick and Goodman, Noah D},
  journal={arXiv preprint arXiv:2407.00695},
  year={2024}
}

The rest of the README is from the upstream repository.

---

Compiling the environment

The Peano enviroment is written in Rust and has a Python API via PyO3.

To compile it, you'll first need to install the Rust toolchain. For that, use rustup.

The environment compiles two targets: a peano binary, that can be used stand-alone, as well as a peano Python library, which we'll use to interact with agents. To build, we'll use maturin, a PyO3 build system. Make sure you have Python version at least 3.9. Then, first make a Python virtual environment (conda works too):

[peano] $ python -m venv /path/to/new/virtual/environment
[peano] $ source /path/to/new/virtual/environment/bin/activate

Now, within your environment, install maturin with:

[peano] $ pip install maturin

With maturin you can now compile both the Peano environment and library with it:

[peano] $ cd environment
[environment] $ maturin dev --release  # This will compile the Peano library.
[...]
[environment] $ cargo build --bin peano --release  # This compiles the peano executable.

This should eventually terminate. It will produce a peano executable, which you can test on some example proofs:

[environment]$ target/release/peano theories/natural_number_game.p t_example1
Loading theories/natural_number_game.p
Verifying t_example1... ok
[environment]$

You should also now have a peano Python module that you can import:

[environment]$ python
>>> import peano
>>>

If this works without errors, you're ready to use Peano from Python. Before running any scripts, make sure to install dependencies with:

[environment] $ cd ../learning
[learning] $ pip install -r requirements.txt

Peano Tutorial

For an introduction to the Peano language, you can follow the tutorial.

To check some more comprehensive examples of proofs in Peano, you're encouraged to take a look at some manually written solutions for the Natural Number Game.

Python API Tutorial

This will come soon - I will write a simple example of loading the environment, loading a background theory, setting a theorem statement as a goal, running proof search and reconstructing the proof.

Running the experiments

The entry point for the conjecture-prove loop is in learning/bootstrap.py. It should suffice to pass it one of the domain configuration files, such as:

[learning] $ python bootstrap.py theory=groups

We use hydra for configuration -- the relevant file here is config/bootstrap.yaml. This will run the loop in "sequential" mode, in a single process. There is a distributed mode, backed by a [https://docs.celeryq.dev/en/stable/](Celery queue), that you can use to leverage multiple CPUs/GPUs, either in the same or different machines (it doesn't matter, as long as they can connect to the queue).

The setup is a bit manual:

1. Install Redis. If you cannot install Redis via package managers, you can compile it locally via:

sh install_redis.sh

1. Start the redis server

sh launch/start_redis.sh

2. Run the Celery worker process

sh launch/start_worker.sh

3. Run bootstrap.py in distributed mode

sh launch/run_bootstrap_distributed.sh

Feel free to open an issue if you're interested in setting this up, and I can expand on the documentation. The details might get a little bit cluster-specific, though the general setup is just that you need (a) a Redis server, (b) a number of worker processes that connect to it, and (c) a teacher process that runs the bootstrapping loop, also connecting to the same Redis server.