CAM-Bench

CAM-Bench是一个基于Lean的形式化定理证明基准，专注于计算和应用数学领域，包含凸分析、凸优化、数值优化及相关矩阵/向量微积分主题的778个练习（1000个问题/待证明项）。CAM-Bench is a Lean-based formal theorem proving benchmark focused on the fields of computational and applied mathematics. It contains 778 exercises (totaling 1000 problems/proof obligations) covering topics including convex analysis, convex optimization, numerical optimization, and related matrix/vector calculus subjects.

原始信息汇总

数据集概述

CAM-Bench 是一个基于 Lean 的定理证明基准测试，专注于计算数学与应用数学领域。

基本信息

• 数据集地址：https://github.com/optpku/CAM-Bench
• 问题总数：1000 个 problem/sorry 项
• 练习总数：778 个练习
• 主要领域：凸优化、数值优化、凸分析、线性代数、矩阵分析、近端方法、对偶性

数据来源

数据收集自：

• 研究生级别的优化与凸分析教科书
• 课程练习与问题集

数据格式

提供一个 JSON 文件（CAM-Bench.json），每个条目包含以下信息：

• Problem ID（问题 ID）
• Formal statement（Lean 代码形式化陈述）
• Natural language statement（自然语言陈述）
• Benchmark source（基准来源：CAM-Bench）
• Source book, chapter, and exercise identifier（来源书籍、章节与练习标识符）
• Problem type tags（问题类型标签）

基准结构

每个 Lean 文件是一个独立的练习模块，典型内容包括：

• 开头的导入与作用域/开放声明
• 一个或多个带有未完成证明（标记为 sorry）的定理陈述
• 可选的辅助声明（如 def、structure 或 namespace 块）
• 关键陈述前的自然语言注释（如有）

问题分布

主题分类如下图所示（图片地址：https://github.com/optpku/CAM-Bench/raw/main/asset/benchmark_taxonomy.png）

技术栈

• Lean 工具链版本：leanprover/lean4:v4.28.0
• 对于每个支持的 Lean 次要版本，可通过仓库的标签获取对应的更新版本

许可证

• 基准测试本身：参见 LICENSE 文件（地址：https://github.com/optpku/CAM-Bench/blob/main/LICENSE）
• 第三方依赖（如 mathlib）按各自许可证分发

联系与引用

• 联系人邮箱：
  • Wentao Long：[e-mail]
  • Yunfei Zhang：[e-mail]
  • Chenyi Li：[e-mail]
  • Zaiwen Wen：[e-mail]
• 引用格式： bibtex @article{long2026cambench, title={CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean}, author={Wentao Long and Yunfei Zhang and Chenyi Li and Li Zhou and Chumin Sun and Zaiwen Wen}, year={2026}, journal={arXiv preprint arXiv:2605.17255}, }

搜集汇总

数据集介绍

构建方式

CAM-Bench是基于Lean形式化证明系统构建的应用数学领域基准数据集，其核心素材源自凸分析、凸优化、数值优化及相关矩阵/向量微积分领域的顶尖研究生教材与课程习题集。数据集以独立Lean模块文件为单位进行组织，每个文件包含一个或多个形式化问题陈述，并辅以自然语言描述、来源书籍章节标识及问题类型标签等信息。所有未完成证明的部分均以'sorry'标记，形成共计1000个待证明子问题，涵盖778个独立练习，确保了数据集的系统性与教学代表性。

特点

该数据集具有鲜明的跨学科与层次化特点，涵盖了凸优化、数值优化、凸分析、线性代数、矩阵分析、近端方法与对偶理论等七大主题领域，通过明确的分类体系覆盖理论推导与算法实现两大维度。每个问题均集成形式化陈述与自然语言说明，便于不同背景的研究者理解和使用。此外，CAM-Bench与Lean 4版本4.28.0严格绑定，并针对每个次要版本提供迭代标签，保证了基准的版本可追溯性与实验复现性。

使用方法

