使用说明（中文）

本包是 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. 安装与验证

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：

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

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

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

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 报错里抠出来。在自己的代码里调用：

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 指标

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/候选）。

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 复现公开成绩的那条命令

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 才包含进来；训练流水线不在本包内。