Create README.md
Browse files
README.md
ADDED
|
@@ -0,0 +1,27 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# SEG-ATP: Segment-Level Learning for LLM-Based Theorem Proving
|
| 2 |
+
|
| 3 |
+
This repository contains the policy model used in the paper **"Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving"**.
|
| 4 |
+
|
| 5 |
+
## Model
|
| 6 |
+
|
| 7 |
+
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.
|
| 8 |
+
|
| 9 |
+
## Training Data
|
| 10 |
+
|
| 11 |
+
The model is trained using proof trajectories derived from STP, LeanWorkbook, and NuminaMath-LEAN.
|
| 12 |
+
|
| 13 |
+
## Usage
|
| 14 |
+
|
| 15 |
+
Please refer to the GitHub repository for preprocessing, inference, and evaluation details:
|
| 16 |
+
|
| 17 |
+
https://github.com/NJUDeepEngine/SEG-ATP
|
| 18 |
+
|
| 19 |
+
## Citation
|
| 20 |
+
|
| 21 |
+
```bibtex
|
| 22 |
+
@article{xu2026rethinking,
|
| 23 |
+
title={Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving},
|
| 24 |
+
author={Xu, Shuo and Zhang, Jiakun and Lai, Junyu and Cao, Chun and Xu, Jingwei},
|
| 25 |
+
journal={arXiv preprint},
|
| 26 |
+
year={2026}
|
| 27 |
+
}
|