Pradheep1647

qwen2.5-coder-1.5b-lean-language-sft

README

License: apache-2.0

Results

Evaluation uses the deterministic, section-stratified validation split from dataset revision 8ba4ea4. Both conditions use greedy decoding with a 256-token generation cap. Every generated answer is checked by Lean 4.31.0-rc2 with Mathlib through the official leanprover-community/repl backend.

Table with columns: Metric, Base model, SFT adapter, Change
Metric	Base model	SFT adapter	Change
Lean compilation	7/34 (20.6%)	26/34 (76.5%)	+55.9 pp
Section-topic contract	20/34 (58.8%)	33/34 (97.1%)	+38.3 pp
Compilation and topic contract	6/34 (17.6%)	25/34 (73.5%)	+55.9 pp
Validation loss	1.1739	0.1859	-84.2%
Validation perplexity	3.2345	1.2043	-62.8%

Held-out generation comparison

Compilation results by documentation section:

Table with columns: Section, Base model, SFT adapter
Section	Base model	SFT adapter
Additional Conveniences	1/3	1/3
Datatypes and Patterns	0/4	3/4
Evaluating Expressions	2/6	6/6
Functions and Definitions	1/6	4/6
Polymorphism	0/3	1/3
Structures	1/5

The adapter improved substantially on this split, but the section breakdown matters. Tuple and convenience syntax did not improve in compilation rate, and polymorphism remains weak. The eight remaining failures include type mismatches, missing type-class instances, invalid field projections, and an unknown identifier.

Training and validation loss

Training

Dataset: Pradheep1647/lean-language-docs-sft
Training examples: 285
Validation examples: 34
Split policy: deterministic per-section holdout with no duplicate code or source-scoped instruction
Objective: completion-only causal language modeling; prompt tokens are masked
LoRA: rank 16, alpha 32, dropout 0.05, all linear modules
Epochs: 4, with the epoch 2 checkpoint restored as best
Effective batch size: 8 (batch size 1, gradient accumulation 8)
Maximum sequence length: 1024 tokens; overlength rows are dropped, not truncated
Learning rate: 1e-4
Precision: BF16
Seed: 42

Validation loss reached 0.1921, 0.1859, 0.1971, and 0.2025 across epochs 1-4. The trainer restored epoch 2 because later epochs began to overfit.

The dataset contains novel, Lean-verified lessons grounded in seven introductory sections of Functional Programming in Lean. Proof content, unsafe constructs, disallowed imports, exact code duplicates, normalized instruction duplicates within each section, and verbatim source examples were filtered before training.

Usage

python
from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base_id = "Qwen/Qwen2.5-Coder-1.5B-Instruct"
adapter_id = "Pradheep1647/qwen2.5-coder-1.5b-lean-language-sft"

tokenizer = AutoTokenizer.from_pretrained(base_id)
model = AutoModelForCausalLM.from_pretrained(base_id, device_map="auto")
model = PeftModel.from_pretrained(model, adapter_id)

messages = [
    {
        "role": "system",
        "content": "You write concise Lean 4 code for language-learning exercises. Return only Lean code.",
    },
    {
        "role": "user",
        "content": "Define a function that doubles a natural number.",
    },
]
inputs = tokenizer.apply_chat_template(
    messages,
    add_generation_prompt=True,
    return_tensors="pt",
).to(model.device)
outputs = model.generate(inputs, max_new_tokens=256, do_sample=False)
print(tokenizer.decode(outputs[0, inputs.shape[-1]:], skip_special_tokens=True))

Generated Lean must still be checked with the same Lean and Mathlib toolchain used by the target project.

Artifacts

adapter_model.safetensors: LoRA adapter weights restored from the best checkpoint
training_metrics.json: baseline, training, and restored-best loss metrics
trainer_state.json: optimizer-step and epoch history
baseline_eval.json: base-model generations and Lean diagnostics
post_sft_eval.json: adapter generations and Lean diagnostics
evaluation_comparison.{png,svg}: before/after evaluation figure
training_dynamics.{png,svg}: training and validation loss figure

Limitations

This remains an exploratory adapter trained on 285 synthetic, documentation-grounded examples. The 34-example validation split is substantially better than the original six-example split but remains too small for broad claims. It covers introductory Lean language syntax rather than repository-scale code, Mathlib API recall, formal proof search, or verifier-guided repair. Use it as a syntax initialization experiment, not as a reliable Lean assistant.

The base model and this adapter are licensed under Apache 2.0. The source documentation used to ground the dataset is licensed CC BY 4.0.

Available on FriendliAI

Dedicated Endpoints

Run this model inference on single tenant GPU with unmatched speed and reliability at scale.

Learn more

Container

Run this model inference with full control and performance in your environment.

Learn more

Model Details

Model Provider

Pradheep1647

Model Tree

Base

Qwen/Qwen2.5-Coder-1.5B-Instruct

Adapter

this model

Input Modalities

Text

Output Modalities