想象一场“国际乐高数学锦标赛”：主办方发给你一本图纸合集，每张图纸画着一道数学竞赛作品的规格，要求你用标准积木搭出一座能让质检机逐块验收的结构。这场考试的奇妙之处在于——参赛选手不是人类，而是 AI。图纸是自然语言的数学题，积木是数学证明步骤，而那座严苛的质检机，就是 Lean、Isabelle 这样的形式化证明助手。这套官方题库，就叫 MiniF2F。 AI 很擅长“报答案”，却常常说不清理由。MiniF2F 专门挑战这件事：模型必须把自然语言题目翻译成形式化陈述，再产出一条机器可验证的完整证明链。答案是抄不来的，图纸上的每个承诺都要用积木实打实兑现，质检机才不会放过任何一处“大约是对的”的模糊表述。这篇文章，我们跟着一位 AI 搭建师的视角，从认识图纸库、看懂质检员、学习裁判手册，到钻研搭建策略、翻看成绩单、请教教练团队，把 MiniF2F 形式化数学这场锦标赛的里里外外看个明白。

岗位关联

对 AI 从业者来说，掌握 MiniF2F 的评测机制与证明搜索方法，意味着你能用“机器可验证”的硬标准设计模型数学能力评估，在模型选型、发布与迭代时拿出真正可信的推理证据。

目录
  1. 可视化演示
  2. 图纸库：认识 MiniF2F 这座乐高锦标赛题库
  3. 质检员：Lean 证明助手与它的放大镜
  4. 裁判手册：如何给 AI 的搭建能力打分
  5. 搭建策略师：AI 选手的解题算法
  6. 成绩单：现在的 AI 能搭出什么水平的塔
  7. 教练团队：优化策略与工程落地
  8. AI 应用场景
  9. Python 演示
  10. 常见误区
  11. 面试题

可视化演示

演示形式化数学定理证明评测基准MiniF2F：工作流展示自然语言题转化为形式化陈述、生成证明代码、证明助手编译验证的流程；证明搜索展示定理树的分支搜索与命中路径；数据集展示validation/test子集各244题的评测统计。

本节配有交互动效（进入视口后自动加载，约 3KB）。

五步验证流程 自然语言题→形式化陈述→证明代码→助手验证 Lean/Isabelle/Metamath 机器可验证确保结果客观可信

图纸库：认识 MiniF2F 这座乐高锦标赛题库

想象你走进一座巨大的仓库，里面摆满了层层叠叠的图纸。每一张图纸都是一道数学竞赛题的“规格说明书”：它用自然语言描述目标，比如“证明 0 是自然数加法的右单位元”，但真正交付时，你必须用形式化积木搭出完整的证明结构。这一仓库图纸，正是 MiniF2F 基准测试的数据集——它从 AIME、AMC 等国际奥林匹克级别的数学竞赛中精选题目，整理成跨系统一致的形式化版本。

MiniF2F 的“Mini“指的是它刻意控制题量，让研究者可以快速迭代评测；”F2F“则强调”从自然语言到形式语言”的面对面翻译挑战。它不只考察 AI 会不会算出最终答案，更考察 AI 能不能把自然语言题目翻译成 Lean、Isabelle 等证明助手能读懂的形式化陈述，并补上完整的证明步骤。题型覆盖代数、数论、组合与不等式，难度从入门级竞赛一路延伸到国际奥赛决赛水平。

这就是 MiniF2F 的核心评测目标：判断模型的形式化证明生成能力，而非简单的答案正确率。它希望每道题都留下一条“机器可查验”的完整推理痕迹：

把图纸库里的每一张图纸走完一遍，AI 就完成了一次“数学体检”。题目从简到难递进，验证器从始至终不近人情——这正是 MiniF2F 作为基准最珍贵的品质。

