README.md · Duoia/duotactic at main

fix: retag as proof-search harness, drop model-centric tags

e5876f2 verified 28 days ago

20.6 kB

---
license: apache-2.0
language:
  - en
tags:
  - lean4
  - theorem-proving
  - proof-automation
  - proof-search
  - tactic-search
  - formal-mathematics
  - mathlib
  - miniF2F
  - proof-harness
  - automated-reasoning
  - interactive-theorem-proving
pipeline_tag: text-generation
---
# DuoTactic — a Lean 4 proof-search harness

> **32.8 % of miniF2F `test`, 34.8 % of miniF2F `valid`, 45 s per problem, every accepted proof
> re-compiled by the Lean kernel.**
> DuoTactic ships with a 39.58 M-parameter tactic model as an **optional candidate generator**; the
> measured end-to-end contribution of that model to those two numbers is **0 of the 165 solved
> problems** (see *Provenance of the score*).

**[中文说明: README.zh.md](README.zh.md) · [Usage guide (EN)](docs/USAGE.md) · [使用说明（中文）](docs/USAGE.zh.md)**

## What DuoTactic is

One sentence: *a proof-search harness for Lean 4 that closes a goal by searching the compositions of
a fixed table of public automation tactics and only believes what the kernel re-compiles.*

Concretely, one `by`-tactic-shaped system with four moving parts:

1. **A fixed 16-entry automation table** (`--force-set v2`: `rfl`, `ring`, `omega`, `simp_all`,
   `linarith`, `trivial`, `nlinarith`, `aesop`, `simp`, `norm_num`, `simp_all ; ring`,
   `simp_all ; norm_num`, `simp_all ; omega`, `simp_all ; linarith`, `gcongr`, `field_simp ; ring`),
   injected at **every** frontier node of **every** depth — so the search also composes them
   (`simp_all` then `ring`), not just tries them once.
2. **Depth-batched best-first search** over the resulting candidate pool (k=16, beam 4, depth 6,
   45 s wall clock per problem, 30 s per round).
3. **Batched kernel verification**: all candidates of a round go into a few `.lean` files, one
   `lean --json` call each, and diagnostics are attributed back to candidates by line number.
4. **A `confirmed` verdict or nothing**: a problem counts as solved only if the accepted proof
   re-compiles standalone — exit code 0, no `error`, no `sorry`, and (audited) axiom dependencies
   ⊆ {`propext`, `Classical.choice`, `Quot.sound`}.

An optional 40M tactic model can feed extra candidates into the same pool (it competes with the
table on equal terms); it is not required, and `--no-model` switches it off completely.

### What DuoTactic is *not* — read this before comparing it to other tools

In the literature a **hammer** is defined as *premise selection + translation to an external
automatic theorem prover + reconstruction of a verified proof* (Sledgehammer, Magnushammer,
LeanHammer). DuoTactic does **none of those three**: there is no premise retrieval, no translation to
an external ATP, and no reconstruction from an external proof trace. Its whole search happens inside
Lean's kernel. Structurally it is closer to `aesop` (white-box best-first proof search over a rule
set) with a hand-fixed rule set, a per-problem budget and a verification back end.

|  | premise selection | external ATP | reconstruction | composition search | batched kernel verification |
|---|---|---|---|---|---|
| Sledgehammer / Magnushammer | ✓ | ✓ | ✓ | partial | — |
| LeanHammer | ✓ | ✓ | ✓ | aesop | — |
| **DuoTactic** | ✗ | ✗ | ✗ | ✓ | ✓ |

## Results

**End-to-end miniF2F** (search configuration in `docs/USAGE.md`). One run per problem, one attempt —
pass@1 *with a search harness*, not pass@k sampling:

| Setting | Problems | Passed | Wall |
|---|---|---|---|
| DuoTactic (model in the pool) | **valid, all 244** | **85/244 = 34.8 %** | 2.3 h |
| DuoTactic (model in the pool) | **test, all 244** | **80/244 = 32.8 %** | 2.5 h |
| DuoTactic (model in the pool) | valid, first 89 | 30/89 = 33.7 % | 51.7 min |
| model variant `e6` instead of `stage3-e3` | valid, first 89 | 30/89 = 33.7 % | 59.8 min |
| DuoTactic, `--no-model` (table only) | valid, first 10 | 2/10 = 20 % | 3.3 min |
| (older, weaker protocol: depth-1 injection, v1 table) | valid, all 244 | 8/244 = 3.3 % | — |

