GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
vignesh-trustt
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Model Details
Model Provider
vignesh-trustt
Model Tree
Goedel-LM/Goedel-Prover-V2-8B
Input Modalities
Output Modalities
Supported Functionality
This adapter is a plumbing probe, not an improved prover. It records one CISPO optimizer step on top of
Goedel-LM/Goedel-Prover-V2-8B (LoRA r64, alpha 128, all attention and MLP projections). The step used 64 rollouts
(8 train-split Goedel-Pset problems x 8 samples, cap 16384 tokens), each verified by a frozen Lean 4 checker (v4.9.0-rc1,
Mathlib d1d1e4b7).
The probe confirmed:
Full numbers are in probe_result.json. Evaluation: none. Do not use it as a better model than the base. No miniF2F test
statement was used for generation or training.
Usage: PeftModel.from_pretrained(AutoModelForCausalLM.from_pretrained("Goedel-LM/Goedel-Prover-V2-8B"), "<this repo>").