| # Kimina-Prover-Distill-8B as the Phase-1 base (lane T, 2026-10-14) |
|
|
| `AI-MO/Kimina-Prover-Distill-8B` is the K1/K2/K6 base in `docs/SOTA_PLAN.md` section 3. This note records what was |
| verified on CPU, and where its prompt and output conventions differ from Goedel-Prover-V2-8B, the model the P2 |
| harness (`extras/vllm_rollout/lean_prompts.py`, `lean_gen.py`) was built and fidelity-tested against. |
|
|
| ## Snapshot |
|
|
| * Location: `HF_HOME=/apps/development/rlhf/hf_cache`, |
| `hub/models--AI-MO--Kimina-Prover-Distill-8B/snapshots/74d328a7b1f001ab4871812582fc66d9bf70c68b` (16 GB, 4 bf16 shards). |
| * Downloaded with `HF_HUB_DISABLE_XET=1`, 2 workers, `nice -n 10 ionice -c3`. `/apps` had 224 GB free before, 206 GB after. |
| * Model card: `base_model: Qwen/Qwen3-8B`, Apache-2.0, a distillation of Kimina-Prover-72B (RL-trained). The card reports |
| 77.86% pass@32 on miniF2F-test. That is the authors' number: the card does not state the token cap or the verifier, so it is |
| not comparable to anything we measure until we reproduce it in our harness (plan section 1, Phase 1 anchor). |
|
|
| ## Loader compatibility (CPU, header-only; no weights loaded) |
|
|
| `scripts/p2/check_qwen3_snapshot.py <snapshot>` (new; tested on a fake snapshot in `tests/test_check_qwen3_snapshot.py`): |
|
|
| | check | result | |
| |---|---| |
| | `read_qwen3_config` (refuses sliding window, scaled RoPE, biases, tied head, non-silu) | parses; 36 layers, hidden 4096, ffn 12288, 32 Q / 8 KV heads, head_dim 128, vocab 151936, rope_theta 1e6, rms_eps 1e-6, max_pos 40960, untied head | |
| | index `weight_map` keys vs `hf_to_align` key table | 399 = 399, no missing, no extra | |
| | shard headers vs index; extents fit the file size (truncation check) | 399 tensors, all in the shard the index names, 4/4 shards complete | |
| | every tensor shape vs the shape the config implies | all match | |
| | dtypes | 399 x BF16 | |
|
|
| `config.json` differs from Goedel's in `transformers_version` only (4.52.4 vs 4.51.3). The architecture block is identical, so |
| `configs/p2_sft.toml`'s `[model]` numbers (`n_params = 8_190_735_360`, LoRA targets, memory envelope) apply unchanged and |
| `qwen3_stage` should accept it. NOT done here (GPU): the `scripts/qwen3_parity.py` logit-parity gate against HF on this |
| checkpoint. Run it once before the first Kimina training job. |
|
|
| ## Tokenizer: identical to Goedel's |
|
|
| `tokenizer.json`, `vocab.json`, `merges.txt`, `added_tokens.json` and `special_tokens_map.json` are byte-identical to Goedel's; |
| `tokenizer_config.json` is equal as parsed JSON (file bytes differ only in key order / whitespace), including the **chat |
| template** (4168 characters, the stock Qwen3 template). EOS/pad are the same: `eos_token = <|im_end|>` (151645), generation EOS |
| `[151645, 151643]`, `pad = <|endoftext|>` (151643), `add_bos_token = false`. `generation_config.json` also matches |
| (temperature 0.6, top_p 0.95, top_k 20). So token ids, the `ids` fidelity check and the SFT collator's `pad_token_id = 151643` |
| need no change. |
|
|
| ## What differs: the prompt and the output convention |
|
|
| Same tokenizer and template, different *content*. The template is applied by `apply_chat_template(..., add_generation_prompt=True)` |
| with `enable_thinking` unset, which ends the prompt at `<|im_start|>assistant\n` (no `<think>` prefill) for both models. |
|
|
| | | Goedel-Prover-V2-8B (what `lean_prompts.py` ports byte-for-byte) | Kimina-Prover-Distill-8B (model card) | |
| |---|---|---| |
| | system message | none (user turn only) | `You are an expert in mathematics and Lean 4.` | |
| | user text | `Complete the following Lean 4 code:\n\n```lean4\n{stmt}```\n\nBefore producing the Lean 4 code ... provide a detailed proof plan ...` | `Think about and solve the following problem step by step in Lean 4.\n# Problem:{informal}\n# Formal statement:\n```lean4\n{stmt}\n```\n` | |
| | informal problem text | not in the prompt | in the prompt (`# Problem:`); also repeated as a `/-- ... -/` docstring on the theorem | |
| | statement shown | `...:= by sorry` (everything after the first `:= by` replaced by ` sorry`) | `...:= by` followed by a newline (open goal, no `sorry`) | |
| | header in the statement | `import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n` (blank lines, `GOEDEL_HEADER`) | same four lines without the blank lines, then the docstring and the theorem | |
| | model output | plan prose, then a ```lean4 block | a `<think> ... </think>` block, then the final ```lean4 block with the complete proof | |
| | card's sampling | (harness) temperature 1.0, top_p 0.95, top_k 0 | temperature 0.6, top_p 0.95, `max_tokens` 8096 in the example (top_k 20 in generation_config) | |
| | repair prompt | Goedel's "The proof (Round k) is not correct ... `<error></error>` ..." template | none published; the card points to the Kimina-Prover-Preview demo repo, not read here | |
|
|
| ## Consequences for the harness (not done in this lane; files are frozen or other lanes') |
|
|
| 1. `extras/vllm_rollout/lean_prompts.py` (`initial_prompt`, `correction_prompt`, `goedel_statement`) is Goedel-only. A Kimina run |
| needs a prompt style that builds the system+user messages above from the problem record's `informal_prefix` and |
| `formal_statement`. This changes the policy conditioning, so the byte-fidelity gate (`lean_prompts.py fidelity`) cannot certify |
| it: a Kimina fidelity check needs the reference demo's own prompt builder. Lane V2 owns that directory. |
| 2. Answer extraction (`extrac_code`: last ```lean4 fence plus import head, then `problem_check` re-inserts the original statement) |
| works on both output shapes in principle, because both end with a fenced block. With Kimina the `<think>` text can contain |
| ```lean4 fences of its own; "last fence wins" still picks the final answer, but a response truncated inside `<think>` yields a |
| draft fence from the reasoning, not a proof. Check the `length`-finish rows when the first Kimina samples exist. |
| 3. `build_sft_data.py`'s statement-fidelity filter compares the theorem the completion displays with the problem statement. It was |
| written against Goedel-shaped answers; run it on a handful of real Kimina samples before trusting its drop counts. |
| 4. Sampling: `lean_gen.py` hard-codes temperature 1.0 / top_p 0.95 (`TEMPERATURE`, `TOP_P`). The card recommends 0.6. The Kimina |
| anchor must state which it uses (plan: every number carries the protocol tuple). K2's T = 1.2 control needs a `--temperature` |
| flag that does not exist yet; `scripts/p2/contrasts.py` lists it as a pending prerequisite and refuses to run K2 without it. |
| 5. Cap: Kimina's own example uses 8k tokens; Goedel's published protocol is 32k and ours is `--cap-tokens 30000..40960`. Thinking |
| length under Kimina is unmeasured here: set `--mean-completion-tokens` for the K-contrast budget arithmetic from the anchor run, |
| not from this note. |
|
|
