LeanReasoner

Installation

To set up your environment, please follow the instructions provided below. Our setup relies on external repositories, LeanDojo and ReProver, for complete installation. There isn't a specific requirements.txt file for this project as all necessary installations are covered through these resources.

Step 1: Install LeanDojo

First, visit the LeanDojo repository and follow the installation instructions provided there. For reference, the commit used for this setup was be04dd3fca520addb497e91339f725e55b3bee74.

Step 2: Clone and Set Up ReProver

Next, clone the ReProver repository to your local machine. Follow the installation instructions detailed within to properly set up ReProver for training LeanReasoner. The specific commit used for ReProver in this setup was ada8cc1f7e8c356ea1af9d3c27e44a6d7494817b.

Data

Two files with detailed to help understand the process of formalizing natural language question to theorems: examples_with_detailed annotation

The annotated data for ProofWriter: data_for_share/ProofWriter

The annotated data for FOLIO - concise version: data_for_share/FOLIO/concise

The annotated data for FOLIO - intuitive version: data_for_share/FOLIO/intuitive

Running experiments

Step 1: Get formalization result with GPT-4

We use GPT-4 with the add_comment_and_use_COT configuration, which adds comments in the formalization process and tries to provide step-by-step proof even when we can't prove the theorem. The prompt input are stored in prompts.py while the prompt output are store in output_prompt and output_prompt_FOLIO

For ProofWriter, run: python gpt4prompt.py

For FOLIO, run: python gpt4prompt_FOLIO.py

Step 2: Preprocess Lean code with LeanDoJo

The training data for FOLIO can be found in reprover_train_FOLIO To generate training data, in the LeanDoJo folder, run

python test_dataset_construction.py output_dir_name

Setup ReProver training, run cp -r output_dir_name ReProver/data/

and change the config accordingly

Step 3: Train premise selection and tactic generation

(For the following commands, use the 'retrieval' folder located within the Reprover repository)

Premise Selection Training:

python retrieval/main.py fit --config retrieval/confs/cli_random_text_math_FOLIO_concise.yaml

Retrieve premise for all proof states:

python retrieval/main.py predict --config retrieval/confs/cli_random_text_math_FOLIO_concise.yaml --ckpt_path logs/premise_math_FOLIO_concise/lightning_logs/version_0/checkpoints/epoch=176-step=8319.ckpt

Evaluate for retrieved premises:

python retrieval/evaluate.py --data-path data/train_FOLIO_concise/random --preds-file logs/premise_math_FOLIO_concise/lightning_logs/version_1/predictions.pickle

Tactic generation:

python generator/main.py fit --config generator/confs/cli_random_math_text_FOLIO_concise.yaml --model.ret_ckpt_path logs/premise_math_FOLIO_concise/lightning_logs/version_0/checkpoints/epoch=176-step=8319.ckpt --data.preds_path logs/premise_math_FOLIO_concise/lightning_logs/version_1/predictions.pickle

Step 4: Do ProofSearch

ReIndex the corpus:

python retrieval/index.py --ckpt_path logs/tacgen_math_FOLIO_concise/lightning_logs/version_0/checkpoints/epoch=59-step=2160.ckpt --corpus-path data/test_FOLIO_all_true/corpus.jsonl --output-path logs/tacgen_math_FOLIO_concise/lightning_logs/version_0/indexed_corpus

Evaluate:

python prover/evaluate.py --data-path data/test_FOLIO_all_true/random --ckpt_path logs/tacgen_math_FOLIO_concise/lightning_logs/version_0/checkpoints/epoch=59-step=2160.ckpt --indexed-corpus-path logs/tacgen_math_FOLIO_concise/lightning_logs/version_0/indexed_corpus --split train --num-cpus 10

Citation

@inproceedings{jiang2024leanreasoner,
 title={LeanReasoner: Boosting Complex Logical Reasoning with Lean}, 
 author = {Jiang, Dongwei and Fonseca, Marcio and Cohen, Shay B.},
 booktitle = {Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies},
 year = {2024}
}

ZIYU-DEEP/theorem-proving-reasoning