Pradheep1647

qwen2.5-coder-1.5b-lean-repository-midtraining

README

License: apache-2.0

Results

Lean language generation

The same 34 held-out prompts were generated greedily before and after midtraining and checked with local Lean 4 + Mathlib.

Table with columns: Metric, Before, After, Change
Metric	Before	After	Change
Compile	26/34 (76.5%)	26/34 (76.5%)	0.0 pp
Topic adherence	33/34 (97.1%)	24/34 (70.6%)	-26.5 pp
Clean compile	25/34 (73.5%)	21/34 (61.8%)	-11.8 pp

Before and after Lean generation evaluation

Repository validation

Table with columns: Metric, Before, After, Change
Metric	Before	After	Change
Loss	1.6767	1.0038	-40.1%
Perplexity	5.3480	2.7287	-49.0%

Midtraining dynamics

The repository loss result shows that the adapter learned the corpus distribution. It does not establish improved theorem-proving ability. The generation results indicate catastrophic forgetting of some instruction-following behavior despite unchanged Lean compilation.

Training

Dataset: Pradheep1647/lean-repository-midtraining-v1
Sources: pinned Lean 4, Mathlib, Batteries, and Aesop snapshots
Usable data: 18,876 chunks and 20,476,910 Qwen tokenizer tokens
Context length: 1,536 tokens; oversized declarations were skipped, not truncated
Epochs: 1
Optimizer steps: 2,228
Effective batch size: 8 via gradient accumulation
Learning rate: 5e-5
Precision: BF16
LoRA: rank 16, alpha 32, dropout 0.05; attention and MLP projections
Trainable adapter parameters: approximately 73.9 MB in safetensors form
Training runtime: 12,751.6 seconds on an NVIDIA RTX 4060 Laptop GPU

The dataset uses file-level train/validation splitting and exact normalized benchmark denylisting. Those checks do not detect semantically equivalent or renamed statements.

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-repository-midtraining"

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

Intended next stage

Use this checkpoint as an initialization for verified proof SFT, mixing some Lean language instruction data to recover instruction adherence. Evaluate on held-out theorem proving tasks before starting verifier-guided RL in the Lean verifier environment.

Limitations

This is an adapter and requires the Qwen base model.
The generation evaluation has only 34 examples and should not be treated as a broad theorem-proving benchmark.
Repository validation loss is not a proof-success metric.
The corpus is primarily library source and can weaken chat or instruction behavior.
Generated Lean must still be checked by a trusted Lean verifier.

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