GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
EPFL-LARA
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Run this model inference with full control and performance in your environment.
Model Details
Model Provider
EPFL-LARA
Model Tree
formalmathatepfl/qwen3-cpt
Input Modalities
Output Modalities
Supported Functionality
bash
pip install torch 'transformers==4.57.3' acceleratehf download EPFL-LARA/lean-one-token-qwen3-8b predict.py lean_validity_one_token.py --local-dir lean-one-tokenpython lean-one-token/predict.py Example.leanThe runner accepts Lean files or standard input and returns is_valid,
probability_true, probability_false, and truncation information as JSON.
The reference runner includes the exact training instruction wrapper ending in
VERDICT=. It uses AutoModelForCausalLM, plain tokenization with
add_special_tokens=False, left padding, and logits_to_keep=1.
Validity is a softmax over the two label logits: true (1866) and false
(3849). Scoring requires one forward pass, with no text generation.
The 32,768-token context uses the supplied make_bounded_prompt helper to
preserve the prompt wrapper and retain 25% of the beginning and 75% of the end
of long source programs. The runner uses a 0.5 decision threshold; use
probability_true >= 0.86 for the calibrated setting below.
Paper results on the 68,932-program evaluation benchmark, using Lean v4.15.0 labels from public-prover candidates on miniF2F and ProofNet:
| Decision threshold | Accuracy | Macro F1 | MCC | AUROC |
|---|---|---|---|---|
| Default: 0.5 | 75.2% | 0.752 | 0.592 | 0.905 |
| Calibrated: 0.86 | 83.1% | 0.831 | 0.683 | 0.905 |
The calibrated threshold was selected on separate in-house validation data. The paper measures 4.9 candidates/s on one H100 as batch throughput.
Pair this model with the Feedback model to form the paper's cascade: the one-token gate screens candidates at 0.5, then the feedback stage scores its positive predictions. The greedy cascade reaches 87.8% accuracy.
Qwen3-8B receives Lean continued pretraining, followed by one supervised epoch
on source_code → isValid pairs from the
compiler-labelled training corpus.
Each example supervises one lowercase true or false token.
Part of Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs.
pip install torch 'transformers==4.57.3' acceleratehf download EPFL-LARA/lean-one-token-qwen3-8b predict.py lean_validity_one_token.py --local-dir lean-one-tokenpython lean-one-token/predict.py Example.lean