Rebuild lean-bench: pages in, verified indexed Lean out
Replaces the previous tree entirely. The pipeline is four separable pieces, each
testable on its own:
1. leanbench/llm.py provider-neutral OpenAI-compatible connector, stdlib only,
with retries, JSON coercion and a scripted client so the
rest of the code is testable without a network.
2. leanbench/detect.py per-page detection of formalizable mathematics. Case 1 is
mathematics asserted as fact (definition/theorem/lemma/...,
deliberately not sub-classified); case 2 is a problem left
open to the reader. Hits come back as spans -- start page
and index, end page and index -- so several per page is
normal. A hit cut off by the page end makes the detector
re-read that page together with the next, repeatedly, so an
item spread over three pages is found whole.
Offsets come from verbatim quotes resolved by
leanbench/anchors.py (exact -> whitespace-insensitive ->
fuzzy), because models quote well and count badly.
3. leanbench/formalize.py + leanbench/verify.py
each span becomes one Lean 4 declaration, judged by the real
compiler: full elaboration for case 1, statement legality
only for case 2, which has no proof to check. Lean's own
diagnostics feed back for a repair attempt. "verified" (Lean
accepted it) and "proved" (accepted with no sorry) are kept
strictly apart.
4. leanbench/db.py indexed SQLite plus JSONL export. Every item is indexed by
the types of its inputs, or by its own type when it is not a
proof, and records the source book (sha256) and the page it
starts on -- so `drop --source H --pages A-B` followed by a
re-ingest redoes exactly those pages and nothing else.
Infrastructure:
- lean/ Lake project pinned to Mathlib.
- docker/ image carrying Lean 4 and a prebuilt Mathlib. The Mathlib
revision and the toolchain are resolved against each other at
build time rather than both hardcoded, so the build does not rot.
One Docker layer per Lean step, each long one under `timeout`:
the gigabyte cache fetch earns a layer that a later failure never
invalidates, and a stalled step fails with a message instead of
sitting silent for an hour. There is deliberately no `lake build`
of our own library -- verification runs `lake env lean` against
Mathlib's oleans and needs nothing else, and building the library
was pure cost. docker/smoke.py runs the whole pipeline inside the
image against the real compiler, with the LLM scripted.
- .gitea/workflows ci (lint + tests in a venv, since the runner image's Python is
Debian-managed and refuses installs into itself), docker (build,
verify, optionally push), ingest (submit a book by hand). The
docker build runs with --progress=plain, because BuildKit's
default renderer collapses a long step into one rewritten line
and a stall then looks exactly like progress.
The docker workflow is not a throwaway build: it leaves the image, the layer cache,
an idle `lean-bench` container and the `lean-bench-data` / `lean-bench-books`
volumes in place on the runner, and never prunes, so the environment is there to be
used afterwards. Pushing to the registry is optional and cannot fail the build --
Gitea's container registry does not accept the built-in Actions token, so that needs
a REGISTRY_TOKEN secret with write:package.
58 tests; they need neither network nor Lean.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ci5T3gWDhhmqDec3e1XtYZ
This commit is contained in:
@@ -0,0 +1,224 @@
|
||||
# lean-bench
|
||||
|
||||
Point it at a mathematics book. It finds the mathematics worth formalizing, turns
|
||||
each piece into Lean 4, asks the Lean compiler whether that Lean is legal, and files
|
||||
the result in a database indexed by the types each item is about.
|
||||
|
||||
```
|
||||
book.pdf ──▶ detect ──▶ formalize ──▶ verify (Lean) ──▶ indexed database
|
||||
│ │ │ │
|
||||
spans across Lean 4 code statements for searchable by the
|
||||
pages, two per item open problems, types an item takes
|
||||
kinds of hit proofs when given in, or is
|
||||
```
|
||||
|
||||
## The four pieces
|
||||
|
||||
**1. The LLM connector** — `leanbench/llm.py`. Stdlib only, no SDK. Any
|
||||
OpenAI-compatible `/chat/completions` endpoint: DashScope/Qwen by default, equally
|
||||
happy with vLLM, Ollama, DeepSeek or OpenAI. Retries, JSON coercion, and a
|
||||
`ScriptedClient` so the rest of the code is testable without a network.
|
||||
|
||||
**2. Detection** — `leanbench/detect.py`. For every page, two questions:
|
||||
|
||||
- *Case 1, `statement`* — is there mathematics asserted as fact here? A definition,
|
||||
theorem, proposition, lemma, corollary, a precise claim inside an example. The
|
||||
kind is deliberately **not** recorded: all that matters is that it can become
|
||||
useful Lean 4.
|
||||
- *Case 2, `problem`* — is there a question left open to the reader? An exercise, an
|
||||
unsolved problem. Formalizable too, as a statement with no proof.
|
||||
|
||||
Each hit is returned as a span:
|
||||
|
||||
```json
|
||||
{"kind": "statement", "label": "Theorem 1.6.3",
|
||||
"start_page": 41, "start_index": 1832,
|
||||
"end_page": 42, "end_index": 96,
|
||||
"spans_pages": 2, "truncated": false}
|
||||
```
|
||||
|
||||
Indices are character offsets into that page's text, so several hits per page are
|
||||
normal and each is addressable. **If a passage runs off the bottom of the page**, the
|
||||
model says so, the page is re-read together with the next one, and that repeats —
|
||||
so an item spread over three pages is found whole, not in fragments. The limit is
|
||||
`--window` (default 3); an item still cut off at the limit is stored with
|
||||
`truncated: true` rather than silently clipped.
|
||||
|
||||
Models cannot count characters, so they are never asked to. They quote the first and
|
||||
last few words verbatim, and `leanbench/anchors.py` turns those quotes into exact
|
||||
offsets — exact match, then whitespace-insensitive match (PDF line breaks), then
|
||||
fuzzy match. A quote that matches none of the three is reported as unresolved, never
|
||||
guessed at.
|
||||
|
||||
**3. Formalization and verification** — `leanbench/formalize.py`, `leanbench/verify.py`.
|
||||
Every detected span becomes one self-contained Lean 4 declaration, which Lean then
|
||||
judges:
|
||||
|
||||
| item | what is checked |
|
||||
|---|---|
|
||||
| `statement` with a proof in the book | the whole declaration, proof included |
|
||||
| `statement` without one | the statement elaborates; the proof is `sorry` |
|
||||
| `problem` (case 2) | **statement legality only** — there is no proof to check |
|
||||
|
||||
When Lean rejects the code, its diagnostics go straight back to the model for one
|
||||
more attempt (`LEANBENCH_REPAIR_ATTEMPTS`). Two flags are kept apart on purpose:
|
||||
`verified` means Lean accepted it, `proved` means Lean accepted it **with no `sorry`
|
||||
anywhere**.
|
||||
|
||||
**4. The database** — `leanbench/db.py`. SQLite, indexed, plus a JSONL export for
|
||||
git. Each item records:
|
||||
|
||||
- its Lean code, imports, and what Lean said;
|
||||
- **the types it is indexed under** — for a proof, the types of its inputs and
|
||||
hypotheses; for a definition, the type of the thing being defined. That is what
|
||||
makes one item relevant to another, and it is what search runs on;
|
||||
- **which book** (sha256 of the file) and **which page it starts on**.
|
||||
|
||||
So any part of any source can be redone without touching anything else:
|
||||
|
||||
```bash
|
||||
lean-bench drop --source <hash> --pages 30-45 # forget those pages
|
||||
lean-bench ingest book.pdf --pages 30-45 # and do them again
|
||||
```
|
||||
|
||||
Re-ingesting does this for you: a run over pages 30–45 deletes exactly the items
|
||||
filed under those pages first. Item identity is `sha1(book hash + span)`, so the same
|
||||
passage of the same book is always the same row.
|
||||
|
||||
## Quick start
|
||||
|
||||
```bash
|
||||
pip install -e ".[dev]"
|
||||
cp .env.example .env # put your API key in it
|
||||
lean-bench doctor # is the LLM reachable? is Lean installed?
|
||||
|
||||
lean-bench ingest book.pdf --pages 30-60 --export datasets/items.jsonl
|
||||
lean-bench stats
|
||||
lean-bench search --type Int --role input --kind problem --code
|
||||
```
|
||||
|
||||
Lean verification needs a Lean project with Mathlib built. Without one, everything
|
||||
still runs and nothing claims to be verified. With Docker you get one for free:
|
||||
|
||||
```bash
|
||||
docker run --rm -e DASHSCOPE_API_KEY \
|
||||
-v "$PWD/books:/books" -v "$PWD/data:/data" \
|
||||
gitea.entroia.com/zayden-jung/lean-bench:latest \
|
||||
ingest /books/book.pdf --pages 30-60
|
||||
```
|
||||
|
||||
## Commands
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| `lean-bench doctor` | check the LLM, Lean and PDF wiring |
|
||||
| `lean-bench ingest SRC` | the whole pipeline; `--pages`, `--no-verify`, `--export` |
|
||||
| `lean-bench detect SRC` | detection only — no Lean, no database |
|
||||
| `lean-bench search` | by `--type`, `--role`, `--kind`, `--page`, `--text` |
|
||||
| `lean-bench sources` / `stats` | what is in the database |
|
||||
| `lean-bench export OUT` | JSONL dump |
|
||||
| `lean-bench drop --source H` | forget a source, or `--pages` of it |
|
||||
|
||||
Sources may be PDFs, or `.txt` files whose pages are separated by form feeds
|
||||
(what `pdftotext` emits).
|
||||
|
||||
## Configuration
|
||||
|
||||
All environment, all optional, all overridable in `.env`:
|
||||
|
||||
| variable | default |
|
||||
|---|---|
|
||||
| `LEANBENCH_LLM_MODEL` | `qwen-max` |
|
||||
| `LEANBENCH_LLM_BASE_URL` | DashScope's OpenAI-compatible endpoint |
|
||||
| `LEANBENCH_LLM_API_KEY_ENV` | `DASHSCOPE_API_KEY` |
|
||||
| `LEANBENCH_DATABASE` | `database/leanbench.sqlite` |
|
||||
| `LEANBENCH_MAX_WINDOW_PAGES` | `3` |
|
||||
| `LEANBENCH_REPAIR_ATTEMPTS` | `1` |
|
||||
| `LEANBENCH_LEAN_COMMAND` | `["lake","env","lean"]` |
|
||||
| `LEANBENCH_LEAN_PROJECT` | unset (a Lake project with Mathlib built) |
|
||||
|
||||
## CI/CD
|
||||
|
||||
Three Gitea Actions workflows, for the `ubuntu-latest` / `ubuntu-24.04` /
|
||||
`ubuntu-22.04` runner:
|
||||
|
||||
- **`ci`** — lint and the full test suite on every push. No network, no Lean: the
|
||||
LLM is scripted and the compiler is faked, so it is fast and deterministic. It
|
||||
installs into a venv, because the runner image's Python is Debian-managed and
|
||||
refuses installs into itself (PEP 668).
|
||||
- **`docker`** — builds the Lean 4 + Mathlib image and checks it honestly: Mathlib
|
||||
really elaborates inside it, and a scripted end-to-end run (`docker/smoke.py`)
|
||||
proves the pipeline writes a verified item to the database with the real compiler
|
||||
attached. The Mathlib revision and the Lean toolchain are resolved *against each
|
||||
other* at build time (`docker/resolve-mathlib.sh`), because hardcoding both is how
|
||||
image builds break two months later.
|
||||
|
||||
The Lean steps are one Docker layer each, and each long one is wrapped in
|
||||
`timeout`. That is not tidiness: the Mathlib cache fetch is gigabytes, so it earns
|
||||
a layer that a later failure never invalidates, and a stalled `lake` step fails
|
||||
with a diagnosable message instead of sitting silent for hours. The build also
|
||||
runs with `--progress=plain`, because BuildKit's default renderer collapses a
|
||||
long step into one rewritten line and a stall then looks exactly like progress.
|
||||
There is deliberately no `lake build` of our own library: verification runs
|
||||
`lake env lean <scratch file>`, which needs Mathlib's oleans and nothing else.
|
||||
- **`ingest`** — run by hand: submit a book (repo path or URL), pick a page range.
|
||||
It runs inside the long-lived container and the results stay in the volume; the
|
||||
artifact is just a copy.
|
||||
|
||||
### What the runner needs
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| RAM | **4 GB minimum, 8 GB comfortable** |
|
||||
| disk | ~20 GB free for the image plus its layer cache |
|
||||
| docker | the CLI plus the host socket (or a docker-in-docker runner) |
|
||||
|
||||
Memory is the real constraint, and it is not negotiable: loading Mathlib's
|
||||
environment needs several GB, and the pipeline does exactly that for **every item it
|
||||
verifies**, not just once at build time. Below the threshold Lean does not fail
|
||||
cleanly — it thrashes, prints nothing, and eventually something kills it. The
|
||||
`docker` workflow therefore checks the host's memory before it starts and refuses
|
||||
with an explanation rather than discovering it forty minutes in. Override with
|
||||
`skip_size_check` if you know better than the check does.
|
||||
|
||||
### The build is not a throwaway
|
||||
|
||||
When the `docker` workflow finishes, the runner host still has everything it built:
|
||||
|
||||
| what | name |
|
||||
|---|---|
|
||||
| image | `lean-bench:latest`, `lean-bench:sha-<commit>` |
|
||||
| layer cache | kept — nothing ever runs `docker system prune`, so a rebuild reuses Mathlib instead of refetching it |
|
||||
| idle container | `lean-bench` (`--restart unless-stopped`) |
|
||||
| volumes | `lean-bench-data` (the database), `lean-bench-books` |
|
||||
|
||||
So you can use it directly, with no rebuild and no `docker run`:
|
||||
|
||||
```bash
|
||||
docker cp your-book.pdf lean-bench:/books/
|
||||
docker exec -e DASHSCOPE_API_KEY=sk-... lean-bench \
|
||||
lean-bench ingest /books/your-book.pdf --pages 30-60
|
||||
docker exec lean-bench lean-bench search --type Int --role input --code
|
||||
```
|
||||
|
||||
A rebuild leaves a running container alone rather than interrupting whatever is in
|
||||
it; re-run the workflow with `refresh_service=true` to move it onto the new image.
|
||||
|
||||
### Secrets
|
||||
|
||||
| name | kind | why |
|
||||
|---|---|---|
|
||||
| `DASHSCOPE_API_KEY` | secret | the LLM, for `ingest` |
|
||||
| `REGISTRY_TOKEN` | secret | a personal access token with `write:package`. **The built-in Actions token is not accepted by Gitea's container registry**, so without this the image is not pushed — it is still built and kept on the runner, and the build does not fail |
|
||||
| `REGISTRY_USER` | variable | only if the pushing account is not the actor |
|
||||
|
||||
## What this does not claim
|
||||
|
||||
Lean says whether the code is *legal*, and — when there is a proof — whether it is
|
||||
*correct*. It cannot say the Lean faithfully renders what the book meant. A
|
||||
well-formed statement of the wrong theorem passes every check here. `confidence`,
|
||||
`match_method` and the stored `source_text` are kept so that judgement stays
|
||||
possible; spot-check before trusting a dataset.
|
||||
|
||||
Source books are not committed. `.gitignore` keeps PDFs and extracted text out of
|
||||
the repository; only code and the short Lean datasets belong in git.
|
||||
Reference in New Issue
Block a user