大模型数学能力评测体系搭建与验证教程

一、教程目标

本教程要解决一个具体问题：如何搭建一套“可复核”的大模型数学能力评测，让分数背后的产出能够被逐项检查。

读完并完成实操后，你将能够：

1. 明确评测要考察的四类数学能力轨道，并为每一轨道定义可机器验证的产出物；
2. 构建具备难度分层与专家评审机制的题库，并把提示词难度从“裸题”到“带思路”分级管理；
3. 接入形式化证明内核，对模型提交的证明项做类型检查，而不是靠人眼判分；
4. 为“解法类”任务编写任务检查器，用一组实例运行模型产出的程序，验证解法是否可复用；
5. 统一尝试次数、联网策略、超时与资源配额，保证不同模型之间的分数可比；
6. 建立结果留档、复现、问题排查与成本优化的完整链路。

这套体系本质上是一套“评测工程”：把主观的“数学好不好”转化为客观的“提交物是否通过验证”。

二、适用场景

• 技术团队需要评估候选大模型是否适合数学推理、算法设计、形式化验证类业务；
• 教育、科研或工业软件团队希望引入模型做定理辅助证明、约束求解、参数推导；
• 需要构建内部回归评测，在模型升级或提示词调整后判断能力是否退化；
• 需要对外输出评测方法说明，向使用方解释分数如何产生、如何复现。

三、前置准备

3.1 基础环境

• 一套可弹性伸缩的计算资源：形式化证明核验与程序验收都偏 CPU/内存密集，建议通过容器平台编排，按任务隔离执行；
• 对象存储用于保存题库、提交物、执行日志与中间产物；
• 日志服务与监控告警用于追踪任务失败率、超时率与核验耗时；
• 消息队列用于把大批量评测任务从判分流程中解耦，避免长任务阻塞。

3.2 知识与数据准备

• 了解形式化验证的基本概念：定理陈述、定义、类型检查、隐式参数；
• 了解“可复现运行”的基本要求：固定依赖版本、固定随机种子、无网络依赖；
• 准备专家评审人员，用于对题目正确性、唯一性与难度做人工确认。

3.3 权限与安全

• 模型调用侧准备隔离的访问凭据，按最小权限授予；
• 执行侧准备独立沙箱账号，禁止访问外网与内部元数据服务。

四、实施步骤

步骤一：定义四条轨道与“可复核产出”

评测的第一原则是：每一题都必须有一个能自动判定的产出物。否则分数会退化为人工主观打分。

建议的四条轨道与对应产出：

轨道	考察能力	提交产出	验收方式
定理轨	证明构造	完整形式化证明项	形式化内核类型检查
求解轨	算法设计	可重复运行的程序	任务检查器跑多组实例
构造轨	对象构造	满足约束的显式对象	约束校验脚本
猜想轨	猜想生成	命题陈述 + 支撑证据	专家评审 + 半自动校验

为什么这样分：四条轨道分别对应“会证明、会算、会造、会想”。只做求解轨，评测会漏掉形式化与构造能力；只做定理轨，评测会漏掉工程可实现性。

步骤二：构建分层题库与评审流程

原始题库的规模通常在百题量级，且每条题都需专家评审通过。落地建议：

1. 按轨道划分目录，每题一个独立目录，内含题面、定义文件、验证脚本、元数据；
2. 元数据至少包含：题目 ID、轨道、来源、难度等级、参考产出、验证方式、预期耗时上限；
3. 建立评审状态机：待审 → 通过 / 退回 → 冻结，冻结后的题目不得静默修改，修改需升版本号；
4. 为每题准备“反向用例”，即刻意错误的产出，用于确认验证脚本确实会拒绝。

第 4 点经常被忽略，但它是评测可信度的关键：如果验证脚本对所有提交都返回通过，分数毫无意义。

步骤三：提示词难度分层

同一道题可提供三个难度的提示档位，用于区分“能力”与“提示依赖”：

• bare：只给目标陈述与所需定义，模型需自行完成全部推导与形式化；
• ladder：额外给出中间引理，考察模型填充细节的能力；
• guided：进一步给出证明思路或算法框架，考察模型执行既定路线的能力。

配置建议：对外公布的正式榜单应统一采用最严格档位（bare），并把分层结果作为诊断信息附在报告中。如果不同模型跑在不同档位，分数不可横向比较。

prompt_policy:
  leaderboard_tier: bare      # 榜单统一档位
  diagnostic_tiers: [ladder, guided]
  per_tier_isolation: true    # 不同档位分别建库，禁止混用缓存

步骤四：接入形式化证明核验链路

定理轨的核心不是让模型“写出看起来对的证明”，而是让证明通过形式化内核的类型检查。核验链路如下：

1. 把模型的提交物写入独立工作目录；
2. 在固定版本的依赖环境中执行类型检查；
3. 内核返回通过或报错；报错信息按类别归类（语法错误、定义缺失、类型不匹配、目标未完成等）；
4. 保留完整错误输出作为诊断数据。

需要注意的额外难度：形式化本身也是被考核对象。模型不仅要想出证明，还要正确处理定义展开、类型推断与隐式参数。自然语言中一句“显然”就跳过的前置条件，在内核里必须逐项交代。

verify_theorem(submission_dir):
    restore(dependency_lockfile)      # 固定依赖版本，保证可复现
    status = kernel_typecheck(submission_dir)
    if status == PASS:
        return {result: "pass", errors: []}
    else:
        return {result: "fail", errors: classify(status.errors)}

步骤五：为求解轨编写任务检查器

求解轨验收的是“一段能反复运行的程序”，而不是某个答案数字。检查器需要：

