murillo2000/qwen3-8b-base-lean-sft-qlora

Qwen3-8B-Base Lean SFT QLoRA

murillo2000/qwen3-8b-base-lean-sft-qlora is the validation-selected Phase 5 adapter produced by the qwen-lean project. It is a standard, unmerged PEFT LoRA adapter for causal language modeling with Qwen/Qwen3-8B-Base.

This repository does not contain Qwen base-model weights. The pinned base model must be downloaded separately:

• Base model: Qwen/Qwen3-8B-Base
• Base revision: 49e3418fbbbca6ecbdf9608b4d22e5a407081db4
• Adapter artifact ID: phase5-train-full-v1-lora
• Selected optimizer step: 9962
• Format: standard unmerged PEFT LoRA

The adapter was trained through QLoRA with rank r=16, lora_alpha=32, dropout 0.0, no bias, and these target modules:

q_proj, k_proj, v_proj, o_proj, gate_proj, up_proj, and down_proj.

Training

The supervised corpus was derived from Lean-verified mathlib theorem/proof pairs. Phase 5 retained all 79,696 eligible training examples under the frozen mathlib-sft-v1 serialization contract and trained for exactly one epoch.

The fixed first-cycle configuration was:

• maximum sequence length: 1,024 tokens;
• completion-only causal-LM loss, including terminal EOS;
• prompt and padding labels masked;
• no packing and no silent truncation;
• 4-bit NF4 base quantization with double quantization and BF16 compute;
• per-device micro-batch size 1;
• gradient accumulation 8, for an effective batch size of 8;
• paged 8-bit AdamW;
• learning rate 1e-4 with cosine scheduling;
• one full eligible training epoch.

The checkpoint at optimizer step 9962 was selected solely because it had the lowest full-validation mean target-token cross-entropy among the planned quarter-boundary checkpoints. Held-out and miniF2F results were not consulted during checkpoint selection. This configuration records the project's first full SFT cycle and is not claimed to be globally optimal.

No chat template was applied during training. The model learned plain causal completion under the project's whole-proof-v1 / mathlib-sft-v1 contracts.

Verifier-based evaluation

A generated proof counts as successful only when Lean accepts the reconstructed theorem. These metrics are verifier-based, not exact-string-match metrics.

Phase 5 mathlib held-out

The workload contains 512 held-out mathlib theorems with 4 sampled candidates per task.

Model	pass@1	pass@4
Qwen3-8B-Base	0.001953125	0.0078125
Phase 5 SFT adapter	0.0166015625	0.048828125

Both arms used the same generation and Lean-verification contract. The comparison completed with zero generation errors, zero verifier errors, and zero unresolved verifier timeouts.

miniF2F validation

The workload contains all 244 miniF2F validation theorems with 8 sampled candidates per task.

Model	pass@1	pass@4	pass@8
Qwen3-8B-Base	0.0128073770	0.0477166276	0.0860655738
Phase 5 SFT adapter	0.0394467213	0.1031615925	0.1434426230

miniF2F test was not evaluated. The validation results were not used for checkpoint selection. All adapter candidates were evaluated through Lean; the accepted run had zero generation errors, verifier errors, and unresolved verifier timeouts.

Usage

Install compatible versions of transformers, peft, torch, and safetensors, then load the pinned base and adapter:

import torch
from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base_model_id = "Qwen/Qwen3-8B-Base"
base_revision = "49e3418fbbbca6ecbdf9608b4d22e5a407081db4"
adapter_id = "murillo2000/qwen3-8b-base-lean-sft-qlora"

tokenizer = AutoTokenizer.from_pretrained(
    base_model_id,
    revision=base_revision,
)
base_model = AutoModelForCausalLM.from_pretrained(
    base_model_id,
    revision=base_revision,
    torch_dtype=torch.bfloat16,
    device_map="auto",
)
model = PeftModel.from_pretrained(base_model, adapter_id)
model.eval()

This adapter was not trained with a chat template. Consumers seeking behavior comparable to the reported evaluation should use the qwen-lean plain-completion prompt contract instead of applying a chat template.

Provenance and integrity

• qwen-lean Phase 5 issue: #19
• merged implementation and evidence: PR #20
• selected training artifact manifest SHA-256: 48d33bc2f276d6f8c22525a5cb30fafe8677da95e866dbf3f37116e78e8ae990
• adapter_model.safetensors SHA-256: 8aa50fa56f6a1d03a702abcaafc20e11d661a4a2ac935864bf5648411e5cdc58
• adapter_config.json SHA-256: 4b7b513b216484554e05d3c75ecf0777ee1fbae94935e93d949d63cf4a76481c

The repository intentionally excludes optimizer/scheduler/RNG state, trainer state, datasets, raw generations, caches, tokenizer copies, and full Qwen weights.

Limitations

• The task is whole-proof generation without tactic-level search.
• Training examples were limited to at most 1,024 serialized tokens.
• This was the project's first full SFT cycle and used a single epoch.
• Training data came primarily from mathlib, so behavior outside that domain is not established.
• Reported miniF2F results are on validation, not test.
• No state-of-the-art claim is made.
• Later Phase 6+ analysis or experiments may select or replace this checkpoint as the project's reference adapter.

License and attribution

The adapter artifacts in this repository are released under Apache License 2.0. This model card is the notice that the adapter is a qwen-lean post-training modification; it remains separate from and does not include the original base weights or the training corpus.

• The base model was created by the Qwen team at Alibaba Cloud and is published under Apache-2.0.
• The source corpus was derived from Apache-2.0-licensed mathlib proofs. Credit belongs to the mathlib and Lean communities and the individual proof authors.
• Post-training, artifact selection, and evaluation were performed by the qwen-lean project.

Downstream users must obtain the base model separately and comply with the applicable licenses for both the base model and this adapter.