发表机构
Shanghai Jiao Tong University; Shanghai Innovation Institute（上海交通大学; 上海创新研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
ProofGap是一个细粒度基准，通过将自然语言解答分解为局部证明缺口，评估模型在数学分析中的逐步形式推理能力，以更精确地定位模型失败。
AI 中文摘要
现有的形式数学基准，如miniF2F、ProofNet和PutnamBench，主要评估模型为具有挑战性的问题构建完整形式证明的能力。由于成功是在定理层面衡量的，这些基准对模型逐步形式推理能力的洞察有限。单独评估这一能力，能够比仅进行定理级评估更精细地诊断模型局限。为填补这一评估空白，我们引入了ProofGap，一个用于逐步形式推理的细粒度基准。ProofGap通过一个自然语言证明处理流水线构建，该流水线将每个推理步骤分解为一个或多个对齐的证明缺口。将此流水线应用于B. P. Demidovich的《数学分析习题集》中3,015道习题的自然语言解答，产生了26,116个缺口。该基准聚焦于数学分析，这一领域对当前模型仍具挑战性。通过显式提供局部上下文和目标，缺口补全将局部形式证明构建与端到端证明组合分离开来，从而能够更精确地定位模型失败。自然语言解答作为这些义务的来源，而基准任务本身则从已形式化的局部上下文和目标开始。除基准测试外，相同的流水线可能支持未来的证明验证系统，前提是语义翻译和顺序证明组合能被可靠处理。
英文摘要
Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited insight into models' step-level formal reasoning. Evaluating this capability separately enables finer-grained diagnosis of model limitations than theorem-level evaluation alone. To fill this evaluation gap, we introduce ProofGap, a fine-grained benchmark for step-level formal reasoning. ProofGap is constructed through a natural-language proof-processing pipeline that decomposes each reasoning step into one or more aligned proof gaps. Applying this pipeline to natural-language solutions to 3,015 exercises in B. P. Demidovich's Problems in Mathematical Analysis yields 26,116 gaps. The benchmark focuses on mathematical analysis, a domain that remains challenging for current models. By supplying the local context and target explicitly, gap completion isolates local formal proof construction from end-to-end proof composition, enabling more precise localization of model failures. Natural-language solutions serve as the provenance of these obligations, while the benchmark task itself starts from an already formalized local context and goal. Beyond benchmarking, the same pipeline may support future proof-verification systems, provided that semantic translation and sequential proof composition are handled reliably.
