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