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