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.

[image]

Repository validation

[image]

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.