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

Qwen3.5-9B equational-theory SAIR R0–R3 — 1M 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 1M nested mixture: 699,261 note tokens and 300,166 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

SAIR evaluation is being launched: 800 Stage 1 questions and 300 Stage 2 questions, four independently seeded responses per question. Stage 2 uses Lean input and natural-language proof/counterexample output, graded by GPT-5.6-sol (high). No final mathematical performance result is available yet. Training/validation cross-entropy is not a proof-accuracy score. GPT judgments are not Lean certification.

Load and generate

from transformers import AutoTokenizer, Qwen3_5ForConditionalGeneration

repo = "violetxi/qwen35-9b-equational-theory-sair-r3-mix1m"
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-mix1m --dtype bfloat16 --reasoning-parser qwen3