---
title: lean-qwen0.5b-rl
canonical_url: "https://www.modelscope.cn/models/mengxin1942/lean-qwen0.5b-rl"
md_url: "https://www.modelscope.cn/models/mengxin1942/lean-qwen0.5b-rl.md"
repository: mengxin1942/lean-qwen0.5b-rl
chinese_name: "Lean4定理证明任务RL版本的qwen0.5b"
last_updated: 2025-02-14
license: "Apache License 2.0"
model_type:
  - qwen2
architectures:
  - Qwen2ForCausalLM
base_model:
  - Qwen/Qwen2.5-0.5B-Instruct
base_model_relation: finetune
parameters: 494.0M
tensor_type:
  - F32
library_name:
  - safetensors
  - pytorch
frameworks:
  - Pytorch
inference_backends:
  - "deploy_task text/emb"
  - "lmdeploy 0.9.1"
  - "lmdeploy_turbomind 0.9.1"
  - "sglang 0.5.2"
  - "vllm 0.9.2"
downloads: 46
stars: 0
---

# lean-qwen0.5b-rl

> lean-qwen0.5b-rl - mengxin1942 在 ModelScope 开源的模型。用于lean4定理证明任务，基于qwen2.5-0.5B的RL优化的模型

mengxin1942/lean-qwen0.5b-rl 是 ModelScope 魔搭社区上的 494.0M 参数机器学习模型，采用 Apache License 2.0 许可，基于 Qwen/Qwen2.5-0.5B-Instruct 构建，可用 deploy_task text/emb、lmdeploy 0.9.1、lmdeploy_turbomind 0.9.1 部署。

- **Repository**: mengxin1942/lean-qwen0.5b-rl
- **License**: Apache License 2.0
- **Parameters**: 494.0M
- **Base model**: Qwen/Qwen2.5-0.5B-Instruct
- **Inference backends**: deploy_task text/emb, lmdeploy 0.9.1, lmdeploy_turbomind 0.9.1, sglang 0.5.2, vllm 0.9.2
- **Downloads**: 46
- **Stars**: 0
- **Last updated**: 2025-02-14

Source: https://www.modelscope.cn/models/mengxin1942/lean-qwen0.5b-rl

---

## Intro

This is a reinforcement learning framework to iteratively optimize the pretrained LLM by rolling out next tactics and comparing them with the expected ones. The experiment results show that it helps to achieve a higher accuracy compared with directly fine-tuned LLM.


| |#Positive sample on MiniF2F | Acc on MiniF2F | Acc on Trainset |
|-----|-----------|---------|-----|
|Lean-qwen0.5B-sft | 11 | 36% |  49% |
|Lean-qwen0.5B-rl | 13 | 43\% | 61% |


[tech report](https://arxiv.org/abs/2502.08908)

[Github](https://github.com/zhilingluo/theorem_prover)


## Models

[Lean-qwen0.5b-sft](https://www.modelscope.cn/models/mengxin1942/lean-qwen0.5b-sft/)

[Lean-qwen0.5b-rl](https://www.modelscope.cn/models/mengxin1942/lean-qwen0.5b-rl/)

## Citation
```bibtex
@article{lean-reinforced-llm,
      title={Reinforced Large Language Model is a formal theorem prover}, 
      author={Zhiling Luo},
      year={2025},
      journal={arXiv preprint arXiv:2502.08908},
      url={https://arxiv.org/abs/2502.08908},
      primaryClass={cs.AI}
}
```

#### 您可以通过如下git clone命令，或者ModelScope SDK来下载模型

SDK下载
```bash
#安装ModelScope
pip install modelscope
```
```python
#SDK模型下载
from modelscope import snapshot_download
model_dir = snapshot_download('mengxin1942/lean-qwen0.5b-rl')
```
Git下载
```
#Git模型下载
git clone https://www.modelscope.cn/mengxin1942/lean-qwen0.5b-rl.git
```

<p style="color: lightgrey;">如果您是本模型的贡献者，我们邀请您根据<a href="https://modelscope.cn/docs/ModelScope%E6%A8%A1%E5%9E%8B%E6%8E%A5%E5%85%A5%E6%B5%81%E7%A8%8B%E6%A6%82%E8%A7%88" style="color: lightgrey; text-decoration: underline;">模型贡献文档</a>，及时完善模型卡片内容。</p>