README.md

metadata

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.

Usage

Please refer to GitHub page for details.