PassRate=1N∑i=1NI[V(πi)=true]\displaystyle \text{PassRate} = \frac{1}{N} \sum_{i=1}^{N} \mathbb{I}\left[ V\left( \pi_i \right) = \text{true} \right]
这个公式是说：一共有 N 道题，把每道题 AI 给出的证明放进验证器 V 里检查，通过了就记 1 分，最后除以 N 得到整体通过率。
  1. 题目编号 i遍历题库中的全部 N 道题，就像把锦标赛的 N 张图纸逐一翻看。
    i∈{1,2,…,N}\displaystyle i \in \{1, 2, \ldots, N\}
  2. 候选证明 πᵢAI 为第 i 题搭建出的“积木塔”，即一整套形式化证明步骤序列。
    πi=[tactic1,tactic2,…,tacticn]\displaystyle \pi_i = [\text{tactic}_1, \text{tactic}_2, \ldots, \text{tactic}_n]
  3. 验证器 V(·)Lean 的质检内核，逐块检查积木塔的每个咬合点是否符合推理规则。
    V(πi)∈{true,false}\displaystyle V(\pi_i) \in \{\text{true}, \text{false}\}
  4. 示性函数 I[·]条件成立记 1，不成立记 0，相当于裁判当场举旗——过了还是没过。
    I[V(πi)=true]={1通过0未通过\displaystyle \mathbb{I}[V(\pi_i) = \text{true}] = \begin{cases} 1 & \text{通过} \\ 0 & \text{未通过} \end{cases}
  5. 求和取平均把所有“举旗”加总再除以 N，得到这位 AI 选手在该赛季的整体通过率。
    1N∑i=1N(⋯ )\displaystyle \frac{1}{N}\sum_{i=1}^{N} (\cdots)

质检员：Lean 证明助手与它的放大镜

假设你是那位 AI 搭建师，搭好一座积木塔后，真正让你紧张的环节来了：一台名为 Lean 的质检机缓缓启动，它的放大镜会把塔上每一块积木的编号、咬合方式、承重计算全部扫描一遍。只要有一块积木接缝不合规，整座塔就会被标记为不合格。Lean 就是这样一台铁面无私的形式化验证器，由微软研究院开发，是 MiniF2F 最常用的证明助手之一。

Lean 的核心是一个内核（kernel），它只做一件事：机械地检查每个证明步骤是否符合类型论规则，绝不容忍任何“显而易见”的跳步。操作上，模型通过一系列 tactic（战术）与证明助手交互：每个 tactic 都像一种搭积木的手法——“apply“是把某块积木按上去，”intro“是拆开一个目标露出内部结构，”rewrite”是把某块积木替换成等价的另一块。所有 tactic 按顺序执行，就像施工单一样逐步改变当前证明状态。

一个证明状态可以写成这样的“施工牌”：

除了内核验证，Lean 还提供策略搜索空间：当前状态可能适用多个 tactic，每个 tactic 又会生成新的子目标，于是证明过程变成了一棵不断分叉的状态树。AI 需要在这棵树里寻找一条通往“所有目标闭合”的路径——就像搭建师在无数可能的搭法中找出唯一能通过质检的施工顺序。

Γ⊢e:P\displaystyle \Gamma \vdash e : P
读作“在上下文 Γ 下，表达式 e 是命题 P 的一个证明”。Lean 内核的工作，就是逐层确认这张施工牌是否真的成立。
  1. 上下文 Γ当前工地上已摆放好的积木与规范集合——已有的假设、变量和公理。
    Γ={H1:A,  H2:B,…}\displaystyle \Gamma = \{H_1 : A, \; H_2 : B, \ldots\}
  2. ⊢ 符号左边资源足以推出右边，表达“必然能搭出来”的推导关系。
    Γ⊢⋯\displaystyle \Gamma \vdash \cdots
  3. 表达式 e待检验的那块积木——一个具体的证明构造（lambda 项或 tactic 执行结果）。
    e:Proof_Term\displaystyle e : \text{Proof}\_\text{Term}
  4. 命题 P积木上标注的规格，它声称自己证明了哪个结论。
    P:Prop\displaystyle P : \text{Prop}
  5. 整体含义在假设堆 Γ 的支持下，构造 e 可以充当规格为 P 的零件；Lean 内核递归确认这条“搭积木许可”。
    Γ⊢e:P\displaystyle \Gamma \vdash e : P

裁判手册：如何给 AI 的搭建能力打分

有了质检机，裁判的工作就简单了吗？不，真正的难题在于“怎么打分才公平”。如果只给 AI 一次机会，它可能因为运气不好搭歪了一块；如果给无限次机会，分数又会虚高。于是裁判手册上写了一条重要规则：Pass@k——允许 AI 对同一张图纸尝试 k 次，只要 k 次里有任意一次通过了质检，就算这道题得分。

这就像乐高比赛的“三次试搭规则”：选手可以快速试搭 k 座塔，裁判逐一送进质检机，只要有一座塔通过验收即判成功。Pass@1 反映模型“一次成型”的稳定实力，Pass@k 则反映模型在多轮采样与搜索下的潜力。此外，裁判还会对题目做难度分层统计：简单竞赛题、奥赛初赛题、IMO 决赛题分别计算通过率，避免简单题拉高总分的假象。

评估体系里还有一个容易忽略的环节：与人类对比。裁判手册要求同时记录人类解题所需步数和模型证明长度，从而衡量模型是否在“绕远路”。MiniF2F 的目标从来不是让模型的分数追平人类，而是让“机器可验证的证明能力”成为一项可追踪、可复现的硬指标。

Pass@k=E[max⁡1≤j≤kI[V(πj)=true]]\displaystyle \text{Pass@}k = \mathbb{E}\left[ \max_{1 \le j \le k} \mathbb{I}\left[ V\left( \pi_j \right) = \text{true} \right] \right]
这个公式给出的是“给 k 次机会时的平均成功率”：k 个候选证明里只要有一个通过验证，该题就算命中。
  1. 采样编号 jAI 对同一张图纸快速搭 k 次，得到 k 座候选积木塔。
    j∈{1,2,…,k}\displaystyle j \in \{1, 2, \ldots, k\}
  2. 逐个质检把每座塔都放进 V 中过一遍质检机，通过记 1，不通过记 0。
    I[V(πj)=true]\displaystyle \mathbb{I}[V(\pi_j) = \text{true}]
  3. 取最大值k 座塔中只要至少有一座通过质检，结果就是 1——这一题成功命中。
    max⁡1≤j≤k(⋯ )\displaystyle \max_{1 \le j \le k} (\cdots)
  4. 期望 E对大量题目重复这个过程，得到“给 k 次机会时的平均成功率”。
    E[⋯ ]\displaystyle \mathbb{E}[\cdots]
  5. 对比解读Pass@1 是“一次成型率”，Pass@3、Pass@5 则反映“多试几次的搜索潜力”；两者差距越大，说明模型越依赖“蒙得多”而不是“蒙得准”。
    Gapk=Pass@k−Pass@1\displaystyle \text{Gap}_{\text{k}} = \text{Pass@}k - \text{Pass@}1

搭建策略师：AI 选手的解题算法

现在轮到 AI 选手本人登场。它站在图纸前，第一步是读懂图纸：把自然语言题目翻译成形式化目标。这一步被称为非形式化到形式化的翻译，通常由预训练语言模型完成，输出像 ∀ m : ℕ, m + 0 = m 这样严谨的谓词。翻译一旦出错，后面搭得再漂亮也是空中楼阁。

第二步，AI 化身搭建策略师，在 Lean 给出的战术状态树上搜索。它可能会用贪心搜索、束搜索（beam search）或 best-first 搜索：每个候选 tactic 对应一个分支，模型给每个分支打分，优先扩展最有希望的路线。就像搭建师手里拿着一张“可能性地图”，每次都挑最像能通向 QED 的方向走。走不通就回溯，换一种手法。

为了让策略更聪明，研究者引入了强化学习：把“成功证明一道题”当作奖励信号，让模型在大量试错中调整策略。证明成功给正奖励，走弯路不惩罚，最终目标是最大化长期回报：

在训练环节，大规模预训练功不可没：模型先在互联网语料上学会自然语言与代码的分布，再在 Lean 社区积累的证明语料上微调，最后用强化学习在 MiniF2F 题目上提升策略。每一步都让策略师手里的“可能性地图”更加精确。

∇θJ(θ)=Eτ∼πθ[∑t=1T∇θlog⁡πθ(at∣st)R(τ)]\displaystyle \nabla_\theta J(\theta) = \mathbb{E}_{\tau \sim \pi_\theta}\left[ \sum_{t=1}^{T} \nabla_\theta \log \pi_\theta\left( a_t \mid s_t \right) R(\tau) \right]
这是策略梯度更新公式：AI 用“哪一步动作让最终证明成功的概率变大”来调整自己的决策网络。
  1. 轨迹 τ一场完整的搭建过程，包含状态 sₜ 和动作 aₜ 的序列。
    τ=(s1,a1,s2,a2,…,sT,aT)\displaystyle \tau = (s_1, a_1, s_2, a_2, \ldots, s_T, a_T)
  2. 参数 θ策略网络权重，决定看到某个证明状态时倾向选哪种 tactic。
    θ∈Rd\displaystyle \theta \in \mathbb{R}^{d}
  3. 对数概率 log πθ当前策略对某个具体动作的“顺手程度”。
    log⁡πθ(at∣st)\displaystyle \log \pi_\theta(a_t \mid s_t)
  4. 奖励 R(τ)质检结果折算的分数——证明成功给正奖励，失败给零分。
    R(τ)=I[V(πθ)=true]\displaystyle R(\tau) = \mathbb{I}[V(\pi_\theta) = \text{true}]
  5. 梯度上升更新把“顺手的、导向成功的”动作方向不断调强，像教练复盘时反复强调精彩过法。
    θ←θ+α∇θJ(θ)\displaystyle \theta \leftarrow \theta + \alpha \nabla_\theta J(\theta)

成绩单：现在的 AI 能搭出什么水平的塔

打开 AI 选手的赛季成绩单，你会发现一个鲜明规律：简单重写题目的通过率已经相当可观，但设计精巧、需要创造性构造的 IMO 级别难题，成功率依然低得令人沮丧。从 2021 年 GPT-f 只能证明题库中的一小部分题目，到最近大模型结合工具调用与搜索，通过率已经有了数量级提升——但赛程远未结束。

典型的失败模式有三种。第一，搜索空间爆炸：证明状态树随题目难度指数膨胀，模型在有限预算内找不到那条唯一通路，就像搭到一半发现积木种类不够，只能空手而归。第二，缺乏创造性构造：许多奥赛题需要引入一个“从天而降”的辅助线或中间引理，模型不知道该怎么凭空造出那块关键积木。第三，证明链过长：步骤越多误差累积越严重，任何一步的微弱偏差都可能让整座塔在质检时轰然倒塌。

研究者用一个量化的指标描述“会做却说不出”的困境——形式化鸿沟：

成绩单背面还写着两行小字：计算成本与数据泄漏风险。一次完整评估要调用模型做成千上万次 tactic 预测，GPU 开销不容小觑；而 MiniF2F 的题目来自公开竞赛，很可能混入预训练语料——模型可能不是“会做题”，而是“背过答案”。

Gap=Anl−AformalAnl\displaystyle \text{Gap} = \frac{A_{\text{nl}} - A_{\text{formal}}}{A_{\text{nl}}}
这个公式衡量的是：AI 能用自然语言把解题思路讲清楚，却无法把它翻译成机器可验证的形式化证明——这种“嘴到手指没到”的落差有多大。
  1. A_nlAI 用自然语言直接解题的正确率——相当于口头说“我懂怎么搭”。
    Anl=自然语言解题正确数总题数\displaystyle A_{\text{nl}} = \frac{\text{自然语言解题正确数}}{\text{总题数}}
  2. A_formalAI 真正交出形式化证明并通过质检的比例——相当于“真搭出来了”。
    Aformal=形式化证明通过数总题数\displaystyle A_{\text{formal}} = \frac{\text{形式化证明通过数}}{\text{总题数}}
  3. 分子差能说会道却搭不出来的题目数，即“认知”与“交付”之间的落差。
    Anl−Aformal\displaystyle A_{\text{nl}} - A_{\text{formal}}
  4. 分母归一用口头正确率当基准，量化鸿沟占口头能力的比例。
    ⋯Anl\displaystyle \frac{\cdots}{A_{\text{nl}}}
  5. 解读Gap 越大，说明模型的“解题思路”越没有真正落到“形式化执行”层面，距离可靠的自动化数学证明也就越远。
    0≤Gap≤1\displaystyle 0 \le \text{Gap} \le 1

教练团队：优化策略与工程落地

面对这样一份成绩单，AI 团队里的“教练组”坐不住了。他们的第一招是数据增强：把大量非形式化的数学解法自动翻译成形式化证明，合成新的“训练图纸”；再让模型自己尝试解题，把成功的证明和失败的反例都收集起来，扩充训练集。这就像给选手准备了一座更大的积木仓库，里面既有经典示范作品，也有踩坑实录。

第二招是课程学习：不让选手一上来就挑战 IMO 压轴题，而是从“证明 0+0=0”这类热身题开始，逐步把题目难度曲线拉高。模型在简单题上建立扎实的基本功后，再面对复杂题目时，搜索策略会更加稳健，不会一上来就在大空间里乱撞。

教练组还会调整混合训练目标，同时利用“标准示范”和“自我实战”两种信号：

落到工程实践，搭建一套规范的 MiniF2F 评估流程至少要四步：先固化题目翻译管线，保证同一道题在多次评测中形式化目标一致；再设定统一的采样数量和随机种子；然后用验证器自动判定而非人工阅卷；最后按难度分层输出 Pass@1 与 Pass@k，并明确标注数据泄漏防护措施。结果解读规范同样重要：一份可信的评测报告必须区分“模型真的会证明”与“模型在搜索空间里撞运气”，否则很容易被漂亮的分数误导。

L(θ)=Lformal(θ)+λ Lself-play(θ)\displaystyle \mathcal{L}(\theta) = \mathcal{L}_{\text{formal}}(\theta) + \lambda \, \mathcal{L}_{\text{self-play}}(\theta)
这是一个组合损失：前半部分让模型模仿人类已有的优秀证明，后半部分让模型从自己的试错反例中学习，λ 控制两者的权重。
  1. L_formal在已有标准证明（历史优秀乐高作品）上做监督学习的损失。
    Lformal(θ)=−E[log⁡pθ(证明∣题目)]\displaystyle \mathcal{L}_{\text{formal}}(\theta) = -\mathbb{E}\left[\log p_\theta(\text{证明} \mid \text{题目})\right]
  2. λ调节“教练带教”与“自主实战”份量的超参数。
    λ∈[0,1]\displaystyle \lambda \in [0, 1]
  3. L_self-play让策略师自我对战、从失败证明中学习的损失项。
    Lself-play(θ)=−E[log⁡pθ(成功∣状态)]\displaystyle \mathcal{L}_{\text{self-play}}(\theta) = -\mathbb{E}\left[\log p_\theta(\text{成功} \mid \text{状态})\right]
  4. 总损失 L两项损失加权求和，梯度下降让模型在两种信号下同步进步。
    θ←θ−η∇θL(θ)\displaystyle \theta \leftarrow \theta - \eta \nabla_\theta \mathcal{L}(\theta)
  5. 调参要点λ 过大容易激进失衡，过小又进步缓慢——需要像教练安排训练量一样反复调参。
    λ=arg⁡max⁡  Pass@k(θ)\displaystyle \lambda = \arg\max \; \text{Pass@}k(\theta)

AI 应用场景

大模型发布前的“数学单科体检”

阶段：模型评估与基准测试

解决的问题：传统人工出题加人工阅卷主观且昂贵，很难精确衡量模型的数学推理能力。MiniF2F 的验证器自动判定证明对错，杜绝“答案对但过程错”的漏网之鱼。

具体案例：某公司训练完新一代基座模型后，在 MiniF2F 测试集上独立采样 5 轮，计算 Pass@1 和 Pass@5，把结果写进技术报告。若发现 Pass@1 下降但 Pass@5 上升，说明模型“想得更多但一次成型变差”，团队据此调整强化学习的奖励设置。

数学教育平台的步骤级批改

阶段：推理与辅助决策

解决的问题：传统自动批改只比对最终答案，无法判断学生的推理链是否完整。形式化验证器能把解题过程变成机器可检查的证明状态，精确定位到是哪一步跳过了必要论证。

具体案例：面向高中生的自适应学习平台接入 Lean 验证器：学生用自然语言写完解题步骤后，后台的翻译模型先把步骤转为形式化目标，再交给验证器逐步检查。系统据此给出“你在第 3 步跳过了分类讨论”这样具体的反馈。

工业级形式化验证的证明补全

阶段：部署与集成

解决的问题：芯片设计、区块链协议等领域需要形式化验证保障安全，但人工编写证明极贵。MiniF2F 训练出的证明搜索模型能自动补全证明脚本，让人工专家只审查大纲。

具体案例：某区块链团队使用自适应证明搜索模型，为智能合约的不变量定理补全 Isabelle 证明；原本需要两周的验证工作缩短到两天，人工审查时只需关注模型生成的引理拆分是否合理。

Python 演示

python98 行
# -*- coding: utf-8 -*-"""迷你 MiniF2F：自然语言题目翻译、形式化证明搜索与 Pass@k 评估"""import random random.seed(42) # 题目库: (自然语言题目, 形式化目标对)PROBLEMS = [    ("证明 0 + 0 = 0", (('+', '0', '0'), '0')),    ("证明 S(0) + S(0) = S(S(0))", (('+', ('S', '0'), ('S', '0')), ('S', ('S', '0')))),    ("证明 (0 + (0 + 0)) + 0 = 0", (('+', ('+', '0', ('+', '0', '0')), '0'), '0')),] # 重写规则库, 对应 Lean 中的简化 tacticRULES = [    (('+', '0', 'n'), 'n'),                            # zero_add    (('+', ('S', 'm'), 'n'), ('S', ('+', 'm', 'n'))),  # succ_add    (('+', 'm', '0'), 'm'),                            # add_zero] def matches(expr, pat, env):    if isinstance(pat, str) and pat.islower():        env[pat] = expr        return True    if expr == pat:        return True    return isinstance(expr, tuple) and isinstance(pat, tuple) \        and len(expr) == len(pat) \        and all(matches(e, p, env) for e, p in zip(expr, pat)) def subst(term, env):    if isinstance(term, str):        return env.get(term, term)    return tuple(subst(t, env) for t in term) def rewrite_once(expr):    """对一个表达式的所有位置尝试所有规则, 返回一步重写后的结果集合"""    out = []    for pat, repl in RULES:        env = {}        if matches(expr, pat, env):            out.append(subst(repl, env))    if isinstance(expr, tuple):        for i in range(len(expr)):            for sub in rewrite_once(expr[i]):                child = list(expr)                child[i] = sub                out.append(tuple(child))    return list(dict.fromkeys(out))  # 去重 def verify(proof, goal):    """质检员: 依次检查证明链每步是否合法, 且最终状态等于目标"""    if not proof or proof[-1] != goal:        return False    for a, b in zip(proof, proof[1:]):        if b not in rewrite_once(a):            return False    return True def search_proof(start, goal, budget=150):    """BFS + 随机出队模拟模型的随机策略采样"""    queue = [(start, [start])]    seen = {start}    while queue and budget > 0:        budget -= 1        idx = random.randrange(len(queue))        cur, path = queue.pop(idx)        if cur == goal:            return path        for nxt in rewrite_once(cur):            if nxt not in seen:                seen.add(nxt)                queue.append((nxt, path + [nxt]))    return None def pass_at_k(problems, k):    """对每道题采样 k 个候选证明, 只要有一个通过验证就算命中"""    hits = 0    for nl, (start, goal) in problems:        ok = False        for _ in range(k):            proof = search_proof(start, goal, budget=random.randint(30, 200))            if proof is not None and verify(proof, goal):                ok = True                break        hits += int(ok)    return hits / len(problems) if problems else 0.0 def main():    print("== 迷你 MiniF2F 形式化数学评测 ==")    for nl, (start, goal) in PROBLEMS:        print("题目:", nl)        print("  -> 形式化目标:", start, "=", goal)    for k in (1, 3, 5):        print("Pass@%d = %.2f" % (k, pass_at_k(PROBLEMS, k))) if __name__ == '__main__':    main()
目的：用一个小型的等式重写系统模拟 MiniF2F 的完整链路——题目翻译、形式化证明搜索、验证器检查与 Pass@k 采样评估。
  1. PROBLEMS = [...]题目库：每条题目同时保存自然语言表述与形式化目标对，对应“非形式化翻译”的产物。
  2. RULES = [...]三条重写规则充当 tactic 库，相当于 Lean 里的简化战术。
  3. matches(expr, pat, env)模式匹配函数，检查某块积木是否适用某条搭建手法。
  4. rewrite_once(expr)一点重写：穷举所有可应用规则的位置，返回一步之内所有可能的搭建结果。
  5. verify(proof, goal)质检员核心：证明链每一步都必须是合法的单步重写，且终点精确等于目标。
  6. search_proof(...)BFS 加随机出队，模拟模型在策略搜索空间里“东试试西试试”的采样行为。
  7. pass_at_k(problems, k)对每道题采样 k 个候选证明，统计至少一个通过验证的题目占比。
  8. random.seed(42)固定随机种子，保证评测结果可复现，这是工程评测的基本素养。

常见误区

误区小白往往以为 MiniF2F 就是考最终答案，AI 算出 `42` 就算过关；看到模型输出“答案是 42”就以为得了分。

正解MiniF2F 全场盯着证明过程。模型必须提交一整套形式化证明，验证器逐块检查每个推导步骤是否合法。答案对了但步骤跳跃、用了未声明公理，照样零分。就像乐高比赛，裁判不会因为你指着成品说“这塔是 42 块积木搭的”就把奖杯给你。

为何常见：人类考试习惯了“结果对即得分”的评分模式，“答案正确”的心智模型太过根深蒂固。

误区有人看到模型 Pass@5 比 Pass@1 高一截，兴奋地说“模型解题能力大幅提升”。

正解Pass@k 衡量的是“给 k 次尝试机会的成功率”，高 Pass@k 可能只是采样或搜索能力强——像投飞镖投了 k 次终于中了一靶。真正反映一次成型稳定性的指标是 Pass@1，两者必须分开报告，否则会被“撞运气”的分数误导。

为何常见：“k“字面像”评审看了 k 次”，忽略了它默认了多次独立采样补偿单次失误。

误区小白以为 MiniF2F 是“全新的、没被看过”的题库，分数一定代表模型真实数学能力。

正解MiniF2F 的题目来自公开数学竞赛，很可能已经出现在预训练语料里。如果模型“背过卷子”，分数会虚高。严谨的评测要剔除训练期可见的题目，或额外构造同级新题复测，就像考试时发现全是平时做过的原题，那这份成绩单的可信度自然要打折扣。

为何常见：公开数据集加大规模预训练时代，“评测集被模型看过”是普遍且隐蔽的问题。

误区看到模型在 MiniF2F 上通过率高，就宣布“AI 数学已经毕业，可以当数学家了”。

正解MiniF2F 覆盖的是已被形式化的竞赛题，范围有限、目标明确；现实数学问题表述模糊、需要构造新定义、常常没有现成战术可用。形式化鸿沟公式清楚表明“口头会解”和“形式化证明”之间仍有巨大落差——通过考试不等于能解决未知问题。

为何常见：“分数高 = 能力强”的类比太自然，容易忘记考试范围由出题者划定，而真实世界的数学没有标准题库。

面试题

Q1. MiniF2F 基准测试的核心评测对象是什么？

单选题 · easy

  • A.数学公式排版工具与渲染器
  • B.形式化定理证明的生成能力← 正确答案
  • C.自然语言到图像的生成质量
  • D.几何图形的三维重建精度

答案：B。MiniF2F 考察的是模型能不能生成机器可验证的形式化证明，而不是排版、画图或重建。就像乐高锦标赛只评价你搭的塔是否通过质检，不看你拍照好不好看。

Q2. MiniF2F 中“形式化”指的是哪种表述方式？

单选题 · easy

  • A.用 Markdown 书写数学公式
  • B.机器可验证的严格数学语言← 正确答案
  • C.用自然语言严谨描述解法步骤
  • D.用 Excel 表格整理计算过程

答案：B。形式化的核心是“机器可验证”。Markdown 只是排版，自然语言再严谨也有歧义，Excel 更与数学证明无关。只有 Lean、Isabelle 这类证明助手能逐条检查的语言才算形式化。

Q3. 下列哪个工具属于形式化证明助手？

单选题 · easy

  • A.Lean← 正确答案
  • B.PyTorch
  • C.Hadoop
  • D.Jupyter

答案：A。Lean 是微软开发的交互式证明助手，也是 MiniF2F 最常用的验证系统之一。PyTorch 是深度学习框架，Hadoop 是大数据工具，Jupyter 是笔记本环境，都不具备数学证明验证能力。

Q4. Pass@k 指标描述的是下列哪种情形？

单选题 · mid

  • A.采样 k 个候选证明至少一个通过验证← 正确答案
  • B.模型在 k 道难题上的平均成绩
  • C.k 次实验中正确率的标准差
  • D.k 折验证下的模型平均精度

答案：A。Pass@k 是指在评估时对同一道题独立采样 k 个候选证明，只要其中任意一个通过了验证器检查，该题就算命中。它强调“多次尝试中的最好结果”，而非平均成绩或稳定性。

Q5. 在 Lean 的证明状态 Γ ⊢ e : P 中，符号 Γ 表示什么？

单选题 · mid

  • A.当前可用假设与变量的集合← 正确答案
  • B.目标命题 P 的复杂程度
  • C.模型网络的梯度参数集合
  • D.证明过程的代码行数预算

答案：A。Γ 是上下文，包含当前证明中可用的假设、变量和公理，相当于搭建现场已经准备好的积木与规范。目标 P 才是待证明的命题，与梯度参数、行数预算完全无关。

Q6. 强化学习训练证明模型时，常见的奖励设计包括哪些？

多选题 · mid

  • A.成功完成 QED 证明时给予正奖励← 正确答案
  • B.对更短的证明路径给予少量奖励← 正确答案
  • C.依赖人类专家对美感的主观评分
  • D.完全不设置任何形式的奖励信号

答案：AB。最核心的奖励是“证明成功”这一二值信号，类似质检通过；缩短路径的小奖励能引导模型少绕路。人类美感评分主观且昂贵，完全不设奖励则无法驱动策略优化，都不合适。

Q7. 形式化鸿沟（Formalization Gap）衡量的是什么？

单选题 · hard

  • A.自然语言解题成功但形式化证明失败的比例← 正确答案
  • B.不同证明助手输出格式之间的差异
  • C.训练数据与测试数据之间的分布差异
  • D.GPU 训练到 CPU 推理阶段的迁移损耗

答案：A。形式化鸿沟衡量“口头会解但搭不出积木塔”的那部分题目占比。它反映从非形式化数学思维到机器可验证证明之间的转化难度，与工具格式差异、数据分布、硬件迁移都无关。

Q8. 为什么 Lean 验证器判定“证明为真”可以作为可靠的得分依据？

单选题 · extreme

  • A.验证器基于类型论内核机械且规则完备← 正确答案
  • B.验证器使用了大型语言模型的打分结果
  • C.验证器通过随机采样统计证明成立概率
  • D.验证器由多位数学奥赛裁判人工表决

答案：A。Lean 的内核把每个证明步骤规约为类型论中的机械检查，推理规则被穷尽地、确定性地验证，不存在神经网络打分或随机采样带来的近似误差。这正是它比人工阅卷更可靠的原因。

Q9. 模型在 MiniF2F 高难度题目上失败的可能原因有哪些？

多选题 · mid

  • A.搜索空间呈指数级爆炸难以穷举← 正确答案
  • B.部分证明需要极具创造性的中间构造← 正确答案
  • C.证明链过长让误差逐步累积放大← 正确答案
  • D.验证器会拒绝所有形式化的表达方式

答案：ABC。难题的证明状态树急剧膨胀，AI 在预算内找不到通路；奥赛题常需要灵光一现的辅助构造，模型难以凭空生成；步骤一多，任何一步的微小偏差都会放大。验证器本身公平接受所有合法证明，D 明显错误。

Q10. 评测时降低数据泄漏风险的正确做法有哪些？

多选题 · hard

  • A.剔除预训练语料中已出现的题目← 正确答案
  • B.划出模型训练阶段完全不可见的题目← 正确答案
  • C.额外构造同级别的新题目进行复测← 正确答案
  • D.允许模型在评测时联网搜索完整解答

答案：ABC。防泄漏的关键是保证“考卷没被背过”：剔除可见题、隔离训练期、用新构造题复测，都是有效手段。允许联网搜索等于直接开卷，完全破坏了评测意义。