violetxi/qwen35-9b-equational-theory-sair-r3-mix30m

Qwen3.5-9B equational-theory SAIR R0–R3 — 30M mixture

Final epoch 2 checkpoint of a full-model SFT run. This is a complete BF16, sharded safetensors model in the native Qwen3_5ForConditionalGeneration layout, including configuration, tokenizer, chat template and processor files. No adapter merge, custom code, base-model download or checkpoint conversion is required. Use a Transformers/vLLM release with Qwen3.5 support. Standard model loading was verified with Transformers 5.13.0; the submitted evaluations use vLLM 0.19.1.

Training

• —Pinned base revision: c202236235762e1c871ad0ccb60c8ee5ba337b9a.
• —Latest live R3 notes plus curated single-turn R0–R3 note-conditioned trajectories.
• —Nominal 30M nested mixture: 20,961,111 note tokens and 9,000,144 assistant-answer tokens per epoch after loss masking.
• —Approximately 70% notes / 30% trajectories; two epochs, eight GH200 GPUs, LR 5e-6, cosine schedule, warmup 0.03, full supervised-token mean CE, no KL.
• —Padding-free packing isolates examples in full attention, linear attention and convolution. Prompts/assistant headers are masked. Notes are plain text. Separate generated thinking is excluded; assistant answers and template/end markers are supervised. The trajectory template therefore includes an empty thinking wrapper.
• —Repetition exclusions and frozen validation are retained. No correctness filter or blanket rejection of length-stopped answers was added.
• —Trained FP32 language weights were converted to BF16. All 427 language tensors, including the output head, were mapped into the native layout. Vision and MTP weights are inherited unchanged from the pinned base.
• —Online training log.

Evaluation

Completed SAIR evaluations use 800 Stage 1 questions and 300 Stage 2 questions, with four seeded responses per question at each output budget. These are per-response rates, not pass@4.

Stage 1 uses rule-based parsing and comparison of the binary verdict. Stage 2 uses GPT-5.6-sol (high) to judge the final natural-language proof/counterexample against Lean input; hidden thinking is excluded, and there are no trusted reference solutions in this evaluation set. Empty and uncertain answers count as non-successes. GPT judgments are not Lean certification.

Generation uses thinking, seeds 0–3, temperature 1.0, top-p 0.95, top-k 20, min-p 0, presence penalty 1.5, frequency penalty 0, repetition penalty 1.0, and a 32,768-token context. Output caps are 16,384 and 24,576 tokens including thinking; the two budgets use separate generations.

• —Public results and response explorer
• —Complete evaluation dataset (private; access required)

Load and generate

from transformers import AutoTokenizer, Qwen3_5ForConditionalGeneration

repo = "violetxi/qwen35-9b-equational-theory-sair-r3-mix30m"
tokenizer = AutoTokenizer.from_pretrained(repo)
model = Qwen3_5ForConditionalGeneration.from_pretrained(
    repo, dtype="auto", device_map="auto"
)
messages = [{"role": "user", "content": "Explain why associativity does not imply commutativity."}]
inputs = tokenizer.apply_chat_template(
    messages, tokenize=True, add_generation_prompt=True,
    enable_thinking=True, return_dict=True, return_tensors="pt"
).to(model.device)
output = model.generate(**inputs, max_new_tokens=1024)
print(tokenizer.decode(output[0, inputs["input_ids"].shape[1]:], skip_special_tokens=True))

vllm serve violetxi/qwen35-9b-equational-theory-sair-r3-mix30m --dtype bfloat16 --reasoning-parser qwen3