2024-10-01 11:34:30 -07:00
|
|
|
# MiniF2F
|
|
|
|
|
|
2024-10-03 15:45:14 -07:00
|
|
|
This is an experiment on running a LLM prover on miniF2F data. Build the project
|
|
|
|
|
`MiniF2F` with `lake build`, and run with
|
2024-10-01 11:34:30 -07:00
|
|
|
|
|
|
|
|
```sh
|
2024-10-03 15:45:14 -07:00
|
|
|
python3 experiments/minif2f/main.py [--dry-run] [--use-llm]
|
2024-10-01 11:34:30 -07:00
|
|
|
```
|
2024-10-03 12:53:07 -07:00
|
|
|
|
2024-10-03 15:45:14 -07:00
|
|
|
Read the help message carefully.
|
|
|
|
|
|
2024-10-03 12:53:07 -07:00
|
|
|
## Developing
|
|
|
|
|
|
|
|
|
|
Run unit tests with
|
|
|
|
|
|
|
|
|
|
``` sh
|
|
|
|
|
python3 -m model.{llm_agent,gen_tactic}
|
|
|
|
|
```
|
|
|
|
|
|
