---
license: apache-2.0
base_model: Qwen/Qwen2.5-Math-7B
datasets:
  - kfdong/STP
  - internlm/Lean-Workbook
  - AI-MO/NuminaMath-LEAN
language:
  - en
tags:
  - theorem-proving
  - automated-theorem-proving
  - lean4
  - mathematical-reasoning
  - llm
  - qwen2.5-math
pipeline_tag: text-generation
---


# SEG-ATP: Segment-Level Learning for LLM-Based Theorem Proving

This repository contains the policy model used in the paper **"Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving"**.

## Model

The model is fully fine-tuned from [Qwen2.5-Math-7B](https://huggingface.co/Qwen/Qwen2.5-Math-7B) using segment-level supervision constructed from Lean 4 proof trajectories.

## Training Data

The model is trained using proof trajectories derived from STP, LeanWorkbook, and NuminaMath-LEAN.

## Usage

Please refer to the GitHub repository for preprocessing, inference, and evaluation details:

https://github.com/NJUDeepEngine/SEG-ATP

## Citation

```bibtex
@article{xu2026rethinking,
  title={Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving},
  author={Xu, Shuo and Zhang, Jiakun and Lai, Junyu and Cao, Chun and Xu, Jingwei},
  journal={arXiv preprint},
  year={2026}
}