Hugging Face's logo

viai957
/
align

Text Generation
English
align
post-training
rlhf
sft
dpo
ppo
grpo
cispo
expert-iteration
lean4
theorem-proving
formal-verification
fsdp2
mixture-of-experts
code
Eval Results (legacy)
Model card Files
xet
 Community
align / code /docs /TEACHERS.md
viai957's picture
viai957
Add files using upload-large-folder tool
d909bd8 verified
preview code
|
Raw History Blame Contribute Delete
22 kB

Open Lean-prover teachers for distillation data (lane T2, 2026-10-19)

Goal: verified proofs from stronger open provers as one more SFT source for the Apache-2.0 research model (base: Goedel-Prover-V2-8B). Nothing here touched a GPU. All sizes/licenses are from the HF hub API and model cards read on 2026-10-19; every miniF2F number is the AUTHORS' number under their own verifier, token cap and sampling, so none is comparable to what we measure until reproduced in our harness (plan section 1).

1. Survey

model license (hub) bf16 size arch / Lean reported miniF2F-test verdict
Goedel-LM/Goedel-Prover-V2-32B Apache-2.0 65.5 GB, 14 shards Qwen3 dense, 64 L, 8 KV heads, ctx 40,960; Lean 4 + Mathlib, same stack as the 8B 88.0% pass@32 (90.4% with self-correction); PutnamBench 43 @32 (57 with self-corr., 86 @192) best fitting teacher; downloaded
deepseek-ai/DeepSeek-Prover-V2-7B repo LICENSE is MIT (code), model card says DeepSeek Model License (use-based restrictions, see 1.1) 13.8 GB Llama, 30 L, 32 KV heads (MHA), YaRN x16 to 65,536 (card: 32K) not on the card (7B row is in the paper, arXiv 2504.21801; not re-read here, so unverified); 671B: 88.9% downloaded; training use blocked on license (1.1)
AI-MO/Kimina-Prover-72B MIT 145.4 GB Qwen2, 80 L, 8 KV heads, ctx 131k 84.0% pass@32 does not fit bf16; no open AWQ/GPTQ safetensors (only GGUF); weaker than Goedel-32B; skip
AI-MO/Kimina-Prover-Distill-8B (= Kimina-Prover-8B, same sha) Apache-2.0 16.4 GB Qwen3-8B 77.86% pass@32 already on disk (docs/KIMINA_BASE.md); same size and weaker than our base, not a teacher
Kimina-Prover-Distill-1.7B / 0.6B, Preview-Distill-7B / 1.5B Apache-2.0 4.1 / 1.5 / 15.2 / 3.6 GB Qwen3 / Qwen2.5-Math below the 8B too weak to teach an 8B
stepfun-ai/StepFun-Prover-Preview-32B / 7B Apache-2.0 65.5 / 15.2 GB Qwen2 (R1-distill base) 70.0% pass@1 (32B) multi-turn REPL loop (<sketch>/<REPL>), not whole-proof; incompatible with lean_gen; skip
ByteDance-Seed/BFS-Prover-V2-7B / 32B Apache-2.0 15.2 / 131.1 GB Qwen2.5 n/a here next-tactic model for tree search, no whole-proof output; skip
ByteDance-Seed/Seed-Prover not open (hub 401; paper/API only) - - - unavailable
mistralai/Leanstral-1.5-119B-A6B (and -2603) Apache-2.0 120.9 GB Mistral Small 4 MoE (119B total, ~6B active), agentic, ctx 256k not read does not fit bf16 on 92 GB; only NVFP4/GGUF/MLX community quants (Blackwell/Apple formats, untested on Ampere); agentic tool protocol, not whole-proof; separate lane
deepseek-ai/DeepSeek-Prover-V2-671B DeepSeek Model License 688.6 GB - 88.9% out of reach
Goedel-LM/Goedel-Prover-SFT MIT 13.8 GB DeepSeek-Prover-V1.5 base ~57% weaker than our base

Quantised open variants found by hub search (names containing awq/gptq/fp8/bnb/nvfp4): Goedel-V2-32B: only mlx-community/...-8bit (Apple); DeepSeek-Prover-V2-7B: athanor-ai/...-GPTQ-4bit, unsloth/...-bnb-4bit, NVFP4/...-FP4; Kimina-72B and Kimina-8B: none. None is needed: the two models we use fit in bf16 (section 2). Third-party quantised copies are not trusted as teachers anyway (unknown calibration, no license chain).

1.1 License finding (read before any DeepSeek output enters training)