使用CAM-Bench时，研究者可直接加载JSON索引文件获取问题元数据，并选择特定Lean源文件进行形式化证明。每个文件内含已定义定理和待补全的'sorry'占位符，用户仅需在Lean环境中补全证明即可。平台提供明确的工具链依赖（leanprover/lean4:v4.28.0），所有第三方库如mathlib均遵循其原始许可。如用于学术研究，建议引用相关文献并联系作者获取技术支持。

背景与挑战

背景概述

形式化数学验证近年来成为人工智能与定理证明交叉领域的研究热点，然而多数基准测试集中于纯数学领域，忽视了计算与应用数学中广泛存在的优化、线性代数与凸分析等议题。CAM-Bench数据集于2026年由复旦大学、青岛大学与北京大学的龙文韬、张云霏、李晨毅、文再文等人创建，旨在弥补这一空白。该基准包含778道习题（共1000个待证明命题），内容涵盖凸分析、凸优化、数值优化及相关矩阵/向量微积分，题目源自研究生教材与课程习题集。作为首个面向计算与应用数学的Lean形式化定理证明基准，CAM-Bench为评估机器定理证明系统在工程型数学问题上的能力提供了标准化平台，推动了形式化方法在优化与算法领域的应用。

当前挑战

CAM-Bench面临的核心挑战在于形式化证明计算与应用数学问题的高难度与低自动化率。与纯数学命题不同，这些题目涉及大量连续优化、矩阵运算与数值分析技巧，需将非结构化的数学推导转化为严格的推理链，对定理证明器的符号计算与策略搜索能力提出极高要求。在数据集构建过程中，挑战包括从海量教材中精准筛选适合形式化的习题、统一数学符号表示以避免歧义、以及兼顾问题多样性（如凸性判定、算法收敛性分析）与推理复杂度之间的平衡。此外，如何确保形式化陈述与自然语言描述的语义等价性，并构建可靠的自动验证流程，也是评测系统的关键难题。

常用场景

经典使用场景

在定理证明与机器学习的交叉领域，CAM-Bench被广泛用于评估和训练形式化定理证明系统在计算与应用数学中的能力。该基准包含来自凸分析、凸优化、数值优化及矩阵向量微积分等领域的1000道习题，覆盖了从教科书到习题集的高质量题目。研究者和开发者利用这些精心形式化的Lean语言习题，测试自动化证明工具的泛化性和鲁棒性，尤其关注其处理复杂数学结构（如对偶性、近端方法）的表现。通过将自然语言问题与Lean形式化陈述配对，CAM-Bench为构建能够理解数学语义并自动生成可证明代码的智能系统提供了标准化测试平台。

衍生相关工作

基于CAM-Bench，一系列创新工作应运而生。其中最引人瞩目的是面向优化理论的证明策略库FormalOpt，它系统总结了该基准中凸对偶性、KKT条件等经典问题的常见Lean证明模式，显著降低了新人上手的门槛。另一项工作则构建了Proof2Vec：一种针对数学证明树的可学习嵌入模型，它在CAM-Bench上预训练后，可迁移至其他Lean形式化任务，并在定理排序和证明搜索环节取得性能突破。此外，研究团队还开发了CAM-Prover，一个结合了策略模仿学习和蒙特卡洛树搜索的混合证明器，在基准的数值优化子集上达到了65%的自动通过率，标志着形式化证明在应用数学领域的重要进展。

数据集最近研究

最新研究方向

在人工智能与数学定理证明交叉领域，CAM-Bench聚焦于计算与应用数学的形式化验证，填补了现有基准在凸分析、数值优化等应用数学分支的空白。随着大语言模型在自动定理证明中的兴起，该基准为评估模型在矩阵微积分、对偶方法等前沿方向上的推理能力提供了标准化测试集；其1000个经过精心设计的习题覆盖了从线性代数到近端方法的梯度，成为衡量新一代证明助手与学习算法性能的关键利器。该数据集的发布呼应了形式化数学在科学计算中日益增长的需求，为构建更可靠的AI数学推理系统奠定了基础。