Segments of the full valid split: 0-89 → 33.7 %, 89-178 → 40.4 %, 178-244 → 28.8 %. Proof length:
**78 of the 85 solutions are a single tactic** (2 / 2 / 3 solutions at depths 2 / 3 / 4). Test split
segments: 38.2 % / 27.0 % / 33.3 %, **76 of the 80 solutions are a single tactic**. All 165 accepted
proofs are `confirmed`.

## Provenance of the score (read before quoting it)

The numbers above are **harness** numbers produced by items 1–4 of *What DuoTactic is*, with the 40M
model merely adding candidates to the same pool. Classifying every accepted proof by where its
**winning** tactic came from:

| Final tactic of the accepted proof | valid (85 solved) | test (80 solved) |
|---|---|---|
| the injected automation table, single step | 78 | 76 |
| the injected table, multi-step chain | 7 | 4 |
| **a tactic proposed by the 40M model** | **0** | **0** |

78/244 (valid) and 76/244 (test) are the *initial goal* closed by one injected tactic at depth 1 —
for those problems no model is in the loop at all. Disabling the model changes nothing: `--no-model`
on valid problems 0-9 returns **2/10 — the same problems, at the same depths, with the same proof
terms** — in 3.3 min instead of 6.5 min (the model's candidates roughly double the wall clock and add
no solution).

Honest one-liner: **a search over public Lean automation tactics, with kernel-checked verification,
solves 32.8 % of miniF2F `test` and 34.8 % of `valid` at 45 s per problem; the attached 40M tactic
model supplies 0 of those solutions.** Do not present these figures as a neural tactic-generation
result, and do not compare them with model-only pass@1 numbers from the literature (those have no
automation table; DuoTactic with the table removed would score 0).

Reproducing both sides of the ablation:

```bash
# the reported numbers (model in the pool)
python code/eval_minif2f.py --split test  --n 244 --k 16 --beam 4 --depth 6 \
    --budget 45 --round-budget 30 --force --force-set v2 --force-depth 99 \
    --lean-parallel 10 --verify-chunk 64 --narrow-imports \
    --ckpt checkpoints/stage3-e3 --tag test244
# the same harness with the model switched off
python code/eval_minif2f.py --split valid --n 244 --k 16 --beam 4 --depth 6 \
    --budget 45 --round-budget 30 --force --force-set v2 --force-depth 99 \
    --lean-parallel 10 --verify-chunk 64 --narrow-imports --no-model \
    --ckpt checkpoints/stage3-e3 --tag nomodel244
```

## How strong is it? Published baselines

| System | Class | miniF2F | Notes |
|---|---|---|---|
| Isabelle **Sledgehammer** | bare hammer | 20.9 % | the baseline every hammer paper reports |
| Isabelle **Magnushammer** | hammer + premise selection | 34.0 % | +13 points from premise selection alone |
| Lean `tidy` (Lean 3) | built-in automation | 23.8 % | on LeanDojo-random, **not** miniF2F — indicative only |
| **DuoTactic** | automation + composition search | **32.8 % test / 34.8 % valid** | 45 s per problem |
| Lean GPT-f (2021) | neural + search | 24.6 % test pass@1 | 10 min per problem, no automation table |
| ReProver / LeanDojo (2023) | neural + retrieval + search | 25.9 % test / 26.5 % valid | |
| DeepSeek-Prover-V1.5-RL (2024) | neural + MCTS | 50.0–50.7 % test | pass@32/64 |
| InternLM2.5-StepProver 7B | neural | 65.9 % test / 69.6 % valid | |
| BFS-Prover / V2 (2025) | neural + tree search | 72.95 % / 95.08 % test | |

Read that cautiously: the neural rows use per-problem budgets and sample counts far above our 45 s /
single attempt, and the Isabelle rows are a different proof assistant. The defensible claim is
narrow: **DuoTactic sits at the level of a premise-selecting hammer and ~1.6× above the bare-hammer
baseline, while being cheap (45 s/problem) and fully kernel-verified.** It is not competitive with
neural provers, and it is not meant to be.

