StepFun-Formalizer-Training

<p align="center">
<img src="assets/logo.png" width="250px"><br>
</p>

# StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

<div align="center">
<a href="https://www.arxiv.org/abs/2508.04440"><img src="https://img.shields.io/static/v1?label=Paper&message=Arxiv&color=red"></a> &ensp;
<a href="https://huggingface.co/stepfun-ai/StepFun-Formalizer-7B"><img src="https://img.shields.io/static/v1?label=Model&message=HuggingFace&color=yellow"></a> &ensp;
<a href="https://github.com/stepfun-ai/StepFun-Formalizer"><img src="https://img.shields.io/static/v1?label=Code&message=Github&color=blue"></a> &ensp;
</div>
<br>

## Introduction

This repository includes the Stage-1 SFT and RL training data of [StepFun-Formalizer](https://huggingface.co/stepfun-ai/StepFun-Formalizer-32B):

- `NuminaMath-Formal-SFT-183K`: Informal-formal problem pairs translated from [NuminaMath-1.5](https://huggingface.co/datasets/AI-MO/NuminaMath-1.5) by [Kimina-Autoformalizer-7B](https://huggingface.co/AI-MO/Kimina-Autoformalizer-7B), used to supplement the model’s domain knowledge in formal language.

- ` StepFun-Formalizer-RL-6K`: We collected informal math problems paired with human-annotated (or model-generated and manually reviewed) formal statements as RL data, including [MiniF2F](https://arxiv.org/abs/2109.00110), [ProofNet](https://arxiv.org/abs/2302.12433), [PutnamBench](https://arxiv.org/abs/2407.11214), [Compfiles](https://github.com/dwrensha/compfiles) and [FormalMATH](https://arxiv.org/abs/2505.02735) (w/o Lite).

The formal statements pass the syntax check of Lean4 v4.15.0. All training data have undergone 13-gram decontamination against benchmarks.

Due to copyright restrictions, the Stage-2 SFT (Reasoning) data cannot be released.

Please refer to our [paper](https://arxiv.org/abs/2508.04440) for more details.

## License

The datasets are released under the Apache License (Version 2.0).

## Citation

```latex
@misc{stepfunformalizer2025,
title={StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion},
author={Yutong Wu and Di Huang and Ruosi Wan and Yue Peng and Shijie Shang and Chenrui Cao and Lei Qi and Rui Zhang and Zidong Du and Jie Yan and Xing Hu},
year={2025},
eprint={2508.04440},
archivePrefix={arXiv},
primaryClass={cs.CL},
url={https://arxiv.org/abs/2508.04440},
}
```

<p align="center">
<img src="assets/logo.png" width="250px"><br>
</p>

# StepFun-Formalizer：通过知识推理融合解锁大语言模型（Large Language Models）的自动形式化潜力

<div align="center">
<a href="https://www.arxiv.org/abs/2508.04440"><img src="https://img.shields.io/static/v1?label=Paper&message=Arxiv&color=red"></a> &ensp;
<a href="https://huggingface.co/stepfun-ai/StepFun-Formalizer-7B"><img src="https://img.shields.io/static/v1?label=Model&message=HuggingFace&color=yellow"></a> &ensp;
<a href="https://github.com/stepfun-ai/StepFun-Formalizer"><img src="https://img.shields.io/static/v1?label=Code&message=Github&color=blue"></a> &ensp;
</div>
<br>

## 简介

本仓库包含StepFun-Formalizer的第一阶段监督微调（Supervised Fine-Tuning，SFT）与强化学习（Reinforcement Learning，RL）训练数据：
- `NuminaMath-Formal-SFT-183K`：由[Kimina-Autoformalizer-7B](https://huggingface.co/AI-MO/Kimina-Autoformalizer-7B)从[NuminaMath-1.5](https://huggingface.co/datasets/AI-MO/NuminaMath-1.5)中翻译得到的非正式-正式问题配对数据集，用于补充模型在形式化语言领域的专业知识。
- `StepFun-Formalizer-RL-6K`：我们收集了非正式数学问题与人工标注（或模型生成并经人工审核）的形式化陈述组成的强化学习数据集，涵盖[MiniF2F](https://arxiv.org/abs/2109.00110)、[ProofNet](https://arxiv.org/abs/2302.12433)、[PutnamBench](https://arxiv.org/abs/2407.11214)、[Compfiles](https://github.com/dwrensha/compfiles)以及[FormalMATH](https://arxiv.org/abs/2505.02735)（不含Lite版本）。

上述形式化陈述均通过了Lean4 v4.15.0的语法校验。所有训练数据均已针对基准数据集完成13-gram去重净化。

由于版权限制，第二阶段监督微调（推理）数据集无法公开。

更多细节请参阅我们的[论文](https://arxiv.org/abs/2508.04440)。

## 许可证

本数据集采用Apache许可证（版本2.0）发布。

## 引用

latex
@misc{stepfunformalizer2025,
title={StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion},
author={Yutong Wu and Di Huang and Ruosi Wan and Yue Peng and Shijie Shang and Chenrui Cao and Lei Qi and Rui Zhang and Zidong Du and Jie Yan and Xing Hu},
year={2025},
eprint={2508.04440},
archivePrefix={arXiv},
primaryClass={cs.CL},
url={https://arxiv.org/abs/2508.04440},
}