Views
No views yet
Qwen/Qwen2.5-0.5B-Instruct fine-tuned directly on the ProofKit SFT set
(visproj/proofkit-sft,
~7,000 synthetic examples). LoRA-trained, then merged to standalone weights. This is
the in-Space Transformers option in ProofKit (runs on ZeroGPU / a small
GPU; loads lazily on first generation).1from transformers import AutoModelForCausalLM, AutoTokenizer
2import torch
3
4m = "visproj/proofkit-qwen0.5b-7k"
5tok = AutoTokenizer.from_pretrained("Qwen/Qwen2.5-0.5B-Instruct") # carries the chat template
6model = AutoModelForCausalLM.from_pretrained(m, torch_dtype=torch.float16).to("cuda").eval()
7
8# NOTE: prompt it with ProofKit's trained prompt_formats.py shapes — see below.
9messages = [{"role": "system", "content": SYSTEM}, {"role": "user", "content": PROMPT}]
10text = tok.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
11ids = tok(text, return_tensors="pt").to("cuda")
12out = model.generate(**ids, max_new_tokens=600, do_sample=True, temperature=0.3, top_p=0.9)
13print(tok.decode(out[0][ids["input_ids"].shape[-1]:], skip_special_tokens=True))gpt-oss experts is a deliberately un-retrained stale control):| model | Claude | GPT-5.5 | Qwen-3B | Avg |
|---|---|---|---|---|
| gpt-5.5 (frontier ceiling) | 94.6 | 95.6 | 90.8 | 93.7 |
| gpt-oss attn (retrained teacher) | 82.0 | 66.8 | 81.4 | 76.7 |
| qwen-0.5b distilled (served) | 79.0 | 68.6 | 82.2 | 76.6 |
| qwen-0.5b direct 7k (served) | 78.6 | 64.4 | 82.0 | 75.0 |
| gpt-oss experts (stale control) | 67.6 | 68.6 | 81.8 | 72.7 |
| qwen-3b base | 62.1 | 67.1 | 80.5 | 69.9 |
| gpt-oss base | 55.4 | 53.8 | 68.2 | 59.1 |
| qwen-0.5b base | 36.5 | 44.5 | 67.9 | 49.7 |
| Repo | What it is |
|---|---|
visproj/proofkit-qwen0.5b-7k | Qwen2.5-0.5B fine-tuned directly on the 7k set (Transformers) |
visproj/proofkit-gpt-oss-20b-lora | gpt-oss-20b LoRA — the distillation teacher |
visproj/proofkit-distilled-qwen0.5b | Qwen2.5-0.5B distilled from the teacher (merged) |
visproj/proofkit-distilled-qwen0.5b-gguf | GGUF of the distilled student (llama.cpp — served) |
visproj/proofkit-sft | SFT dataset (synthetic, license-safe) |
visproj/proofkit-distill-qwen0.5b | Distillation dataset (teacher completions) |
target = template instead of target = f(input). The fix — faithfulness anchors
(a distinctive token shared by the answer and the target) + seeded per-example
variation across every task, then a full-chain retrain — is what these current
weights reflect.prompt_formats.py. They only behave well when prompted in that format; reworded or
free-form prompts push them off-distribution. They are purpose-built components of the
ProofKit app, not general chat models.