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

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)

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:

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

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).

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

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.