1. 准备一组公开实例与一组隐藏实例；
2. 对提交程序执行超时、内存上限与进程隔离；
3. 对每组实例比对输出是否满足判定条件（精确匹配、数值容差或约束满足）；
4. 统计通过比例，并区分“公开实例通过 / 隐藏实例通过”。

solver_check:
  instances:
    public: 5
    hidden: 10
  timeout_seconds: 60
  memory_limit_mb: 2048
  compare: constraint_satisfy   # exact | tolerance | constraint
  report: per_instance

为什么强调隐藏实例：只在公开样例上对答案的程序，很可能只是“背题”。单独撞对一个实例提供的证据非常有限，多实例与隐藏实例才是解法泛化的证据。

步骤六：统一尝试次数与采样策略

不同模型如果允许不同的尝试次数，分数之间就失去可比性。原始评测中就出现过一个模型每题 1 次、另一个模型每题 3 次的情况，这类差异必须在报告中显式标注。

建议做法：

• 主榜单统一 attempts = 1，指标记为 pass@1；
• 诊断实验可开 attempts = k，指标记为 pass@k，但必须单列，不与主榜混排；
• 固定解码参数与随机种子，记录每次尝试的完整输出；
• 每题记录总耗时，用于区分“做对”与“试很多次偶然做对”。

步骤七：联网隔离与执行沙箱

定理轨与求解轨建议关闭通用联网。原因有两点：一是避免模型直接检索到题目来源造成分数虚高；二是保证评测结果反映的是模型自身的推理与编码能力。

落地要点：

• 评测执行容器置于无外网子网，仅保留到模型推理服务的必要通路；
• 提交程序运行在只读文件系统 + 临时可写目录的沙箱内；
• 限制进程数、fork 能力与系统调用白名单，防止死循环或资源耗尽影响判分；
• 全程留档，保证任一分数都能回溯到具体提交物与执行日志。

步骤八：批量执行与结果采集

for track in tracks:                     # theorem / solver / construct / conjecture
    for item in track.items:
        for attempt in 1..attempts:
            output   = call_model(prompt(item, tier), tools=[])
            verdict  = verify(item, output)     # 内核检查或检查器验收
            archive(item, output, verdict, latency)
        item_score = aggregate(attempts)        # pass@1 / pass@k 明确标注

archive 是整个流程里最容易被省掉、但最不能省的一步：没有归档就无法复现，无法复现的评测无法作为技术决策依据。

五、配置说明与风险

配置项	含义	常见取值逻辑	风险
attempts	每题尝试次数	榜单取 1	跨配置比较会高估能力
prompt_tier	提示难度档位	榜单取最严档	混档导致不可比
timeout	单题时限	按题类分别设定	过短误判失败，过长拖慢评测
memory_limit	单进程内存上限	略高于参考实现峰值	过低造成假失败
allow_network	是否允许联网	推理类轨道关闭	开启后存在检索污染
dependency_lock	依赖版本锁定	全部锁定	未锁定导致结果漂移

六、结果验证

判断评测体系是否搭建成功，看四条标准：

1. 反向用例被正确拒绝：注入错误证明与错误程序，验证脚本必须返回失败；
2. 重复运行一致：同一提交物在同一配置下重复多次，判定结果完全一致；
3. 抽样人工复核：抽取若干“通过”样本由专家复核，确认内核与检查器判定与人工判断一致；
4. 榜单可下钻：任一分数字段都能追到题面、提示档、尝试次数、提交物全文与执行日志。

七、常见问题与排查

现象	可能原因	排查思路
大量证明“通过类型检查但语义不对”	提交中修改或重定义了目标命题	校验提交是否改动题目定义文件，做哈希比对
同一模型两次评测分数差异大	未固定解码参数或依赖版本	检查种子、温度与依赖锁文件
求解轨通过率异常高	检查器只跑了公开实例	确认隐藏实例数量与判定条件已启用
任务频繁超时	超时阈值低于模型正常耗时	按题类统计耗时分位数后重设阈值
模型输出被截断导致判失败	单次生成长度上限不足	提高输出上限并区分“截断失败”与“推导失败”
无法复现历史结果	提交物或日志未归档	补齐对象存储归档与版本号管理

八、优化建议

• 成本：先在小子集上做冒烟评测，通过后再跑全量；对失败样本单独回归，避免全量重复消耗。
• 稳定性：把判分任务放进消息队列并设置重试与幂等键，防止重复计费或重复写入。
• 安全：模型调用凭据与执行沙箱凭据分离，日志中脱敏处理题面与密钥。
• 可维护性：题库、验证脚本、评测配置三者版本化绑定，形成不可变的评测快照。
• 可扩展性：轨道以插件形式接入，新增题类只需实现“产出物 + 验证器”两个接口。
• 可观测性：对失败率、超时率、平均核验耗时设置监控告警，异常波动往往意味着环境而非模型发生了变化。

九、总结与后续方向

这套评测真正的价值不在于排出一张名次表，而在于它把“模型数学能力”拆成了可验证的动作：写出能通过内核检查的整段证明、写出能通过多实例验收的可复用程序、构造出满足全部约束的对象、提出经专家确认的猜想。分数只是这些动作的汇总。

有了这样的基础设施，你可以进一步关注三个方向：一是用分层档位与 pass@k 定位模型是“不会”还是“需要更多提示”；二是把失败样本按错误类型聚类，反哺业务提示词与工具链设计；三是把评测做成模型升级前的固定回归环节。

在落地资源时，可依托百度智能云的容器平台、对象存储、日志服务、监控告警等通用能力承载评测集群，实现任务隔离、结果归档与异常告警的一体化，让评测从一次性活动变成可持续运行的能力基线。