File size: 649 Bytes
666328c a9dde19 666328c aa8e7b1 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 |
---
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. |