| license: apache-2.0 | |
| datasets: | |
| - SJTULean/LeanStatement_CoT | |
| language: | |
| - en | |
| base_model: | |
| - Qwen/Qwen2.5-7B-Instruct | |
| Wishing users to be clear that the model's formalization ability is (contrastivelty) relatively faible compared to LeanStatement_SFT and PPO, thus may only be considered as an experimental model. |