StochBench: 专为 Lean 设计的随机过程领域特定基准测试

# 一个用于Lean中随机过程的领域特定基准
来源：https://arxiv.org/html/2609.09264
工作坊标题：第六届数学推理与人工智能研讨会

Debargha Ganguly
Vikash Singh
Vipin Chaudhary
单位：凯斯西储大学
邮箱：\{idan, debargha, vikash, vipin\}@case.edu
链接：https://huggingface.co/datasets/IdanDavidovich/StochBench

###### 摘要
当前用于大语言模型形式化定理证明的主要基准，如IMO和Putnam竞赛，只是少量竞赛数学题目的集合，无法很好地代表特定领域的应用。我们引入了**StochBench**，这是一个包含450道研究生级别随机过程问题的Lean 4基准，问题涵盖不同的抽象层次，每道题都附有其自然语言来源。该基准针对Mathlib中代表性不足的领域，涵盖了有限和可数马尔可夫链、更新过程、随机游走、鞅、停时、排队论、布朗运动、随机微积分、弱收敛以及泊松和连续时间马尔可夫过程。我们基于Opus 4.8的智能体在每题15分钟的限制下，达到了34.9%的证明率（157/450）。StochBench更真实地代表了特定领域的应用数学，同时对先进的证明器仍具挑战性。

## 1 引言
Lean支持可机器验证的数学，已有包括八维球面填充、布朗运动和费马大定理（针对正则素数）等重大形式化成果（Hariharan et al., 2026; Degenne et al., 2025; Best et al., 2025）。将这一进展扩展到日常的数学辅助，需要评估自动化证明器在多大程度上能一致地处理某个学科反复出现的论证。竞赛基准和广泛的教科书集合提供了宝贵的测试，但聚合分数可能会掩盖特定领域的优势和失败（Zheng et al., 2021; Azerbayev et al., 2023; Tsoukalas et al., 2024）。我们介绍了**StochBench**，一个针对研究生随机过程的Lean 4基准，该领域是统计学和机器学习的核心。我们专注于马尔可夫链、鞅和连续时间过程中的相关问题，优先考虑领域内的深度而非跨领域的广度。然而，一些问题需要Mathlib环境中不可用的基础设施（The mathlib Community, 2026）。

*直接*目标使用Mathlib或共享定义，而*抽象化*目标则将所需属性作为假设。Lean验证每个证明的结论都是由其声明的假设推导得出的。我们已极其谨慎地确保（全部由人类编写的）定义和假设忠实地反映了源问题，但进一步的同行评审将使其受益。

我们的贡献包括：
1.  **一个领域聚焦的基准**：我们发布了450个配对了非形式化陈述的Lean 4定理目标，以及共享定义和基线证明尝试。
2.  **一个考虑范围的基线评估**：我们标注了形式化的范围，并在每题15分钟的上限下评估了一个编译器引导的证明智能体，按主题和表示形式报告结果。

请参见图1说明：StochBench的构建过程：由数学家主导的策展和LLM辅助的形式化，通过共享定义产生了跨八个主题的450个Lean 4目标，包含114个直接目标和336个抽象化目标。

## 2 相关工作
**形式化数学推理的基准**：基于Lean的评估沿着竞赛难度、课程覆盖范围和研究背景的互补轴线发展。miniF2F（Zheng et al., 2021）建立了一个以奥林匹克数学为中心的基准，ProofNet（Azerbayev et al., 2023）将非形式化的陈述和证明与形式化的本科定理陈述配对，PutnamBench（Tsoukalas et al., 2024）将基于竞赛的评估扩展到具有挑战性的本科问题。FormalMATH（Yu et al., 2025）扩展了Lean 4基准的规模和学科覆盖范围，而FormalProofBench（Ravi et al., 2026）则针对来自教科书和资格考试的高级本科和研究生问题。在走向数学实践方面，RLMEval（Poiroux et al., 2025）评估研究级别的Lean形式化项目中的定理，FormalML（Yang et al., 2025）研究机器学习理论中的子目标完成，包括优化和概率不等式。

