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

Qwen2.5-Coder 1.5B Lean language SFT

This repository contains a LoRA adapter for Qwen/Qwen2.5-Coder-1.5B-Instruct. It is a small syntax warm-up trained to follow introductory Lean 4 programming instructions. It is not a theorem-proving model and was not trained on proof generation.

This revision replaces the original 99-row experiment with 285 training examples and a 34-example held-out evaluation split. All 319 dataset answers were independently recompiled before training.

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.

Compilation results by documentation section:

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

• 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
• Hardware: one NVIDIA GeForce RTX 4060 Laptop GPU
• Training runtime: 167.4 seconds

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

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.