Instructions to use ofankit/finance-formalisation-rlvr-4b-focus with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use ofankit/finance-formalisation-rlvr-4b-focus with PEFT:

from peft import PeftModel
from transformers import AutoModelForCausalLM

base_model = AutoModelForCausalLM.from_pretrained("Qwen/Qwen3-4B-Instruct-2507")
model = PeftModel.from_pretrained(base_model, "ofankit/finance-formalisation-rlvr-4b-focus")

Transformers

How to use ofankit/finance-formalisation-rlvr-4b-focus with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="ofankit/finance-formalisation-rlvr-4b-focus")

# Load model directly
from transformers import AutoModel
model = AutoModel.from_pretrained("ofankit/finance-formalisation-rlvr-4b-focus", device_map="auto")

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use ofankit/finance-formalisation-rlvr-4b-focus with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "ofankit/finance-formalisation-rlvr-4b-focus"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ofankit/finance-formalisation-rlvr-4b-focus",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

Use Docker

docker model run hf.co/ofankit/finance-formalisation-rlvr-4b-focus

SGLang

How to use ofankit/finance-formalisation-rlvr-4b-focus with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "ofankit/finance-formalisation-rlvr-4b-focus" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ofankit/finance-formalisation-rlvr-4b-focus",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "ofankit/finance-formalisation-rlvr-4b-focus" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "ofankit/finance-formalisation-rlvr-4b-focus",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

Docker Model Runner
How to use ofankit/finance-formalisation-rlvr-4b-focus with Docker Model Runner:
```
docker model run hf.co/ofankit/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},
}

Downloads last month: 14

Model tree for ofankit/finance-formalisation-rlvr-4b-focus

Base model

Qwen/Qwen3-4B-Instruct-2507

Adapter

(5654)

this model

Paper for ofankit/finance-formalisation-rlvr-4b-focus

DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models

Paper • 2402.03300 • Published Feb 5, 2024 • 148