docs/USAGE.md

# Usage guide (English)

This package is **DuoTactic** — a Lean 4 proof-search harness — together with the 39.58 M-parameter
tactic model (`leanoar-schemec-40m`) that it can use as an optional candidate generator.

* To **run the harness** (sections 3 onward) you need Lean `4.35.0-rc2` and a mathlib4 checkout with a
  prebuilt `.lake` cache (~10 GB). This is what produces miniF2F `test` 32.8 % / `valid` 34.8 %, at
  45 s per problem, with every accepted proof re-compiled by the kernel.
* To **load or sample the model** (sections 0–2) you need no Lean. Note that `SchemeC` is **not** a
  standard `transformers` model: it is defined in `code/leanoar/model.py`, its weights are plain
  `lit_model.pth` / `model.safetensors` files, and it emits a *single Lean tactic* per call. There is
  no `AutoModelForCausalLM.from_pretrained`. Everything below is copy-paste runnable from the package
  root.

```
duotactic/
├── code/eval_minif2f.py       DuoTactic itself: the end-to-end search harness
├── code/leanoar/              search + batched verifier + the 40M model
├── checkpoints/e6/            model weights (highest dev top-1)
├── checkpoints/stage3-e3/     model weights, end-to-end best variant (same pass@1, 16% faster)
├── data/dev/                  dev protocol arrays (1024 rows)
├── data/minif2f/              miniF2F valid/test records + .lean files
├── data/whitelist/            seed for the search's first-token whitelist
├── examples/dev_sample.jsonl  16 real dev states + the real mathlib tactic
├── config.json metrics.json tokenizer_v1.json special_tokens_v1.json SHA256SUMS
└── README.md  README.zh.md  docs/USAGE.md  docs/USAGE.zh.md
```

## 0. Install and verify

```bash
pip install -r code/requirements.txt      # torch>=2.4, tokenizers>=0.19, numpy>=1.26, safetensors>=0.4
python -c "import torch; print(torch.__version__, torch.cuda.is_available())"

python code/verify_package.py             # full check, 1024 dev rows (≈1 min on GPU)
python code/verify_package.py --quick     # 128 rows, CPU-friendly
```

`verify_package.py` prints four sections and ends with `PASS` / `FAIL`:

1. **parameter count** — rebuilds `SchemeC` from `config.json`, must be 39,582,595 for both variants;
2. **dev protocol** — recomputes top-1/top-5/CE on the packaged 1024 rows and compares with
   `metrics.json` (tolerance 5e-4). This is the check that makes the published numbers auditable;
3. **inference wiring** — runs the packaged example state through the sampler (it also shows whether
   the model's preferred first token matches mathlib's; a miss is normal and does not fail the check);
4. **checksums** — every file against `SHA256SUMS`.

Exit code is 0 only if 1, 2 and 4 pass. Use `--skip-sums` if you only have the weights.

## 1. Standalone inference (no Lean)

```bash
python code/generate.py                              # packaged dev example #0
python code/generate.py --example 3 --k 8            # another real dev state
python code/generate.py --state-file state.txt       # your own state (format below)
python code/generate.py --ckpt checkpoints/stage3-e3 # the other variant
```

A **state** is the text Lean prints for a goal, i.e. hypotheses then `⊢ goal`:

```
n m : ℕ
h : n < m
⊢ n ≤ m
```

You can obtain one from Lean with `trace_state` inside a proof, or from an `unsolved goals` error
message. In your own code:

```python
import json, os, sys, torch
sys.path.insert(0, 'code')
from common import load_model, load_tokenizer, encode_state, specials, whitelist
from generate import propose

net, cfg, device = load_model('checkpoints/e6')     # or 'checkpoints/stage3-e3'
tok, wl = load_tokenizer(), whitelist()
for tactic, avg_logprob in propose(net, tok, wl, state, k=16, device=device):
    ...   # send to Lean for verification
```

Four rules that matter:

* **Restrict the first token** to `first_token_whitelist.json` (64 ids, 97.6 % of training first
  tokens). `propose()` already does this. Without it, most candidates start with meaningless tokens
  and the type-check rate collapses.
* **One candidate is one tactic.** The model separates two intended steps by a double space and may
  end a truncated tactic with a dangling connective; `propose()` cuts both.
* **Truncation**: states longer than `ctx − 4 − max_new_tokens` tokens keep the head 60 % and the
  tail 40 % (the `⊢ goal` line is last). Never feed more than `context_length` tokens total.
* **Only the Lean kernel decides correctness.** Ask for many candidates and verify them; do not trust
  any single output. Whole-tactic exact match is 0/200, and a "valid" (type-checking) candidate is
  still not a proof.

## 2. Reproduce the dev metric

```bash
python code/eval_dev.py --all --compare     # both variants, 1024 rows, compare with metrics.json
python code/eval_dev.py --ckpt checkpoints/e6 --rows 256
```

Expected (tolerance 5e-4):

| variant | top-1 | top-5 | CE |
|---|---|---|---|
| `checkpoints/e6` | 0.3076 | 0.7090 | 2.5494 |
| `checkpoints/stage3-e3` | 0.2891 | 0.7246 | 2.4971 |

The protocol: take the first 1024 rows of `data/dev/dev_ids.npy` whose second token is `<|FORWARD|>`,
read the logits at `mask_start − 1` and score the token at `mask_start`. **Do not compare these with
the numbers a trainer prints** — those come from a length-bucketed reshuffle of the dev split.

## 3. End-to-end proof search on miniF2F (needs Lean + mathlib)

### 3.1 Prerequisites

