ayush1801 / naturalprover Goto Github PK

NaturalProver: Grounded Mathematical Proof Generation with Language Models
Sean Welleck*, Jiacheng Liu*, Ximing Lu, Hannaneh Hajishirzi, Yejin Choi

This repo contains:

• The NaturalProofs-Gen datasets.
• GPT-3, GPT-J, GPT-2 code for training and generation.
• Automatic evaluation for proof generation and next-step suggestion.
• GPT-2 trained model.

Please cite our work if you found the resources in this repository useful:

@article{welleck2022naturalprover,
    title={NaturalProver: Grounded Mathematical Proof Generation with Language Models},
    author={Sean Welleck and Jiacheng Liu and Ximing Lu and Hannaneh Hajishirzi and Yejin Choi},
    year={2022},
    eprint={2205.12910},
    archivePrefix={arXiv},
    primaryClass={cs.CL}
}

To download and unpack the data, models, and other files discussed below:

pip install gdown
python download.py --data --model --other --savedir /path/to/savedir

This creates the following file structure:

data/   # NaturalProofs-Gen datasets
model/  # Pretrained NaturalProver models 
other/  # Additional files (e.g. example predictions)

To download and unpack the NaturalProofs-Gen datasets:

pip install gdown
python download.py --data --savedir ./

This creates the following file structure:

data/base  # Original proofwiki, NaturalProofs-Gen (unsplit), redirects (used in evaluation).
data/gpt3  # NaturalProofs-Gen formatted for GPT-3 fine-tuning + ref-reconstruction for retrieved & provided settings.
data/gptj  # NaturalProofs-Gen formatted for GPT-2/J fine-tuning (similar to data/gpt3).

Within each folder, you will see datasets with varied reference-conditioning (norefs, retrefs, gtrefs) and reference reconstruction (ref-pretrain) settings.

Alternatively, the NaturalProofs-Gen datasets are also stored in the data/ directory using git-lfs:

git-lfs pull

This will create the same file structure discussed above.

See npgen/gpt3/finetune_gpt3.sh.

For full-proof generation,

cd npgen/gpt3
python generate_gpt3_stepwise.py  # see generate_gpt3_stepwise.sh for example arguments

See npgen/gpt3/generate_gpt3_stepwise.sh for example commands for greedy decoding, full-proof sample-and-select, and stepwise++ decoding. Also see npgen/gpt3/generate_gpt3.sh for greedy decoding commands using various models.

For next-step generation:

cd npgen/gpt3
python generate_gpt3.py --ckpt ${CKPT} --refs {no,gt,ret}refs --mode nextstep --core-only

See npgen/gpt3/generate_gpt3.sh for example commands.

For an example of running automatic metrics for full-proof generation, first download the naturalprover generations:

pip install gdown
python download.py --other --savedir /path/to/savedir

==> /path/to/savedir/other/naturalprover_generations

Then see this notebook for an example of running the metrics:

notebooks/evaluation.ipynb

The notebook reproduces the GPT-3 automatic metrics in the paper (Table 7).

We use the mallorbc/Finetune_GPTNEO_GPTJ6B repo. Setup that repo by following its README, then see npgen/gptj/train_gpt{j,2}.sh for example commands.

We provide a GPT-2 model fine-tuned with provided in-context references and reference reconstruction.

pip install gdown
python download.py --model --savedir /path/to/savedir

==> /path/to/savedir/model/naturalprover_gpt2

See commands in:

cd npgen/gptjft
bash eval_gpt2.sh

For GPT-J, see npgen/gptjft/eval_gptj.sh.

For an example of running automatic metrics for full-proof generation, first download the naturalprover generations:

pip install gdown
python download.py --other --savedir /path/to/savedir

==> /path/to/savedir/other/naturalprover_generations

Then see this notebook for an example of running the metrics:

notebooks/evaluation.ipynb

We provide GPT-2 and GPT-J6B generations (provided in-context references, greedy decoding) in /other/naturalprover_generations.

Due to a GPT-J6B-specific discrepancy, GPT-J6B achieves better results than in the inital manuscript

The repo does not have stepwise++ or next-step suggestions for GPT-2/J.