EPFL-LARA/lean-encoder-modernbert-large

Text Classification • 0.4B • Updated 2 days ago • 25

Note Encoder: ModernBERT-large (395M). Predicts Lean program validity in one forward pass.

EPFL-LARA/lean-one-token-qwen3-8b

Text Classification • 8B • Updated 2 days ago • 34

Note One-token: Qwen3-8B. Scores validity using the true/false next-token logits, without generating text.

EPFL-LARA/lean-feedback-qwen3-4b

Text Generation • 4B • Updated 2 days ago • 820

Note Feedback: Qwen3-4B. Generates annotated feedback traces; validity is derived from feedback parsing and generation stop conditions.

Note Training corpus: 4,836,380 compiler-labelled Lean programs with reference feedback, using Lean v4.15.0.

Note Evaluation benchmark: 68,932 candidate programs from three public provers on miniF2F and ProofNet.