Independent support for the design choice: on miniF2F-test, DeepSeek-Prover-V1.5-RL improves from
42/244 to 55/244 when a *fixed schedule of 15 tactic skeletons* is placed in the prompt, while
doubling the sampling budget (k=32 → k=64) finds **zero** additional proofs
(*Inference-Time Diversity in RL-Trained Lean Provers*, 2026). A fixed tactic skeleton schedule —
i.e. exactly what DuoTactic's table is — is a stronger inference-time lever than more sampling, even
for a 7B RL model.

## The tactic model (`leanoar-schemec-40m`) — an optional component

A **from-scratch** 39.58 M-parameter decoder-only transformer that reads a Lean 4 proof state
(`trace_state`-style text, including the `⊢ goal` line) and writes **one tactic**. Trainable and
runnable on a single 8 GB consumer GPU (RTX 4060 Laptop: 4.83 GiB VRAM, 36 k tok/s, 35.7 min for one
epoch over 317 k samples). Its dev metric is real; its end-to-end contribution is not (0/165).

```bash
pip install -r code/requirements.txt        # torch, tokenizers, numpy, safetensors
python code/verify_package.py               # verify this package against its own documented numbers
python code/generate.py                     # real dev example -> top-5 tactics
python code/generate.py --ckpt checkpoints/stage3-e3 --k 8
python code/eval_dev.py --all --compare     # recompute the dev metric for both variants
```

`verify_package.py` checks four things and prints PASS/FAIL: the parameter count, the dev protocol
(1024 fixed rows) against `metrics.json`, inference wiring, and the checksums. Real, unmodified output
of `python code/generate.py` on the packaged dev example #0:

```
--- real dev example #0 (row 0 of the packaged dev split) ---
--- state ---
T : Theory L
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T
--- top-5 tactics (device=cuda, ckpt=checkpoints/e6) ---
  -0.512  rw [IsUnit.iff_eq_bot] exact h.symm simp only [IsUnit.iff_eq_true
  -1.044  simp only [IsUnit.iff_eq, h.eq_iff, not_and_or, not_and_or]
  -0.475  refine ⟨fun h ↦ ?_, fun h ↦ h.trans h.symm⟩ exact h.symm exact h.symm exact h
  -0.105  constructor rw [IsUnit.iff_eq_bot] exact h.symm simp [h.symm]
  -0.694  exact ⟨fun h => h.trans h.symm, fun h => h.symm ▸ h.symm⟩ exact h.symm
--- the tactic mathlib actually used here (reference) ---
  rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
  h.completeTheory_eq]
```

That is what the model really produces: structurally plausible openers (`refine ⟨fun h ↦ ?_, …⟩`),
sensible context references (`h.symm`), and some concatenated garbage. Nothing matches the reference
tactic — which is exactly why verification is not optional.

**Dev, first-token protocol** (first 1024 `FORWARD` rows of the packaged dev split; logits at
`mask_start-1` predicting the token at `mask_start`). This is the only protocol comparable across
models — the trainer's logged dev numbers use a length-bucketed reshuffle and must not be compared.

| Variant | top-1 | top-5 | CE |
|---|---|---|---|
| `checkpoints/e6` | **0.3076** | 0.7090 | 2.5494 |
| `checkpoints/stage3-e3` | 0.2891 | **0.7246** | **2.4971** |
| trivial baseline (most frequent first token) | 0.2171 | 0.6079 | — |

### Architecture

| Component | Spec | Parameters |
|---|---|---|
| Backbone | decoder-only, 8 layers, d_model 640, 10 heads (head_dim 64), RoPE, RMSNorm, dropout 0.1 | — |
| Attention projections | Q/K/V/O = 4 × 640×640, no bias | 13,107,200 |
| SwiGLU FFN | d_ff 1536 (gate/up/down) | 23,592,960 |
| Token/output embedding | 4096 × 640, **tied** with the output projection | 2,621,440 |
| Policy head | low-rank 640 → **128** → tied embedding | 163,840 |
| Value head | MLP 640→128→32→3, observed under stop-grad only (experimentally negative, see below) | 86,275 |
| RMSNorm ×17, misc | — | 10,880 |
| **Total** | context 768, vocab 4096 | **39,582,595** |
The tied embedding plus a low-rank policy head keeps the model under 40 M, which is what makes the
whole data → train → search loop fit on one 8 GB card. `generate()` uses no KV cache (prefix
generation ≈ 12.4 ms/token), but that is ~8 % of wall clock; Lean compilation is 91 %.
### Training data
**A. LeanDojo/Mathlib traces (base split).** Of 87,766 mathlib declarations, 41,944 carry tactic
traces → 169,530 `(state, tactic)` pairs; 15 % REPAIR augmentation (a proof step replaced by its own
prefix state) + exact de-duplication by token payload → **188,501 training samples**.
**B. Self-built replay mining ("E6", new data).** 45,822 declarations had **no** trace; sampling showed
37 % of them are `:= by` proofs — only the *states* were missing. Method: wrap every prefix of every
source proof in its own probe declaration and read the state back from Lean's **`unsolved goals` error
message**; tactic boundaries are detected automatically by *state change*. Result: **8,536 files /
88,418 declarations / 401,523 probes → 136,258 pairs** in 83 minutes with 6-way parallelism, and
**0** pairs containing `sorry`/`admit`. Merged and de-duplicated against the base split:
**317,492 train / 6,165 dev** samples (`steps_v2`, context 768, covering 99.4 % of proof steps).

