Dataset · Hugging Face

stepfun-ai/StepFun-Formalizer-Training

Name: StepFun-Formalizer-Training
Creator: stepfun-ai
License: apache-2.0
Keywords: task_categories:text-generation, language:en, license:apache-2.0, size_categories:100K<n<1M, format:parquet, modality:text, library:datasets, library:dask, library:mlcroissant, library:polars, arxiv:2508.04440, arxiv:2109.00110, arxiv:2302.12433, arxiv:2407.11214, arxiv:2505.02735

StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion Introduction This repository includes the Stage-1 SFT and RL training data of StepFun-Formalizer: NuminaMath-Formal-SFT-183K: Informal-formal problem pairs translated from NuminaMath-1.5 by Kimina-Autoformalizer-7B, used to supplement the model’s domain knowledge in formal language. StepFun-Formalizer-RL-6K: We collected informal math… See the full description on the dataset page: https://huggingface.co/datasets/stepfun-ai/StepFun-Formalizer-Training.

View on Hugging FaceReport an issue

Author / organization	stepfun-ai
License (as declared)	apache-2.0
Downloads	143 (as reported by Hugging Face)
Likes	5
Created	13 October 2025
Last updated at source	13 October 2025

AutoformalizationLean4

Embed this entry

<iframe src="https://silytics.si/embed/item/a1ab993e-f5ad-40ad-a9e0-0c1961c64313" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

More from stepfun-ai

stepfun-ai/Step-3.5-Flash-SFTDataset
stepfun-ai/GEdit-BenchDataset
stepfun-ai/NextStep-dataDataset
stepfun-ai/PaCoRe-Train-8kDataset
stepfun-ai/StepEval-Audio-ToolcallDataset
stepfun-ai/StepEval-Audio-ParalinguisticDataset

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.