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')

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