Note the **distribution shift**: the mined data mostly adds *proof-structure* tactics (`refine` share
0.55 % → 7.77 %, `convert!` 0 → 1 %, multi-line tactics 9.1 % → 22.4 %) while goal-*closing* tactics
drop (47.6 % → 27.6 %).

| Variant | Init | Data | Recipe | Wall |
|---|---|---|---|---|
| `stage3-e3` | low-lr fine-tune from an LM-pretrained checkpoint | 188,501 | lr 2e-5, 1 epoch tactic-only | 14.5 min |
| `e6` | **from scratch** | 317,492 | 1.5-epoch cap, early stop (best step 5000) | 35.7 min |

### What we measured about this component (four findings)

1. **The two variants solve exactly the same 30 problems (first 89) at exactly the same depths** —
   zero gained, zero lost. Raising dev top-1 from 0.2891 to 0.3076 (+1.85 points) bought **nothing**
   end-to-end and cost 16 % wall clock. This is the third independent time a model-side improvement
   failed to transfer to pass@1.
2. **Candidate-level reality**: only **7.9 %** of proposals type-check; **56.6 %** of states yield at
   least one type-checking candidate, but only **6.3 %** yield one that closes the goal. The
   bottleneck is closing, not proposing.
3. **The value head is not usable**: AUC 0.5201 vs 0.7475 for the policy's own confidence; reranking
   with it hit valid candidates 7.0 % of the time vs 19.6 % for plain top-1. Do not use it to rerank.
4. **The tail of the split is not a collapse**: without injection the last 66 problems score 1.5 %
   (first 89: 3.4 %), with injection they score 28.8 %. What lifted them was automation coverage,
   not any change in how hard the problems are.

### Known limitations of the model

1. Emits **one tactic at a time**; long proofs need external search to chain candidates.
2. Whole-tactic greedy exact match **0/200** — treat the output as candidates, never as answers.
3. **Repetition degeneration** happens (`ring ring ring ring`, `h₂ h₂ h₂ h₂`); search-side de-dup and
   Lean verification contain it.
4. **Hard-bound to the v1 id space**: always pair with `tokenizer_v1.json`. The project's other
   tokenizer (`tokenizer.json`) has an extra `<|premises|>` and shifts every content id by one;
   pairing it with these weights produces gibberish and a bogus CE.
5. **Context 768 is baked in.** Longer states are truncated to head 60 % + tail 40 % (the goal line is
   last). The prompt also reserves 4 special tokens plus the generation window: the harness budgets
   `ctx − 4 − max_new_tokens` state tokens.
6. **Model-side gains do not move pass@1** (see above). For a higher score, invest in the
   verifier/search side — that is where every measured gain came from.

### Known limitations of the harness

1. **No premise selection**: DuoTactic cannot invent a library lemma name, so problems whose proof
   needs a specific mathlib lemma it does not try are out of reach — that is the main reason the
   score stops at ~33 %.
2. **Lean/mathlib version sensitive**: collected and evaluated on Lean `4.35.0-rc2` + a mathlib4
   snapshot (Sept 2026). Two miniF2F problems do not compile on mathlib master at all
   (`mathd_numbertheory_711`, `imosl_2007_algebra_p6`).
3. **Fixed budget**: 45 s per problem and depth 6 cap the search; the ablation shows throwing more
   time at it was not where the gains were.
