# 使用说明（中文）

本包是 **DuoTactic** —— 一个 Lean 4 证明搜索 harness —— 连同它可选的候选生成器：39.58 M 参数的
tactic 模型（`leanoar-schemec-40m`）。

* **跑 harness**（第 3 节起）需要 Lean `4.35.0-rc2` 与带预编译 `.lake` 缓存的 mathlib4（约 10 GB）。
  miniF2F `test` 32.8% / `valid` 34.8% 就是它跑出来的：每题 45 s，每条被接受的证明都经内核重编译。
* **加载/采样模型**（第 0–2 节）不需要 Lean。注意 `SchemeC` **不是**标准 `transformers` 模型：它定义在
  `code/leanoar/model.py`，权重是普通的 `lit_model.pth` / `model.safetensors`，每次调用只产**一条
  Lean tactic**，没有 `AutoModelForCausalLM.from_pretrained` 这种入口。下面所有命令都可以在包根目录
  直接复制运行。

```
duotactic/
├── code/eval_minif2f.py      DuoTactic 本体：端到端搜索 harness
├── code/leanoar/             搜索 + 批量验证器 + 40M 模型
├── checkpoints/e6/           模型权重（dev top-1 最高）
├── checkpoints/stage3-e3/    模型权重，端到端最佳变体（同样通过率，快 16%）
├── data/dev/                 dev 协议数组（1024 行）
├── data/minif2f/             miniF2F valid/test 题目 + .lean 文件
├── data/whitelist/           搜索用首 token 白名单的种子文件
├── examples/dev_sample.jsonl 16 条真实 dev 状态 + 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. 安装与验证

```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             # 完整校验，1024 行（GPU 约 1 分钟）
python code/verify_package.py --quick     # 128 行，CPU 也能跑
```

`verify_package.py` 打印四段，最后给出 `PASS` / `FAIL`：

1. **参数数量**——从 `config.json` 重建 `SchemeC`，两个变体都必须是 39,582,595；
2. **dev 协议**——在包内 1024 行上复算 top-1/top-5/CE 并与 `metrics.json` 对比（容差 5e-4）。
   这一步让公开数字是可审计的；
3. **推理连通性**——拿包内示例状态跑一遍采样（同时显示模型首选首 token 是否与 mathlib 一致；
   不一致是正常的，不影响判定）；
4. **校验和**——逐文件对照 `SHA256SUMS`。

只有 1、2、4 全过才返回 0。只有权重时可用 `--skip-sums`。

## 1. 独立推理（不需要 Lean）

```bash
python code/generate.py                              # 包内真实 dev 样本 #0
python code/generate.py --example 3 --k 8            # 另一条真实 dev 状态
python code/generate.py --state-file state.txt       # 你自己的状态（格式见下）
python code/generate.py --ckpt checkpoints/stage3-e3 # 换变体
```

**状态**就是 Lean 打印目标时的那段文本——先是假设，然后 `⊢ 目标`：

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

可以在证明里用 `trace_state` 拿到，或从 `unsolved goals` 报错里抠出来。在自己的代码里调用：

```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')     # 或 'checkpoints/stage3-e3'
tok, wl = load_tokenizer(), whitelist()
for tactic, avg_logprob in propose(net, tok, wl, state, k=16, device=device):
    ...   # 交给 Lean 验证
