Qwen3.5-2B-FineProof-RL

Qwen3.5-2B, trained with RL from the base model (no SFT) to write olympiad proofs. The reward is QED-Nano's: gpt-oss-20b grades each proof 0–7 against the problem's own marking scheme. Training ran through FineProofEnvs, which serves those problems and that judge as Harbor tasks, with TRL's AsyncGRPO and OpenEnv's Harbor integration.

Held-out eval: 64 problems × 4 attempts	Qwen3.5-2B	this model	change, paired by problem
mean rubric score, gpt-oss-20b (the training judge)	0.217	0.407	+0.190 ± 0.030
mean rubric score, gpt-oss-120b regrade, high effort	0.259	0.464	+0.204 ± 0.034
attempts with full marks (7/7)	12.1%	25.4%
problems with a full-marks attempt (pass@4)	26.6%	40.6%

• The eval set: the 64 FineProofs-RL-test problems whose reference proof gpt-oss-120b scores at least 6/7. None of the test problems is in the training data.
• The comparison: 47 problems improved and 6 got worse.
• The checkpoint: this is the last one (update 500), not the best, so choosing it never looked at the eval.
• Cut-off proofs: the eval keeps the judge's partial credit for a proof cut off at 32,768 tokens. Scored as training scores it (0), the model gets 0.395 and the gain is +0.179 ± 0.027.

Reading the proofs shows the model finds key steps the base model missed. Both judges, though, forgive contradictions left around a correct argument, so the absolute scores run high. See Limitations.

• Training logs: Trackio dashboard.
• Every eval attempt, with its proof and grades: FineEnvs/fineproof-rl-runs.
• Code, recipe and full results: FineEnvs on GitHub.

Use it

The chat template has thinking turned off, as in training: the model writes its proof directly. Serve it with vLLM and give it the prompt it was trained on:

vllm serve FineEnvs/Qwen3.5-2B-FineProof-RL --max-model-len 40960

from openai import OpenAI

client = OpenAI(base_url="http://localhost:8000/v1", api_key="-")
problem = "Let $a, b, c$ be positive reals with $abc = 1$. Prove that $a + b + c \\ge 3$."
messages = [
    {"role": "system", "content": "You are solving an olympiad problem by writing a proof. There are no tools: reply "
     "in Markdown, with LaTeX for formulas. Your proof is read by a strict grader who gives credit only for steps "
     "that are fully justified."},
    {"role": "user", "content": f"Prove the following olympiad problem.\n\n## Problem\n\n{problem}\n\n"
     "## What to submit\n\nWrite a complete, rigorous proof in plain language (Markdown, with LaTeX for formulas). "
     "If the problem asks for a value or a set of values, state it and prove it. Prove every claim you rely on; a "
     "result you cite counts only if it is a standard named theorem."},
]
reply = client.chat.completions.create(model="FineEnvs/Qwen3.5-2B-FineProof-RL", messages=messages,
                                       temperature=0.8, max_tokens=32768)
print(reply.choices[0].message.content)

Training and evaluation sampled at temperature 0.8 with up to 32,768 output tokens. The exact training prompt also mentions the harness's /workspace/proof.md. The task files have it word for word.

Training

Base model	Qwen/Qwen3.5-2B, non-thinking mode
Data	1,024 FineProofs-RL problems, sampled from the 1,066 on which QED-Nano's base model averaged 0.5–0.9
Reward	gpt-oss-20b rubric score / 7, mean of 2 grades; a proof cut off at 32,768 tokens scores 0
Algorithm	AsyncGRPO (TRL), 500 updates of 128 rollouts (8 problems × 16)
Objective	advantage = reward − group mean (no std division); token losses summed and divided by 32,768, as in QED-Nano and Dr. GRPO
Optimizer	AdamW 8-bit, learning rate 1e-6, 10 warm-up updates, fp32 master weights
Hardware	one h200x4 HF Job, 28 hours of training (about $580 of GPU time), plus $241 of judge calls

The weights are published in bf16 (training kept fp32 master weights). The full recipe, the eval curve over 14 checkpoints, the 120b regrades and what failed first are in RESULTS.md.

Limitations

• The judge is the target. Training and the headline eval both use gpt-oss judges. A hand audit of four 7/7 proofs found the right key idea in all four, but two kept false statements or an unresolved contradiction that a careful grader would mark down to about 4/7.
• Scratch work in the answer. In non-thinking mode the model often works through the problem in the reply before its final proof, and wraps the proof in a Markdown block.
• Narrow scope. English olympiad proofs only; not evaluated on IMO-ProofBench or other domains. It is not a verified prover: check every proof.
• Small eval. 64 problems, one training run, standard errors of about 0.03.

Credits

Problems, marking schemes and the judge prompt are from the QED-Nano release by the LM-Provers team (CMU, Hugging Face, ETH Zurich, Numina), Apache-2.0. The base model is Qwen3.5-2B by the Qwen team.