CoolFace
Modelpublic

budget-internalization-iclr2027/qwen3.5-4b-2k-grpo-lean-upwardgull-s50

sourceHugging Faceapache-2.0updated 2d agoView on Hugging Face
0likes12downloads
Model Card

Qwen3.5-4B · 2k-token budget · grpo-lean · upwardgull

RL-finetuned Qwen/Qwen3.5-4B trained with GRPO on Lean Workbook formal theorem proving under a 2,048-token generation budget. Released as part of an anonymous ICLR 2027 submission.

Run ID (petname): `upwardgull` · checkpoint step 50

Training

Base modelQwen/Qwen3.5-4B
AlgorithmGRPO (leave-one-out baseline, group reward normalization, token-level loss).
Generation budget (max_new_tokens)2,048
DataLean Workbook (Lean 4 formal statements), 5 epochs max
Batch32 prompts × 8 rollouts per step
OptimizerAdam, constant LR schedule, LR 1e-06, 10 warmup steps
Steps50
Rewardproof accepted by the Lean 4 checker
Weights dtypeBF16

Prompts are the Lean Workbook formal theorem proving task prompts, rendered with the base model's chat template.

Usage

python
from transformers import AutoModelForCausalLM, AutoTokenizer

repo = "budget-internalization-iclr2027/qwen3.5-4b-2k-grpo-lean-upwardgull-s50"
tok = AutoTokenizer.from_pretrained(repo)
model = AutoModelForCausalLM.from_pretrained(repo, torch_dtype="auto", device_map="auto")

With vLLM: vllm serve budget-internalization-iclr2027/qwen3.5-4b-2k-grpo-lean-upwardgull-s50

License

Inherits the license of the base model (Qwen/Qwen3.5-4B).