# Finetuning GPT-3 with ProofWiki

## Generate the dataset

**Generate the reference-augmented data.**

Go to the repo's root directory and run
```
python npgen/raug/format_natproofs.py \
    --filepath data/latest/proofwiki.json \
    --output-dir data/latest/ \
    --dataset-name proofwiki \
    --refs ground_truth
python npgen/raug/format_natproofs.py \
    --filepath data/latest/proofwiki.json \
    --output-dir data/latest/ \
    --dataset-name proofwiki \
    --refs retrieved
```
This should create two additional files in `data/latest/`.

**Generate the GPT3-specific data.**

Go to `gpt3ft/` and run
```
python convert_to_gpt3ft.py --refs no --ref-pretrain
python convert_to_gpt3ft.py --refs gt --ref-pretrain
python convert_to_gpt3ft.py --refs ret --ref-pretrain
```
This should create 9 new files in `gpt3ft/data/latest/`.

**Finetune GPT3.**

Go to `gpt3ft/` and run
```
openai api fine_tunes.create -m curie \
    -t gpt3ft_proofwiki_norefs.train.jsonl \
    -v gpt3ft_proofwiki_norefs.valid.jsonl
```
If you wish to finetune with other datasets, pass the appropriate values to the -t and -v params.

**Generate from finetuned GPT3.**

Obtain the finetuned model name. It should look something like `curie:{ANONYMIZED}`. Run
```
python generate.py --ckpt [MODEL_NAME] --refs norefs --mode fullgen
python generate.py --ckpt [MODEL_NAME] --refs norefs --mode nextstep
```
Make sure that the --refs param should match the training setting of the model ckpt used here.

**Generate with stepwise search.**
Use `python generate_stepwise.py` instead of `generate.py`. 

Note that stepwise search is only supported for full proof generation.

Examples:
```bash
# greedy-decoding
python gpt3ft/generate_greedy_stepwise.py --ckpt "$ENGINE_GT" --refs gtrefs --mode full --temperature 0.0 --split "$SPLIT" --reduced-idxs "$REDUCED" --n 1 --max-steps "$MAX_STEPS" --num-runs 1

## full-proof sampling
python gpt3ft/generate_greedy_stepwise.py --ckpt "$ENGINE_GT" --refs gtrefs --mode full --temperature "$TEMP" --split "$SPLIT" --reduced-idxs "$REDUCED" --n "$N" --max-steps "$MAX_STEPS" --num-runs "$NRUNS" --alpha "$ALPHA"

# stepwise beam
python gpt3ft/generate_greedy_stepwise.py --ckpt "$ENGINE_GT" --refs gtrefs --mode stepwise_beam --split "$SPLIT" --reduced-idxs "$REDUCED"  --expansion multitemp --selection diversity  --temperature "$TEMP" --n "$N" --num-runs "$NRUNS" --max-steps "$MAX_STEPS" --alpha "$ALPHA"
```
See `generate_stepwise.sh` for detailed commands.


