metadata
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 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
@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}
}