qwen-lean4-formaliser-vDoRA
A QDoRA 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: 64% Pass@5 with multi-turn compiler repair. Highest accuracy of all trained variants.
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.
DoRA (Weight-Decomposed Low-Rank Adaptation) decomposes weight updates into separate magnitude and directional components, generally yielding stronger generalization than standard LoRA at the cost of ~2x lower inference throughput.
Adapter Configuration
| Setting | Value |
|---|
| Method | QDoRA |
| 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
Benchmark Results (ProofNet Test Set, n=50)
| Metric | Stage 1 (SFT) baseline | This model (Stage 2 RLCF) |
|---|
| Well-Formed Rate | 100.0% | 98.0% |
| Compile@1 | 32.0% | 36.0% |
| Compile@2 | 44.0% | 54.0% |
| Compile@3 | 46.0% | 58.0% |
| Compile@4 | 48.0% | 62.0% |
| Pass@5 | 48.0% | 64.0% |
| Mean Iterations to Solve | 1.46 | 1.72 |
| Structural Faithfulness | 0.484 | 0.623 |
| Throughput (tok/s) | - | 3.2 |
RLCF improves Pass@5 by +16 points over the Stage 1 SFT baseline. This variant achieves the highest overall Pass@5 (64%) across all trained configurations. DoRA's weight decomposition adds per-forward-pass overhead, yielding ~3.2 tok/s vs ~6.8 tok/s for the LoRA variant; see
qwen-lean4-formaliser-vLoRA for the higher-throughput option.
Usage
1from transformers import AutoTokenizer, AutoModelForCausalLM
2from peft import PeftModel
3
4base_id = "Qwen/Qwen3-Coder-30B-A3B-Instruct"
5adapter_id = "JanosMozer/qwen-lean4-formaliser-vDoRA"
6
7tokenizer = AutoTokenizer.from_pretrained(adapter_id)
8model = AutoModelForCausalLM.from_pretrained(base_id, device_map="auto", torch_dtype="auto")
9model = 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[3] Liu et al. (2024).
DoRA: Weight-Decomposed Low-Rank Adaptation. arXiv:2402.09353.
https://arxiv.org/abs/2402.09353[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