The DeepSeek Model License (LICENSE-MODEL, the one the Prover-V2 card links) defines "Derivatives of the Model" to include "any other model which is created ... by transfer of patterns of the ... output of the Model ... including distillation methods ... or methods based on the generation of synthetic data by the Model for training the other model". Section 4 requires every derivative to carry the Attachment-A use-based restrictions as an enforceable term. An SFT model trained on DeepSeek-Prover-V2 proofs is therefore a Derivative that cannot be released under plain Apache-2.0. The hub repo's LICENSE file is MIT, which contradicts the card; the card + LICENSE-MODEL is the safer reading. Decision for the owner: either (a) do not train on DeepSeek-Prover-V2 outputs (default here), or (b) accept Attachment-A on the released weights. Using it for evaluation or as a baseline is unaffected. Goedel-V2-32B (Apache-2.0) and Kimina (MIT / Apache-2.0) carry no such clause. Apache-2.0 / MIT model cards do not mention an output-use clause; we record the hub license string and card revision per teacher anyway.

2. Feasibility on 4x A10G (22.5 GiB usable each, 90 GiB total, TP=4, PCIe + host-SHM NCCL)

Model: per-GPU weights = bytes/4; KV bytes/token (global) = layers x 2 x kv_heads x head_dim x 2; each GPU stores 1/4 of the heads. Per decode step each GPU reads its weight shard plus the live KV; step time = bytes / (eff x 600 GB/s). eff is calibrated on OUR 8B measurement: 256 seqs at cap 16k = 1,363 tok/s (docs/P2.md, P2-B), mean completion 4,996 tokens, mean live context about 5,000 gives eff = 0.46 (this folds in the NCCL cost). The model reproduces the 8B at 84 seqs as 1,171 tok/s (measured 1,043 end-to-end / 1,015 in the smoke). Overhead reserved per GPU: 2.0 GiB (CUDA context, activations, graphs, NCCL). These are ESTIMATES; the section 6 smoke replaces them.

Goedel-8B (ours, measured) Goedel-V2-32B bf16 same, util 0.94 same, fp8 KV (untested on A10G) DeepSeek-Prover-V2-7B bf16 same, fp8 KV
weights / GPU 3.8 GiB 15.3 GiB 15.3 15.3 3.2 GiB 3.2
KV bytes / token (global) 144 KiB 256 KiB 256 128 480 KiB (MHA) 240
KV room / GPU at util 0.90 14.4 GiB 3.0 GiB 3.9 (0.94) 3.0 15.0 GiB 15.0
KV capacity (tokens) 420k 49k 64k 98k 131k 263k
sequences at 16k / 32k (worst case) 25 / 13 3.0 / 1.5 3.9 / 1.9 6 / 3 8 / 4 16 / 8
sequences at mean live ctx 5k 84 9 12 19 26 52
est. tok/s 1,000-1,360 ~130 ~160 ~270 ~365 ~730
max_model_len it can start with 40,960 40,960 needs 2.5 GiB/GPU for one sequence: starts at 0.90, no headroom; use <= 33,000 32,768

Reading: bf16 weights of the 32B fit (61 GiB of 90) but leave only 3-4 GiB per GPU for KV, so the engine runs ~9-12 concurrent sequences, is KV-capacity-bound and runs at roughly 130-160 tok/s, 7-8x slower than the 8B. It is the only open model above our base that fits at all. The 7B teacher is not fast either: it is MHA (32 KV heads, 3.3x the KV per token of Qwen3-8B), so its KV room, not its weights, caps it at ~365 tok/s. Alternatives considered: TP=2 x 2 replicas for the 7B gives the same total capacity and doubles the engine count (no throughput gain, more load time); a 4-bit 32B (18 GB) would free ~10 GiB of KV per GPU and ~4x the concurrency, but no trustworthy open GPTQ/AWQ of Goedel-V2-32B exists and making one needs a calibration run and 65 GB scratch we do not have headroom for: not pursued. The cheapest lever is --kv-cache-dtype fp8 in vLLM (2x capacity); on Ampere it is storage-only fp8 with a slower attention path, so measure it in the smoke before trusting the ~270 tok/s. Prefix caching (already on) helps nothing here: prompts are short and unique.

3. What was downloaded

All via scripts/teachers/download_teacher.py (disk floor 60 GB enforced against hub-reported bytes BEFORE fetching; 2 workers, nice -n 10 ionice -c3, hostguard cap 2 cores / 8 GB, HF_HUB_DISABLE_XET=1), into HF_HOME=/apps/development/rlhf/hf_cache.