4. **Narrow imports**: with `--narrow-imports` each problem's header is replaced by `#min_imports` +
   `Mathlib.Tactic` (3.41 s → 1.74 s per `lean --json` call, 1.98× end-to-end on already-solved
   problems). Any candidate failing with "unknown identifier/tactic" is automatically re-checked with
   the full import, so narrowing cannot lose a proof (verified 85/85).

## Files

| Path | What it is |
|---|---|
| `code/eval_minif2f.py` | **DuoTactic itself** — the end-to-end harness that produced every pass rate in this card. |
| `code/leanoar/search.py` | depth-batched best-first search, frontier management, budgets, whitelist, `confirmed` verdict. |
| `code/leanoar/lean_batch.py` | batched `lean --json` verification, `confirm()`, narrow-import computation. |
| `code/leanoar/model.py`, `code/leanoar/data.py` | the 39.58 M model and its dataset/tokenizer plumbing. |
| `checkpoints/e6/` | model weights: `lit_model.pth` + `model.safetensors` + `training_meta.json`. Highest dev top-1 (0.3076). |
| `checkpoints/stage3-e3/` | model weights, **end-to-end best variant** (same architecture and size). Identical pass@1 to `e6`, 16 % faster. |
| `config.json` | Authoritative architecture, context length, special-token ids, prompt template, weight roles. |
| `metrics.json` | Every measured number, each with the protocol it was measured under. |
| `tokenizer_v1.json` | **Must be paired** — v1 id space (8 specials, ids 0–7). |
| `special_tokens_v1.json` | The 8 special token ids. |
| `first_token_whitelist.json` | 64 most frequent first tokens of the training split (97.6 % coverage). |
| `examples/dev_sample.jsonl` | 16 real dev states + the tactic mathlib actually used on them. |
| `data/dev/` | The dev protocol arrays (1024 fixed rows + `build_meta.json`) so anyone can recompute the headline metric. |
| `data/minif2f/` | miniF2F `valid`/`test` records + their `.lean` files, as used by the harness. |
| `data/whitelist/` | Small seed files from which the search code derives the first-token whitelist (instead of shipping 479 MB of training arrays). |
| `code/common.py`, `generate.py`, `eval_dev.py`, `verify_package.py` | loading / sampling / metric reproduction / one-shot package verification. |
| `docs/USAGE.md` / `docs/USAGE.zh.md` | Usage guide: standalone inference, metric reproduction, end-to-end search with Lean. |
| `SHA256SUMS` | Checksums of every file in the package. |
| `LICENSE` / `NOTICE` | Apache-2.0 text + upstream provenance (mathlib4, LeanDojo, miniF2F). |

Loading the model needs three things: `config.json` + a weight file (`lit_model.pth` or
`model.safetensors`) + `tokenizer_v1.json`. `code/generate.py` is the minimal correct example — copy
from it. Running the harness needs Lean + mathlib as well (next section).

## End-to-end search (needs Lean + mathlib)

`code/eval_minif2f.py` ships the harness that produced the numbers above, including the exported
automation-tactic table (`--force-set v2`). It needs a working Lean 4.35.0-rc2 toolchain and a mathlib4
checkout with a prebuilt `.lake` cache (≈10 GB); point the package at them with:

```bash
export LEANOAR_LEAN_BIN=/path/to/lean-4.35.0-rc2-linux/bin/lean
export LEANOAR_MATHLIB=/path/to/mathlib4
python code/eval_minif2f.py --n 89 --ckpt checkpoints/stage3-e3      # reproduce 30/89
```

Full setup, the exact search configuration, expected runtimes and troubleshooting: **`docs/USAGE.md`**.
Measured cost: 2 125 `lean --json` calls in 3.3 h on the valid split, 2 921 in 2.5 h on test with
narrow imports (3.1 s per call).

## Provenance and license

* Weights, tokenizer and data are derived from **mathlib4** (Apache-2.0) and **LeanDojo** traces
  (MIT). miniF2F (`data/minif2f/`) is MIT. Released under **Apache-2.0**, consistent with upstream —
  keep the provenance note if you redistribute, and cite mathlib4 and LeanDojo: they supplied all of
  the supervision. What this project adds is the pipeline, the search harness and the 40 M model.
* Training/inference environment: Python 3.13, torch 2.14 (cu130), WSL2 Ubuntu 24.04, single
  RTX 4060 Laptop (8 GB).
* Research artifact: **no guarantee** that any generated tactic is correct. Only the Lean kernel
  decides that — which is why every number here is a re-compilation, not a similarity score.