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

Qwen2.5-Coder 1.5B Lean repository midtraining

This repository contains a LoRA adapter continued from Pradheep1647/qwen2.5-coder-1.5b-lean-language-sft on 20.48M usable Lean repository tokens. The base model is Qwen/Qwen2.5-Coder-1.5B-Instruct.

This is a repository-language continuation checkpoint, not a finished theorem prover. It improves held-out repository language-model loss, but did not improve compilation on the small instruction benchmark and reduced instruction adherence. The measured regression is reported below because this adapter should be followed by proof-focused SFT before verifier RL.

Results

Lean language generation

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

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

Repository validation

Metric	Before	After	Change
Loss	1.6767	1.0038	-40.1%
Perplexity	5.3480	2.7287	-49.0%

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

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.