finance-formalisation-rlvr-4b-focus

finance-formalisation-rlvr-4b-focus

This is a PEFT LoRA adapter for Qwen/Qwen3-4B-Instruct-2507, specialized for formalizing finance theorems in Lean 4. It was warm-started from verified supervised examples and refined with verifier-reward GRPO/RLVR.

Quick start

from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base_id = "Qwen/Qwen3-4B-Instruct-2507"
adapter_id = "ofankit/finance-formalisation-rlvr-4b-focus"

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)

Evaluation

On the repository's held-out finance formalization benchmark, this adapter solved 107 of 153 examples at pass@1 (0.6993). The verified SFT warm start solved 106 of 153 (0.6928) under the same evaluator.

Intended use and limitations

Use this adapter for research on finance-domain formalization, Lean 4 generation, and verifier-guided post-training. Generated proofs must still be checked by Lean. The benchmark is domain-specific and does not establish general mathematical, financial-advice, or production-safety performance.

Training procedure

This model was trained with GRPO, a method introduced in DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models.

Framework versions

• PEFT 0.18.1
• TRL: 0.24.0
• Transformers: 4.57.6
• Pytorch: 2.10.0
• Datasets: 4.3.0
• Tokenizers: 0.22.2

Citations

@article{shao2024deepseekmath,
    title        = {{DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models}},
    author       = {Zhihong Shao and Peiyi Wang and Qihao Zhu and Runxin Xu and Junxiao Song and Mingchuan Zhang and Y. K. Li and Y. Wu and Daya Guo},
    year         = 2024,
    eprint       = {arXiv:2402.03300},
}