```

**四条必须遵守的规则**：

* **首个 token 必须限制**在 `first_token_whitelist.json`（64 个 id，覆盖训练集 97.6% 的首 token）。
  `propose()` 已经做了这件事；不做的话多数候选会以无意义 token 开头，编译通过率会崩。
* **一条候选 = 一条 tactic**。模型用双空格分隔它想表达的两步；被截断的 tactic 可能以悬挂连接词结尾，
  `propose()` 两种都会切掉。
* **截断规则**：超过 `ctx − 4 − max_new_tokens` 个 token 的状态，会保留头部 60% + 尾部 40%
  （`⊢ 目标` 在最后）。总输入绝不能超过 `context_length`。
* **只有 Lean 内核能判对错**。请多要候选 + 逐个验证，不要相信任何单条输出。整条 tactic 的精确匹配率是
  0/200，而且「通过编译（valid）」也不等于「证明成立」。

## 2. 复算 dev 指标

```bash
python code/eval_dev.py --all --compare     # 两个变体 × 1024 行，并与 metrics.json 对比
python code/eval_dev.py --ckpt checkpoints/e6 --rows 256
```

预期（容差 5e-4）：

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

协议：取 `data/dev/dev_ids.npy` 中第二个 token 为 `<|FORWARD|>` 的前 1024 行，读 `mask_start − 1`
位置的 logits，对 `mask_start` 处的 token 打分。**不要拿它跟训练器打印的 dev 数字比**——后者按长度
分桶重排过，不是同一批样本。

## 3. miniF2F 端到端搜索（需要 Lean + mathlib）

### 3.1 前置条件

* **Lean 4.35.0-rc2** 工具链（例如 `elan toolchain install leanprover/lean4:v4.35.0-rc2`）。
  注意这是 release candidate；换 Lean 版本后 mathlib 的展开方式与状态文本都会变。
* **带预编译 `.lake` 缓存的 mathlib4 检出**（本项目用 2026-09 的快照；发布包里没有钉死 commit，
  所以换 revision 时状态文本可能有轻微漂移）。在检出目录里执行 `lake exe cache get` 拿 olean 缓存——
  本地全量编译要数小时，缓存只要几分钟、约 7 GB。
* 用 `--lean-parallel 6` 时建议 ≥16 GB 内存（每个 `lean --json` 进程都要加载 mathlib；
  实测单候选 0.4 s、6 路并行后 0.034 s/候选）。

```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          # 自检
```

### 3.2 复现公开成绩的那条命令

```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
```

预期：**30/89 = 33.7%**，RTX 4060 Laptop 上约 52 分钟（换成 `e6` 变体也是同样 30 题，约 60 分钟）。
全量 `valid` 已用这份完全相同的配置跑完：**85/244 = 34.8%**，约 2.3 小时（分段 33.7% / 40.4% / 28.8%；
85 条解出里 78 条只有一条 tactic）。想再快就动两处：每次 `lean --json` 调用的固定成本约 **6.6 s**
的 `import Mathlib`（而每条候选只要约 0.03 s），所以墙钟全花在并行度和导入裁剪上。

各参数的含义——成绩其实来自这里：

| 参数 | 含义 |
|---|---|
| `--k 16` | 每个状态提 16 条候选（白名单内 top-16 首 token + 贪心续写） |
| `--beam 4` | 每轮扩展 4 个开放状态 |
| `--depth 6` | 证明长度上限（以 tactic 计）。实测：30 条解出里有 25 条是 depth 1 |
| `--budget 45` | 每题墙钟预算 45 秒；`--round-budget 30` 限制单轮 |
| `--force --force-set v2` | 在每一层注入导出的自动化表（`rfl`、`ring`、`simp_all`、`omega`、…、`simp_all ; ring`、`gcongr`）。**这是最大的杠杆**：带它前 89 题是 30/89；不带它的全量 244 题只有 8/244 |
| `--lean-parallel 6` | 6 路并发验证候选（纯工程收益：墙钟 2.07×） |
| `--narrow-imports` | 每题把全量 Mathlib 导入换成 `#min_imports` + `Mathlib.Tactic`（实测每次 `lean --json` 从 3.41 s 降到 1.74 s）。命中「未知标识符/tactic」的候选会自动用全量导入重验，所以窄导入**不可能丢证明**（已验：85/85 条已验证证明仍可编译） |
| `--no-model` | 对照开关：只验证注入表、不提模型候选。在 valid 前 10 题上它与带模型的结果完全一致（2/10、同题、同证明项），而墙钟减半 |

引用任何通过率之前，请先读 `README.zh.md` 的「**这个成绩是怎么来的**」：这些是**系统**成绩
（注入的自动化表 + 搜索 + 内核验证），随包模型的贡献是 0 条。

### 3.3 看结果与续跑

结果按行追加到 `reports/search_eval_valid_mine.jsonl`（每个题目一个 JSON：`solved`、`depth`、
`seconds`、`verified`、`proof`、`confirmed`、`reason`），同时实时打印累计进度与 ETA。因为是追加写入，
中断后用 `--start <已写入行数>` 续跑即可，或者直接重跑同一条命令。

### 3.4 疑难排查

* 某题报 `initial-state-failed`：它的陈述在你的 mathlib revision 上根本编译不过。有 2 道 miniF2F
  题对所有人都不通过（`mathd_numbertheory_711`、`imosl_2007_algebra_p6`）。
* 报 `No such file or directory: .../bin/lean`：设 `LEANOAR_LEAN_BIN`。
* Lean 报缺 olean / `unknown module prefix 'Mathlib'`：把 `LEANOAR_MATHLIB` 指向**已编译**
  （`.lake/build/lib/lean` 与 `.lake/packages/*` 齐备）的检出目录，验证器会据此拼 `LEAN_PATH`。
* `verified` 数特别低：确认首 token 白名单生效、切词器用的是 `tokenizer_v1.json`。
* 旧版本在超长状态上会让上下文溢出 1 个 token；本包内的 `search.py` 已按
  `ctx − 4 − max_new_tokens` 计算预算并在 `ctx` 处硬停。如果你改采样器，请保持这个不变式。

## 4. 扩展

* 换自己的权重：把 `lit_model.pth`（和 `model.safetensors`）放进一个目录，给
  `generate.py` / `eval_dev.py` / `eval_minif2f.py` 传 `--ckpt <目录>`。`config.json` 必须与架构一致；
  词表与 ctx 是固定的。
* 往 `code/eval_minif2f.py` 的 `FORCE_SETS` 里加自动化 tactic——本项目所有实测收益几乎都来自这张表
  与搜索/验证器侧，而不是模型。
* Value 头虽然随包发出但不可用（AUC 0.5201，低于策略自身置信度）。不要拿它做重排。
* `code/leanoar/data.py` 只是因为搜索代码要用里面的 `load_specials` 才包含进来；训练流水线不在本包内。