repo revision path size check
deepseek-ai/DeepSeek-Prover-V2-7B a8d9e14432b2e8dd9df2a4d4e70f1ba9bc8d9b7b hub/models--deepseek-ai--DeepSeek-Prover-V2-7B/snapshots/a8d9e144... 13.8 GB, 2 bf16 shards check_snapshot.py: 273/273 tensors, shapes match, shards complete, 273 x BF16
Goedel-LM/Goedel-Prover-V2-32B 851bf85d329b0f819e1a44db30e05d16e07d15c0 hub/models--Goedel-LM--Goedel-Prover-V2-32B/snapshots/851bf85d... 65.5 GB check_snapshot.py: 14/14 shards complete, 707/707 tensors present exactly once, every shape matches, 707 x BF16, all 25 files byte-size equal to the hub's; warning: the upstream model.safetensors.index.json assigns 657 of 707 tensors to the wrong shard (3.2)

Disk: 148 GB free before the 32B (166 GB at the start of the lane), 74 GB free after both (floor 60 GB; the disk is shared and other writers took ~10-15 GB during the 90 minutes, so re-check df -h /apps before any further download). Both downloads resumed cleanly after one ReadTimeout; no .incomplete blobs remain.

3.1 Verification tools

  • scripts/teachers/check_snapshot.py SNAPSHOT [--json] (new, stdlib only, header-only, tested in tests/test_teacher_check_snapshot.py): config architecture (Llama / Qwen2 / Qwen3 dense), index key set equals the key set the config implies, every shard exists, header extents equal the file size (truncation), tensor-in-index-shard, every shape, dtypes. It reports rope_scaling / sliding_window / tie_word_embeddings rather than refusing.
  • scripts/p2/check_qwen3_snapshot.py for the Qwen3-family 32B as well (it additionally proves the key set maps into align's loader). align does not need to LOAD the 32B (teacher use is vLLM generation only); the check is for completeness.

3.2 Findings on the 32B snapshot

  • Upstream index defect. All 707 tensors exist exactly once across the 14 shards and every shard header matches its file size, but model.safetensors.index.json (byte-identical to the hub's at this revision) names the wrong shard for 657 of them (e.g. model.embed_tokens.weight is in shard 1, the index says shard 3). vLLM and transformers read every shard listed in weight_map and are unaffected; scripts/p2/check_qwen3_snapshot.py reports NOT COMPATIBLE because align's loader keys on the index. Consequence: use the 32B ONLY through vLLM (as planned); if align ever needs to load it, regenerate the index from the shard headers (a 20-line script, no weight I/O) rather than patching the snapshot in place. check_snapshot.py --strict-index turns the mismatch into a failure.
  • Config: Qwen3ForCausalLM, 64 layers, hidden 5120, ffn 25600, 64 Q / 8 KV heads, head_dim 128, vocab 151,936, rope_theta 1e6, no rope scaling, max_position_embeddings 40,960, bf16, untied head.
  • Tokenizer: tokenizer.json, vocab.json, merges.txt, added_tokens.json, special_tokens_map.json, tokenizer_config.json (so the chat template) are byte-identical to Goedel-8B's: token ids and the prompt render are unchanged.
  • generation_config.json differs: 32B has only eos_token_id 151645, no sampling defaults; the 8B has temperature 0.6, top_k 20, top_p 0.95 and EOS [151645, 151643]. lean_gen passes temperature/top_p explicitly, but not top_k: do not let vLLM's generation_config="auto" supply different defaults per model (pass --generation-config vllm, or set top_k explicitly) so 8B and 32B samples come from the same sampler.

4. Prompt formats (record of what each teacher expects)

Goedel-Prover-V2-32B DeepSeek-Prover-V2-7B
chat template stock Qwen3 (`< im_start
user prompt the Goedel prompt, byte-identical to the 8B: Complete the following Lean 4 code:\n\n```lean4\n{stmt}```\n\nBefore producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.\nThe plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof. the same CoT prompt text, but the card's fence is {stmt}\n```` (a newline before the closing fence); Goedel's is {stmt}```` with none. The two are therefore NOT byte-identical: goedel format on DeepSeek is a one-newline deviation from the card, to be pinned and recorded (or add a deepseek format that inserts the newline; prefer that, 5 lines)
statement shown GOEDEL_HEADER + ...:= by sorry card example: import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n + optional /-- informal -/ docstring + theorem := by\n sorry (same header as GOEDEL_HEADER)
output plan prose, then a final ```lean4 block plan prose, then a final ```lean4 block
sampling (card / harness) temperature 1.0, top_p 0.95 (Goedel protocol; what lean_gen hard-codes by default) card gives none; use the same 1.0 / 0.95 for comparability
context 40,960 (Qwen3) config 65,536 (YaRN x16, orig 4,096), card says 32K: run with --max-model-len 32768, cap <= 30,000
repair prompt the Goedel round-k correction prompt works as for the 8B (model is the same family and trained for it; 90.4% "self-correction mode") none published; round 0 only

The Goedel format of extras/vllm_rollout/lean_prompts.py serves Goedel-32B exactly (same family, same template) and DeepSeek-7B up to the one-newline fence difference above. What is needed is in section 5.

5. Design note: changes for extras/vllm_rollout/ (another lane's files; NOT edited here)

  1. Double BOS for DeepSeek (correctness). lean_gen.prepare() does ids = list(tokenizer.encode(text)) (default add_special_tokens=True) on text produced by apply_chat_template(tokenize=False). For Qwen3 that is a no-op (no BOS). The DeepSeek template already prints bos_token, and encode would prepend a second BOS id 100000. Change: a bos_in_text = tokenizer.bos_token is not None and text.startswith(tokenizer.bos_token) test and tokenizer.encode(text, add_special_tokens=not bos_in_text); apply the same expression in run_fidelity's id check and in prompt_render_sha (so the sha pins the ids actually sent). Note lean_gen sends prompt_token_ids, not text, so vLLM adds nothing itself. Without this fix DeepSeek-7B generates with a doubled BOS: a silent quality loss, not an error.

  2. Teacher provenance in every record (needed for the license ledger, section 7). build_record(..., extra=...) already takes extra: add --teacher-id (hub repo), --teacher-license (hub string) and --teacher-card-rev; write {"teacher": {"repo", "revision", "license", "role": "teacher"}} into each record and into write_manifest. model_rev_of already supplies the snapshot sha. Make resume_conflicts refuse to resume a file under a different teacher id.

  3. Engine flags for the 32B, as CLI options passed through to LLM(...) (today LLM(...) is called with a fixed kwarg set): --kv-cache-dtype {auto,fp8} (default auto), --enable-chunked-prefill (leave vLLM default), and a default --max-num-seqs 16 for the 32B (128 is the 8B default; with room for ~12 sequences a larger value only grows the preemption/recompute churn). --gpu-mem-util 0.94 is worth one smoke try, with the NVML guard the lane already has.

  4. --max-model-len: default 40,960 is right for Goedel-32B (Qwen3 limit) and wrong for DeepSeek-7B (use 32,768). The existing check "max_model_len above the model's position limit raises" must read max_position_embeddings=65536 yet the card limit is 32K: add an explicit --max-model-len 32768 in the launch command rather than trusting the config.

  5. No change to extraction (extrac_code, last ```lean4 fence), lean_code_for_record, problem_check or the sampling defaults: both teachers answer in the Goedel output shape. The kimina format and kimina_final_answer are irrelevant here.

  6. Cap: use --cap-tokens 16384 for the first pass. Goedel reports their protocol at 32k; at cap 16k the 8B hit the cap in 8.2% of miniF2F samples and the hard band will be higher (assume ~35%). Rejected-by-cap samples are not proofs and cost the most, so a second pass at 32k only on never-solved statements (section 6).

  7. Sampler parity: pass generation_config="vllm" to LLM(...) (or explicit top_k) so a model's own generation_config.json (3.2) cannot change the sampler.

6. Plan: what each teacher attempts

Definitions (from the Phase-0a supply audit, scripts/p2/supply/): the band is every pool statement that passed the elaboration check and the misformalisation screen, with a profile of OUR 8B at n = 16-32.

  • Marginal band M: 8B pass rate in (0, 0.25]. Real proofs exist, the 8B finds them rarely; a stronger teacher's proofs add style and a higher hit-rate signal. Highest expected yield per token.
  • Never-solved band N: 0 / 32 for the 8B, and not flagged misformalised (Goedel: >80% of unsolved Pset statements were misformalised; a teacher "proof" of a vacuous or wrong-statement theorem is worthless, so the screen comes first).
stage teacher statements n cap rate (est.) mean tokens box-h expected yield
T0 smoke / calibration Goedel-32B 64 from M, round 0 2 16,384 measure measure ~1.5 (incl. load ~4 min) replaces every rate in this note
T1 marginal Goedel-32B M (B_M, expect a few hundred) 4 16,384 ~145 tok/s ~8,000 B_M x 4 x 8,000 / 145 / 3600: B_M=300: 18 h; 500: 31 h high: expect pass@4 of 30-60% on M
T2 never-solved Goedel-32B N screened (B_N) 8 16,384 ~145 tok/s ~11,000 B_N=300: 51 h; 500: 84 h low: single-digit % of N; each proof is a new problem
T3 correction round Goedel-32B, Goedel correction prompt N statements with failures that have compile errors (feedback present) 1 per failed parent 16,384 ~145 ~9,000 ~25% of T2 adds the "self-correction" lift (88.0 to 90.4 on miniF2F, a reported figure)
T4 (optional, license-gated) DeepSeek-Prover-V2-7B M + N 4 16,384 ~365 tok/s ~7,000 B=800: 15 h different proof style; only if 1.1 is resolved

Budget rule of thumb: the 32B costs 7 box-h per 1M generated tokens (145 tok/s), so the SFT-worth of T2 must be weighed against the SOTA_PLAN line items (Phase 1 ~200 box-h). Recommended: T0 then T1 (≈20-30 box-h), then T2 only on the screened subset of N with a prior (e.g. classifier score) and B_N <= 200 (35 h), stop early with the lane's early-stop when yield per box-h drops below the 8B's own self-distillation yield. All stages run strictly serially with the 8B generation (hostguard lock: never two heavy jobs), and stage-checkpoint at every lean_gen flush (the writer already flushes every 8 records).

Throughput honesty: 130-160 tok/s is the model's estimate with eff calibrated on the 8B. Two unmeasured risks: (a) NCCL all-reduce at 128 per step with only ~10 sequences is latency-bound and may be worse than eff 0.46 suggests (could be 100 tok/s); (b) fp8-KV on Ampere may be slower or unsupported. T0 resolves both. If T0 reads below ~100 tok/s, T1 halves (B_M x n = 600 samples) and T2 is dropped.

7. How teacher proofs enter training

  1. Verified only by OUR frozen verifier (docs/LEAN_VERIFIER.md, hash-pinned): the teacher's own claim of success, its own compile feedback, and any third-party verifier are ignored. The accepted set is exactly what verify_generations.py accepts at the frozen verifier hash (300 s, axiom walk, statement-fidelity check, problem_check re-insertion of the ORIGINAL statement).
  2. Decontaminated before training with the same pipeline as every other source (align.data.decontam, elaborated-statement hashing + MinHash + the base-model membership check): the PROBLEM must be absent from miniF2F valid/test, ProofNet, PutnamBench and every eval set; teacher output does not launder a contaminated statement. Teachers were trained on data we do not control (Goedel-V2 on its own Workbook/Pset; verify the Goedel-Pset overlap with the pool statement sha, not just by name). Proof text is also MinHash-checked against the eval proof sets (miniF2F solution zips) so a memorised published proof cannot enter.
  3. Provenance on every row: {source: "teacher", teacher_repo, teacher_revision, teacher_license, card_revision, prompt_format, temperature, top_p, cap, seed, verifier_hash, problem_ancestry}. build_sft_data.py gets a --source-tag so teacher rows are a separate, countable stream; per-problem cap (--max-per-problem 4) applies across self + teacher rows.
  4. Separate arm in the contrasts: teacher rows are added as their own SFT arm (self-only vs self+teacher, same token budget) so a gain is attributable and a loss is not hidden by the pooled mix. Same eval, same verifier, same seeds, matched row counts; the teacher stream is registered in the pre-registration BEFORE generation (docs/PREREG_SOTA.md) with its pass/fail gate (it must not lower self-distillation accepts/box-h).
  5. Licenses recorded and checked at release: docs/TEACHERS.md (this file) plus a machine-readable ledger teachers_ledger.json written by the lane from the record teacher blocks; the release script refuses a model whose training mix has a teacher with a non-permissive or unresolved license (DeepSeek until 1.1 is decided). Goedel-V2-32B is Apache-2.0 with no output clause: attribution only (NOTICE entry). Distillation from a model whose own base is Qwen3-32B (Apache-2.0) adds no further restriction.
  6. Selection: drop teacher proofs whose length exceeds the SFT sequence budget (16,384), those that hit statement-rewrite paths, and those that use sorry/axiom tricks (verifier already rejects). Keep at most 2 distinct proofs per problem from the teacher (diversity over volume), shortest-accepted-completion first as the 8B pipeline does.