**证明自动化、表示与语义保真度**：Lean 4（Moura and Ullrich, 2021）和Mathlib（The mathlib Community, 2020）提供了一个可扩展的证明环境和可复用的数学抽象用于自动推理。LeanDojo（Yang et al., 2023）结合了编程证明交互与检索增强的前提选择，而Lean Copilot（Song et al., 2024）将策略建议和证明搜索集成到交互式形式化中。Lean-STaR（Lin et al., 2024）将非形式推理与策略生成交织进行；DeepSeek-Prover-V1.5（Xin et al., 2024）结合了证明助手反馈与强化学习和树搜索；DeepSeek-Prover-V2（Ren et al., 2025）围绕子目标分解发展了强化学习。这些进展解决了证明构造问题，但证明成功本身并不确立与预期非形式主张的对应关系。FormalAlign（Lu et al., 2024）明确评估了非形式-形式语义对齐，而MathAtlas（Patel et al., 2026）则考察了涉及定义和依赖结构的研究生级别自动形式化。TaoBench（Taylor et al., 2026）通过成对的、数学上等价但使用定制定义和Mathlib定义表达的陈述，隔离了一个相关的表示问题。

**形式化概率与随机过程基础设施**：大量的Lean发展已经为StochBench背后的数学提供了支持。Ying and Degenne (2022)形式化了Doob鞅收敛定理以及条件期望、停时和鞅理论；Marion (2025)通过Ionescu–Tulcea定理构造了轨迹空间概率测度，Degenne (2025)发展了马尔可夫核和分解。Degenne et al. (2025)形式化了布朗运动及其扩展和路径连续性机制，而Coelho (2026b)发展了L² Itô积分和对具有有界导数的C³函数的Itô公式。互补性工作将教科书概率与Mathlib接口连接起来（Deng and Shum, 2026），验证了强化学习收敛性（Zhang, 2025），并构建了一个具有显式保真度审计的数学金融库（Coelho, 2026a）。

## 3 StochBench基准
#### 来源与选择。
StochBench包含450个研究生随机过程领域的Lean 4定理目标。我们结合了为基准编写的题目，以及从《概率、数理统计与随机过程》（Siegrist, 2022）和MIT的《随机过程导论》（Wu, 2015）、《高级随机过程》（Gamarnik, 2013）和《离散随机过程》（Gallager, 2011）课程笔记和作业中选出的练习、引理、定理和推论。我们选择了与随机过程相关的问题，并将它们写成带有假设的命题。更接近一般概率论的陈述，例如“证明总变差距离满足三角不等式：‖μ−ν‖TV≤‖μ−η‖TV+‖η−ν‖TV”，未被包含。语料库涵盖八个主题，汇总于表1中。

#### 陈述构建。
所有基准特定的定义、假设和问题均由人类撰写。基于Opus 4.8的形式化助手协助将问题表达为Lean定理陈述。我们使用Lean反馈修订候选陈述，直到它们能在Lean 4.30.0及固定Mathlib版本下进行精化。精化检查确保陈述类型良好。我们认为任务在于证明与源问题建立对应关系的定理。以防有形式化错误潜入，我们也接受对定理不正确的内核检查证明。

#### 共享数学定义。
我们为反复出现的概念构建了共享的抽象和定义。有限状态链使用共同的矩阵表示来描述随机性、平稳性、不可约性、非周期性、转移幂的最终正性、细致平衡、时间反演和总变差距离。`IsHittingSolution`和`returnTime`表达第一步方程，而`nstep`通过无穷和定义可数状态情况下的转移幂。其他定义将目标连接到Mathlib：`natStop`将自然数值停时转换为`WithTop`，`runningMax`表达有限运行最大值，`IsConstDrift`陈述条件增量恒等式。重用这些定义为相关目标提供了共同的数学表示。