* A **Lean 4.35.0-rc2** toolchain (e.g. `elan toolchain install leanprover/lean4:v4.35.0-rc2`).
  Note: this is a *release candidate*; newer Lean versions will re-elaborate mathlib differently.
* A **mathlib4 checkout with a prebuilt `.lake` cache** (this project used the Sept 2026 mathlib
  snapshot; the exact commit is not pinned in the release, so state text may drift slightly on other
  revisions). Build the cache with `lake exe cache get` inside the checkout — a full local build takes
  hours, the olean cache takes minutes and ~7 GB.
* ≥ 16 GB RAM if you use `--lean-parallel 6` (each `lean --json` process loads mathlib; ~0.4 s per
  candidate, 6 in parallel measured at 0.034 s/candidate).

```bash
export LEANOAR_LEAN_BIN=/path/to/lean-4.35.0-rc2-linux/bin/lean
export LEANOAR_MATHLIB=/path/to/mathlib4
$LEANOAR_LEAN_BIN --version          # sanity check
```

### 3.2 The run that produced the published number

```bash
python code/eval_minif2f.py --split valid --n 89 --start 0 \
    --k 16 --beam 4 --depth 6 --budget 45 --round-budget 30 \
    --force --force-set v2 --force-depth 99 --lean-parallel 6 \
    --ckpt checkpoints/stage3-e3 --tag mine
```

Expected: **30/89 = 33.7 %**, ≈52 min on an RTX 4060 Laptop (the `e6` variant gives the same 30
problems in ≈60 min). The full `valid` split was run end-to-end with this exact configuration:
**85/244 = 34.8 %** in ≈2.3 h (segments 33.7 % / 40.4 % / 28.8 %; 78 of the 85 solutions are one
tactic). Longer runs are easier as `--lean-parallel` rises: the fixed cost of every `lean --json`
call is ≈6.6 s of `import Mathlib` (vs ≈0.03 s per candidate), so parallelism and import trimming
are where the wall clock goes.

What the flags do — this is where the score comes from:

| Flag | Meaning |
|---|---|
| `--k 16` | candidates per state (top-16 whitelisted first tokens, greedy continuation) |
| `--beam 4` | how many open states are expanded per round |
| `--depth 6` | max proof length in tactics (measured: 25 of 30 solutions are depth 1) |
| `--budget 45` | wall-clock seconds per problem; `--round-budget 30` caps a single round |
| `--force --force-set v2` | inject the exported automation table (`rfl`, `ring`, `simp_all`, `omega`, …, `simp_all ; ring`, `gcongr`) at every depth. **This is the single biggest lever**: with it the first-89 result is 30/89, without it the whole 244 gives 8/244. |
| `--lean-parallel 6` | verify 6 chunks of candidates concurrently (pure engineering: 2.07× wall clock) |
| `--narrow-imports` | per problem, replace the full Mathlib import by `#min_imports` + `Mathlib.Tactic` (measured 3.41 s → 1.74 s per `lean --json` call). A candidate that fails with "unknown identifier/tactic" is automatically re-checked with the full import, so narrowing cannot lose a proof (verified: 85/85 accepted valid proofs still compile) |
| `--no-model` | ablation switch: verify only the injected table, no model proposals. On valid problems 0-9 this reproduces the model's result exactly (2/10, same problems, same proof terms) in half the wall clock |

Before quoting any pass rate, read **“Where this score comes from”** in `README.md`: these are
*system* numbers (injected automation table + search + kernel verification), and the shipped model
supplies 0 of the accepted proofs.

### 3.3 Reading and resuming results

Results are appended to `reports/search_eval_valid_mine.jsonl` (one JSON object per problem:
`solved`, `depth`, `seconds`, `verified`, `proof`, `confirmed`, `reason`) and every run prints
cumulative progress with an ETA. Because the file is append-only, an interrupted run resumes with
`--start <rows already written>` — or simply re-run the same command.

### 3.4 Troubleshooting

* `initial-state-failed` for a problem: its statement does not even compile against your mathlib
  revision. Two miniF2F problems fail on mathlib master for everyone
  (`mathd_numbertheory_711`, `imosl_2007_algebra_p6`).
* `No such file or directory: .../bin/lean`: set `LEANOAR_LEAN_BIN`.
* Lean errors about missing oleans / `unknown module prefix 'Mathlib'`: set `LEANOAR_MATHLIB` to a
  checkout with a **built** `.lake/build/lib/lean` (and `.lake/packages/*`); the verifier assembles
  `LEAN_PATH` from those paths.
* Very low `verified` counts: check that the first-token whitelist is being applied and that the
  tokenizer is `tokenizer_v1.json`.
* A state longer than the prompt budget used to overflow the context by one token in old builds; the
  shipped `search.py` budgets `ctx − 4 − max_new_tokens` and hard-stops at `ctx`. If you edit the
  sampler, keep that invariant.

## 4. Extending

* Swap in your own weights: put `lit_model.pth` (+ `model.safetensors`) in a directory and pass
  `--ckpt <dir>` to `generate.py` / `eval_dev.py` / `eval_minif2f.py`. `config.json` must match the
  architecture; the vocabulary and context length are fixed.
* Add automation tactics to `FORCE_SETS` in `code/eval_minif2f.py` — measured gains in this project
  came almost exclusively from that table and from the search/verifier side, not from the model.
* The value head is shipped but unusable (AUC 0.5201, below the policy's own confidence). Do not
  build a reranker on it.
* `code/leanoar/data.py` is included because the search code imports `load_specials` from it; the
  training pipeline itself is not part of this package.