| --- |
| 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. |