#### 边际分布与联合过程法则。
我们区分了过程在一个时间点的分布与其在时间上的联合行为。`HasMatrixMarginals`将Xₙ的分布与Pⁿ的对应行联系起来。`HasChainLaw`则通过ℙₘ(X₀=x₀, …, Xₙ=xₙ)=ν(x₀)∏ᵢ₌₀ⁿ⁻¹ P(xᵢ, xᵢ₊₁)指定有限维概率。耦合界限目标结合了矩阵边际和过程在相遇时间后一致的显式条件。强平稳时间目标则利用联合法则和停时条件，将停时处的状态与之后确定时间处的状态联系起来。这些表示指明了证明器可用的关于过程的哪些信息。

**形式化范围**。一些问题需要Mathlib环境中不可用的基础设施。*直接*目标使用Mathlib对象或共享定义，而*抽象化*目标则将所需属性作为假设。JSON记录分别将这些标签记为`literal`和`abstract`。提供的属性可能定义了一个对象或提供了来自源问题的中间结果。这是不同的选择：指定布朗运动的性质并不假设二次变差结论，而假设无记忆性则消除了从连续时间链动力学推导它的需要。同样，通过第一步方程陈述的命中时间目标无需建立其解等于路径期望命中时间。

**路径性质与收敛**。目标明确陈述了所需形式的收敛。布朗运动性质通过高斯增量定律、独立性和几乎处处路径连续性来表达；多个目标将这些性质封装在局部`IsBM`定义中。二次变差目标要求当分割网格趋于零时均方误差的收敛。Donsker目标要求对C([0,T], ℝ)上的每个有界连续泛函的期望收敛，而不仅仅是在单个时间点的收敛。另一个单独的目标要求在连续路径空间上Wiener测度的存在性和唯一性。

**人工审核与发布**。我们根据源问题审核了定义和假设，但它们将受益于进一步的同行评审。Lean验证了每个完成的证明都在声明的假设下确立了其结论；源审核则评估定义和假设是否代表了预期的问题。每个JSON记录包含一个标识符、问题名称、非形式陈述、Lean目标和表示标签。我们还发布了共享定义和基线证明尝试。该发布是一系列定理目标的集合，而非声称所有目标都有完整证明。基线证明检查和结果在第4节描述。

表1：StochBench的语料库构成和基线结果（记录的证明时间最多为15分钟）。仅计入记录证明时间不超过900秒的证明。主题比率使用该主题中的所有项目；类别比率使用该类别中的所有项目。类别比较是描述性的，而非受控的因果效应。

## 4 评估
我们使用`lean4skills`和Lean LSP MCP服务器评估了一个基于Opus 4.8的、使用多轮工具的智能体（Freer, 2025; Dressler, 2025）。每个目标运行一次，上限为15分钟，允许进行Lean错误检查、库和共享定义搜索、loogle和leansearch查询以及证明修订。相同的模型系列协助了陈述构建。这是一个单智能体、单预算的基线，而非模型比较或重复运行评估。该智能体在450个目标中产生了157个干净的证明。如果Lean接受证明且不含`sorry`、`sorryAx`或额外的被承认事实，则该证明是*干净的*，由Lean比较器检查。表1和表1（应为图1，可能原文有误）报告了主题和类别细分。这些是描述性比较：它们没有区分抽象化效应与问题差异或库支持差异。定性检查发现了在看似合理的目标上的证明搜索失败、缺失的引理或困难的库接口，以及一小部分形式化缺陷，包括缺失可测性、可积性或非空性假设。

## 5 局限性与结论
我们注意到，StochBench的问题策展、忠实度审查及其主题和直接/抽象化分类目前由人类策展者决定，引入了一些偏差；因为相应的术语在本工作的范围内未被严格定义。尽管存在这些局限，StochBench为评估研究生随机过程证明智能体提供了一个集中的测试平台。其新构建的非形式-形式配对可以支持自动形式化训练，而成功检查的基线证明为证明生成提供了监督。连同共享定义，这些