qwen-lean4-formaliser-vLoRA

A QLoRA adapter on Qwen3-Coder-30B-A3B-Instruct for Lean 4 autoformalization, translating natural-language mathematics into verified Lean 4 theorem statements, type-checked against Mathlib.

Evaluated on the ProofNet test set: 63% Pass@5 with multi-turn compiler repair.

Training Procedure

This model was produced by a multi-stage fine-tuning and reinforcement learning pipeline:

Stage 1, Syntax Alignment (SFT)

Supervised fine-tuning on ~40,000 informal/formal statement pairs (subsampled and filtered from Herald and Lean-Workbook). Completion-only cross-entropy loss on Lean 4 output tokens. This stage teaches Lean 4 syntax and theorem structure.

Stage 2, Reinforcement Learning with Compiler Feedback (RLCF)

Group Relative Policy Optimization (GRPO) with a persistent Lean 4 REPL worker pool as the reward environment. The policy generates G=8 completions per prompt; each is type-checked against Mathlib. A composite gated reward function penalizes malformed output, partially rewards well-formed failures, and rewards compilation weighted by structural faithfulness to a reference formalization. Final RLCF training used the miniF2F benchmark dataset.

Adapter Configuration

Setting	Value
Method	QLoRA
Base model precision	NF4 double-quantized (bfloat16 compute)
Rank (attention)	r=64, α=128
Rank (expert MLP)	r=8, α=16
Target modules	q/k/v/o_proj, gate/up/down_proj
Trainable parameters	468M (2.92% of total)
Dropout	0.1
Training hardware	NVIDIA RTX 5090ti (32 GB VRAM)

Training Data

Dataset	Role	Citation
Herald	Stage 1 SFT corpus	[8]
Lean-Workbook	Stage 1 SFT corpus	[7]
miniF2F	Stage 2 RLCF training	[9]
ProofNet	Evaluation benchmark	[10]

Benchmark Results (ProofNet Test Set, n=100)

Metric	Stage 1 (SFT) baseline	This model (Stage 2 RLCF)
Well-Formed Rate	96.0%	99.0%
Compile@1	31.0%	38.0%
Compile@2	39.0%	53.0%
Compile@3	41.0%	59.0%
Compile@4	42.0%	60.0%
Pass@5	44.0%	63.0%
Mean Iterations to Solve	1.52	1.67
Structural Faithfulness	0.469	0.639
Throughput (tok/s)	-	6.8

RLCF improves Pass@5 by +19 points over the Stage 1 SFT baseline. Multi-turn compiler repair adds a further +25 points over single-turn Compile@1.

Usage

from transformers import AutoTokenizer, AutoModelForCausalLM
from peft import PeftModel

base_id = "Qwen/Qwen3-Coder-30B-A3B-Instruct"
adapter_id = "JanosMozer/qwen-lean4-formaliser-vLoRA"

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

For best results, pair with a Lean 4 REPL for multi-turn compiler feedback (up to 5 repair iterations).

References

[1] Qwen Team (2025). Qwen3 Technical Report. arXiv:2505.09388. https://arxiv.org/abs/2505.09388

[2] Dettmers et al. (2023). QLoRA: Efficient Finetuning of Quantized LLMs. arXiv:2305.14314. https://arxiv.org/abs/2305.14314

[4] Shao et al. (2024). DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv:2402.03300. https://arxiv.org/abs/2402.03300

[5] Guo et al. (2025). DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. arXiv:2501.12948. https://arxiv.org/abs/2501.12948

[6] Zheng et al. (2023). ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. arXiv:2302.12433. https://arxiv.org/abs/2302.12433

[7] DeepSeek-AI (2024). Lean-Workbook. https://huggingface.co/datasets/deepseek-ai/Lean-Workbook

[8] Alex J. Best (2024). Herald. https://huggingface.co/datasets/alexjbest/herald

[9] Facebook Research (2021). miniF2F. https://huggingface.co/datasets/facebook/miniF2F

[10] Hoskinson Center (2023). ProofNet. https://huggingface.co/datasets/hoskinson-center/proofnet