FormalStep

用于增强大型语言模型在数学推理中的表现，通过回顾性步骤感知的形式验证方法。

Intended to enhance the performance of large language models in mathematical reasoning through the form of methodological verification by retrospective steps.

原始信息汇总

Safe (ACL 2025 Main) 数据集概述

数据集基本信息

• 名称: FormalStep
• 关联论文: Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
• 论文链接: https://www.arxiv.org/abs/2506.04592
• 代码仓库: https://github.com/liuchengwucn/Safe
• 数据集地址: https://huggingface.co/datasets/liuchengwu/FormalStep

数据集用途

• 用于通过Lean 4形式化语言对大型语言模型的数学推理能力进行形式化验证。

数据集组成

• 包含数据集:
  • Math
  • GSM8K
  • PRM800K (MATH-500)
  • CollegeMath
• 获取方式:
  • Math/GSM8K/CollegeMath已包含在项目中
  • PRM800K需使用download.py脚本下载

运行环境要求

• 硬件要求:
  • 至少2块NVIDIA GPU
  • 每服务约需40GB显存(验证器和推理模型各需一块GPU)
• 软件依赖:
  • Docker with NVIDIA Container Toolkit
  • Docker Compose插件
  • Lean环境(推荐使用项目提供的Docker镜像)

模型依赖

• 推理模型:
  • meta-llama/Llama-3.1-8B-Instruct
  • deepseek-ai/deepseek-math-7b-instruct
  • meta-llama/Meta-Llama-3-8B-Instruct
• 验证器模型:
  • deepseek-ai/DeepSeek-Prover-V1.5-RL
• 奖励模型:
  • peiyi9979/math-shepherd-mistral-7b-prm
  • RLHFlow/Llama3.1-8B-PRM-Deepseek-Data
  • RLHFlow/ArmoRM-Llama3-8B-v0.1
  • Skywork/Skywork-Reward-Llama-3.1-8B-v0.2

实验复现步骤

1. collect_trace.py - 收集推理轨迹
2. aggregator.py - 训练LSTM聚合器
3. benchmark.py - 评估SAFE框架性能
4. benchmark_ensemble.py - 测试超参数alpha的影响

引用信息

bibtex @misc{liu2025safe, title={Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification}, author={Chengwu Liu and Ye Yuan and Yichun Yin and Yan Xu and Xin Xu and Zaoyu Chen and Yasheng Wang and Lifeng Shang and Qun Liu and Ming Zhang}, year={2025}, eprint={2506.04592}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2506.04592}, }

搜集汇总

数据集介绍

构建方式

在数学推理领域，FormalStep数据集的构建采用了严谨的学术方法论。研究团队基于Lean 4形式化语言，通过回溯式步骤感知的形式验证技术，对大型语言模型的数学推理能力进行系统性评估。数据集整合了Math、GSM8K、PRM800K和CollegeMath等多个权威数学基准，采用两阶段构建流程：首先收集推理轨迹作为训练数据，随后训练LSTM聚合器进行特征提取，最终形成具有形式化验证标签的高质量数据集。

使用方法

使用该数据集需遵循特定的技术规范。研究者需配置包含NVIDIA GPU的计算环境，建议通过Docker容器部署预构建的Lean开发环境。典型工作流程包括：加载预训练的语言模型和验证器，运行collect_trace.py收集推理轨迹，通过aggregator.py训练特征聚合器，最后使用benchmark系列脚本进行性能评估。数据集支持多种主流数学推理模型的对比实验，特别适合研究形式化验证对数学推理能力的提升效果。

背景与挑战

背景概述

FormalStep数据集由Liu Chengwu等研究人员于2025年提出，旨在通过Lean 4形式化语言验证大语言模型在数学推理任务中的表现。该数据集作为ACL 2025会议论文《Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification》的核心组成部分，聚焦于解决数学定理证明和复杂问题求解中的形式化验证难题。研究团队整合了Math、GSM8K、PRM800K和CollegeMath等多个数学推理基准，通过构建回溯式步骤感知的验证框架，显著提升了模型在严格数学推导中的可靠性。

当前挑战

该数据集面临双重技术挑战：在领域问题层面，数学形式化验证需要精确处理高阶逻辑和抽象代数结构，现有神经符号系统难以平衡推理效率与严格性；在构建过程中，需协调7B参数规模的语言模型与Lean证明助手的交互，涉及复杂的GPU资源调度和Docker环境配置。数据集要求同时部署推理模型与证明模型，对计算基础设施的异构加速能力和数学知识库的完整性提出极高要求。

常用场景

经典使用场景

在数学推理领域，FormalStep数据集被广泛应用于验证大型语言模型（LLM）的数学推理能力。通过使用Lean 4形式化语言，该数据集能够精确地验证每一步数学推理的正确性，从而为研究者提供一个可靠的评估平台。其经典使用场景包括验证模型在复杂数学问题中的推理步骤是否严谨，以及评估模型在形式化验证环境下的表现。

解决学术问题

FormalStep数据集解决了数学推理中形式化验证的难题，为研究者提供了一个标准化的评估框架。通过该数据集，研究者能够系统地分析LLM在数学推理中的错误模式，从而改进模型的推理能力。此外，该数据集还促进了形式化验证技术在自然语言处理领域的应用，推动了数学推理研究的深入发展。

实际应用

在实际应用中，FormalStep数据集被用于优化教育辅助工具和自动解题系统。通过验证LLM的数学推理步骤，该数据集帮助开发者构建更可靠的数学辅助工具，提升学生的学习体验。同时，该数据集还被用于金融和工程领域，验证复杂计算和推理过程的准确性。

数据集最近研究

最新研究方向

在形式化验证与大型语言模型交叉领域，FormalStep数据集正推动数学推理能力验证的前沿探索。该数据集通过Lean 4形式语言构建的验证框架，解决了传统数学推理评估中逻辑严谨性不足的痛点。当前研究聚焦于三步验证范式：基于LSTM的推理轨迹聚合器训练、动态回溯式步骤感知机制设计，以及多模型协同验证系统的构建。这种将形式化方法深度融入预训练模型微调流程的创新模式，显著提升了GSM8K、PRM800K等数学基准测试的验证效率。其提出的α超参数优化策略，为平衡验证精度与计算开销提供了新的方法论参考，相关技术已被应用于DeepSeek-Prover等开源证明系统的性能增强。