| # 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|>`), no BOS, EOS `<|im_end|>`; tokenizer and template byte-identical to the 8B's (3.2) | DeepSeek-V3 style: text starts with `bos_token` (`<｜begin▁of▁sentence｜>`, id 100000) + system, then `<｜User｜>{user}<｜Assistant｜>`; `add_bos_token = true`; EOS `<｜end▁of▁sentence｜>` (100001) | |
| | 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. |
| |
