ExamFormal-Bench
收藏魔搭社区2025-11-26 更新2025-11-22 收录
下载链接：
https://modelscope.cn/datasets/iflytek/ExamFormal-Bench
下载链接
链接失效反馈官方服务：
资源简介：
###### **ExamFormal-Bench**
We introduce ExamFormal-Bench, which is a benchmark for formal proof generation. It begins with a large-scale question bank, built by collecting problems across middle school, high school, and undergraduate academic levels from exams and competitions, processed via manual OCR. These problems are systematically classified into a structured knowledge taxonomy, including Analysis, Geometry, Algebra, Probability \\\& Statistics, Computational Mathematics, and Discrete Mathematics. The complete question bank is formed by drawing problems from each of these top-level categories. The final test set contains 402 problems.
###### **Information**
**Language:** Lean4
**Content:** id, natural\_language, formal\_statement
## License Agreement
ExamFormal-Bench is licensed under Apache 2.0.
###### **ExamFormal-Bench**
我们提出了ExamFormal-Bench，这是一款面向形式化证明生成的基准测试集。该数据集以大规模题库为基础：通过人工光学字符识别（Optical Character Recognition, OCR）技术，收集自中学、高中及大学本科阶段的各类考试与竞赛试题。
这些试题被系统性归类至结构化的知识分类体系中，涵盖分析学、几何学、代数学、概率论与统计学、计算数学以及离散数学六大顶级类目。完整题库通过从上述各顶级类目下抽取试题整合而成，最终测试集共包含402道试题。
###### **Information**
**语言**：Lean4
**内容**：id、自然语言（natural language）、形式化陈述（formal statement）
## License Agreement
ExamFormal-Bench 采用Apache 2.0许可协议进行授权。
提供机构：
maas
创建时间：
2025-11-17
