GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
budget-internalization-iclr2027
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Model Details
Model Provider
budget-internalization-iclr2027
Model Tree
Qwen/Qwen3.5-4B
Input Modalities
Output Modalities
Supported Functionality
| Base model | Qwen/Qwen3.5-4B |
| Algorithm | GRPO (leave-one-out baseline, group reward normalization, token-level loss). |
Generation budget (max_new_tokens) | 4,096 |
| Data | Lean Workbook (Lean 4 formal statements), 5 epochs max |
| Batch | 32 prompts × 8 rollouts per step |
| Optimizer | Adam, constant LR schedule, LR 1e-06, 10 warmup steps |
| Steps | 70 |
| Reward | proof accepted by the Lean 4 checker |
| Weights dtype | BF16 |
Prompts are the Lean Workbook formal theorem proving task prompts, rendered with the base model's chat template.
python
from transformers import AutoModelForCausalLM, AutoTokenizer repo = "budget-internalization-iclr2027/qwen3.5-4b-4k-grpo-lean-boldthrush-s70"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-4k-grpo-lean-boldthrush-s70
Inherits the license of the base model (Qwen/Qwen3.5-4B).