| | --- |
| | license: apache-2.0 |
| | datasets: |
| | - internlm/Lean-Workbook |
| | language: |
| | - en |
| | base_model: |
| | - Qwen/Qwen2.5-Math-7B |
| | tags: |
| | - lean4 |
| | - theorem-proving |
| | - formal-mathematics |
| | metrics: |
| | - accuracy |
| | pipeline_tag: text-generation |
| | --- |
| | |
| | # LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation |
| |
|
| | This repository contains the model used in the paper *"LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation"*. |
| |
|
| | ## Model |
| |
|
| | The model is full-tuned based on [Qwen2.5-Math-7B](https://huggingface.co/Qwen/Qwen2.5-Math-7B). |
| |
|
| | ## Usage |
| |
|
| | Please refer to [GitHub page](https://github.com/NJUDeepEngine/llm_based_atp) for details. |
