{"data":{"kind":"file","path":"README.md","version_id":"dj312f1ajb603n0e3eje675n","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":2868,"modified_at":"2025-12-10T14:16:15.885000","content_hash":"59c2d0dea209916fee08d9d65f12c1503f4713b07226474f3b4e957a83d4e289"},"entries":[],"content":"# ProverBench\n\n### Overview\n- **Environment ID**: `ProverBench`\n- **Short description**: Theorem proving environment for DeepSeek ProverBench problems using Lean 4 verification\n- **Tags**: theorem-proving, lean4, prover-bench, mathematics, eval\n\n### Datasets\n- **Primary dataset(s)**: DeepSeek ProverBench - 325 mathematical problems across 10 domains\n- **Source links**: [https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench)\n- **Split sizes**: Configurable filtering by mathematical area, problem count\n\n### Task\n- **Type**: single-turn\n- **Parser**: Custom Lean 4 code block extractor (```lean4 or ```lean)\n- **Rubric overview**: Binary verification (1.0/0.0) via kimina-lean-server compilation\n\n### Prerequisites\n- **Docker**: Required for kimina-lean-server (default) OR\n- **Local Setup**: kimina-lean-server installed locally (set `use_docker=false`)\n\n### Quickstart\nRun an evaluation with default settings:\n\n```bash\nuv run vf-eval ProverBench\n```\n\nConfigure model, sampling, and filtering:\n\n```bash\nuv run vf-eval ProverBench \\\n  -m gpt-4o-mini \\\n  -n 20 -r 1 -t 4096 -T 0.7 \\\n  -a '{\"areas\": [\"Number Theory\", \"Linear Algebra\"], \"max_examples\": 10}'\n```\n\n### Environment Arguments\n\n| Arg | Type | Default | Description |\n| --- | ---- | ------- | ----------- |\n| `cache_path` | str | `~/.cache/verifiers/environments/proverbench` | Local cache for ProverBench dataset |\n| `areas` | list | `None` | Filter by mathematical areas, e.g., `[\"Number Theory\", \"Calculus\"]` |\n| `max_examples` | int | `-1` | Limit dataset size (-1 for all) |\n| `server_port` | int | `8000` | Port for kimina-lean-server |\n| `server_memory` | str | `\"4g\"` | Memory limit for kimina-lean-server |\n| `use_docker` | bool | `True` | Use Docker for kimina-lean-server (vs local install) |\n\n### Available Filters\n**Mathematical Areas**:\n- `AIME` (15 problems) - Competition problems from AIME 2024 & 2025\n- `Number Theory` (40 problems)\n- `Elementary Algebra` (30 problems) \n- `Linear Algebra` (50 problems)\n- `Abstract Algebra` (40 problems)\n- `Calculus` (90 problems)\n- `Real Analysis` (30 problems)\n- `Complex Analysis` (10 problems)\n- `Functional Analysis` (10 problems)\n- `Probability` (10 problems)\n\n### Metrics\n\n| Metric | Meaning |\n| ------ | ------- |\n| `reward` | 1.0 if proof compiles successfully, 0.0 otherwise |\n| `verification_success` | Boolean compilation success |\n| `parse_success` | Boolean code block extraction success |\n| `error` | Compilation error message if failed |\n| `compilation_output` | Full compiler output for debugging |\n\n### Setup Notes\n- First run automatically downloads ProverBench dataset from HuggingFace\n- kimina-lean-server starts automatically via Docker\n- Requires internet connection for initial setup\n- Each problem includes informal statement and formal Lean 4 theorem","encoding":"utf-8","truncated":false,"total_bytes":2868},"status":null}