History

Qi Liu f4cc21cc96 Async: implemented; MiniF2F: fixed		2024-12-13 06:15:52 +00:00
..
MiniF2F	chore: Update Pantograph and Lean version to 4.12	2024-10-06 22:04:10 -07:00
model	feat: Handle exceptions in tactic generation	2024-10-11 22:51:20 -07:00
.gitignore	doc: Improve error message	2024-10-03 15:45:14 -07:00
README.md	fix: Filter out val/test data	2024-10-09 18:23:21 -07:00
main.py	fix: Experiments with new `load_sorry`	2024-12-11 17:32:07 -08:00
test.jsonl	Async: implemented; MiniF2F: fixed	2024-12-13 06:15:52 +00:00
valid.jsonl	Async: implemented; MiniF2F: fixed	2024-12-13 06:15:52 +00:00

MiniF2F

This is an experiment on running a LLM prover on miniF2F data. Build the project MiniF2F with lake build. Check the environment and data with

python3 experiments/minif2f/main.py check
python3 experiments/minif2f/main.py list

and run experiments with

python3 experiments/minif2f/main.py eval [--use-llm] [--use-hammer]

Read the help message carefully.

Developing

Run unit tests with

python3 -m model.{llm_agent,gen_tactic}