TB-MathModel 附录：十八道赛题、评分公式与 Lean 义务

附录总览

译注：本篇是同一篇论文的附录全文，正文见 https://openqa.cn/articles/tb-mathmodel-verifiable-modeling-zh 。

本补充材料使主论文的构造与论断可被审计。附录 A 给出数据集构成、逐任务表、交付的目录结构，以及一项明确陈述：TB-MathModel 没有训练/验证/测试划分。附录 B 记录软件与硬件环境以及网络隔离策略。附录 C 列出逐条目配置、智能体命令模板，以及重试/产物恢复细节。附录 D 对被称为“baseline”的三个对象消歧。附录 E 复现提示词模板与评测框架包裹层。附录 F 给出三项案例研究背后的完整数值。附录 G 给出评分公式、被排除的指标，以及硬门槛判定。附录 H 编目 Lean 义务、信任审计与判别套件。

• 附录 A：数据集构成、逐任务表、交付结构与划分
• 附录 B：主机、智能体容器、验证器容器、资源限制、网络隔离
• 附录 C：逐条目配置、命令模板、重试、成本核算
• 附录 D：flash 基线、Outstanding 锚点、遗留端点、锚点注意事项
• 附录 E：提示词结构、产物块、评测框架包裹、版本注意事项
• 附录 F：完整数值案例研究表
• 附录 G：指标面板、公式、被排除的指标、硬门槛
• 附录 H：义务计数、代表性义务、信任审计、判别套件

附录 A 数据集细节

A.1 构成

表 4：18 项 TB-MathModel 任务及其 O 奖锚点。“Final Q”是其数值核心被评分的竞赛问题；oracle 覆盖为 18/18。

TB-MathModel 有 18 项任务，列于表 4（正文）。其构成为 CUMCM（中文）2023、2024、2025 $\times$ 问题 A、B、C $=$ 9 项任务，加上 MCM（英文）2023、2024、2025 $\times$ 问题 A、B、C $=$ 9 项任务。每项任务是一道含若干子问题的完整竞赛题；仅最终问题的数值核心被评分。问题 A 通常为物理/工程，B 为优化/数据，C 为数据科学，因此每年三题全取，以避免主题上的择优挑选。

A.2 逐任务摘要

表 5 逐项概括每项任务。“#Fig.”统计从官方 PDF 裁出的不重复图数；“#Metric”是被评分指标的数量。

表 5：逐任务摘要。“Final Q”是被核定的最终问题。

†18 项任务上共有 60 个被评分指标；另有一项 Wordle 指标声明权重为 0，并被排除出评分。这些计数已对照已发布任务核验；21 张图在去重后不重复，并交付两次——一次内联于指令文件，一次置于容器图路径下。数据来源为官方竞赛材料：CUMCM 赛题位于 cumcm/problems/{year}/{X}.md，MCM 位于 mcm/problems/{year}/{X}.md；用于锚点的 Outstanding 论文 PDF/OCR 来自同一语料库的 outstanding/ 目录树，且每项任务记录其论文标识、PDF/OCR 源路径及其 reproduction_scope。

A.3 逐任务多参考分数

表 6：四个代表性条目的逐任务多参考 O-Eval（%）。每一列的均值等于该条目主表中的 O-Eval，因此逐任务数值与榜单相符。

A.4 交付结构

每个任务目录包含一个指令文件（即提示词）、一个元数据文件（限制）、一个环境目录（智能体镜像加数据）、一个测试目录（验证器、评分配置、锚点），以及一个解答目录（oracle）。环境数据目录内有赛题副本、输出纲要（仅字段名与类型）、一份把每个可见文件映射到其语料路径的来源清单、以扁平文件名存放并带索引的逐字附件、原始语料的全路径镜像，以及拥有这些图的六项任务的裁剪图。

A.5 划分

图 4：一张官方赛题图，从 CUMCM 2023 A 的 PDF 裁出，并内联交付于提示词中。分布于 6 项任务的 21 张此类图是承重的：最终答案取决于阅读它们。

图

不存在训练/验证/测试划分。TB-MathModel 是纯评测集：18 项任务全部是评测任务，统一评测，没有留出划分，也没有逐任务难度层级。（有一项任务的 oracle 模型包含针对 Wordle 问题的任务内训练/测试划分；那是该问题建模内容的一部分，与基准划分无关。）

附录 B 软件与硬件环境

B.1 主机与框架

评测框架从一台 macOS 主机（arm64）运行。它编排逐任务的 Docker 容器；所强制的资源限制是容器限制，而非主机限制。

B.2 智能体容器

全部 18 项任务使用同一基础镜像与依赖集。基础镜像为 python:3.12-slim 加 uv。位于 /opt/venv 的 Python 环境固定 NumPy 2.0.2、pandas 2.2.2、SciPy 1.14.1、scikit-learn 1.5.2、Matplotlib 3.9.2（MPLBACKEND=Agg）、openpyxl 3.1.5 与 xlrd 2.0.1。可写路径为 /root/data（只读输入）、/root/results（被评分的产物）与 /logs/agent。

B.3 验证器容器

验证器运行于一个由最小 python:3.12-slim 镜像构建、仅安装 pytest 的独立容器中。它没有网络，除已复制的产物外不能访问智能体的工作目录。验证器超时为 180 s。

B.4 资源限制

所有任务的限制相同：2 个 CPU、8192 MB 内存、20480 MB 存储、0 个 GPU。构建超时为 900 s，智能体超时为 14400 s（4 h），并在每条提示词末尾同样写明。所记录的运行使用一次并发试验且不重试。

B.5 网络隔离

每项任务都禁用互联网访问。模型流量经本地重试代理路由，因此智能体可以调用模型 API，但不能在运行时获取解答、下载软件包或安装工具。因为试验开始后无法安装，CLI 智能体（codex、opencode、claude-code）必须存在于镜像中；第三方操作者的运行在 Dockerfile 末尾预装了这些 CLI，并仅将模型网关列入允许名单，赛题、数据与验证器保持不变。

B.6 冻结版本

为可复现性，我们固定评测框架版本、上文的 Python 依赖集，以及用于成本的本地价格快照，从而使所报告的成本在重复运行之间保持稳定。

附录 C 实验设置

C.1 逐条目配置与结果

表 7 列出七个多模态条目，以及实际传入的评测框架与推理档位和它们的全部分数。多模态状态指评测框架暴露图像通道。每个条目对每项任务以三个种子运行。

表 7：多模态榜单，18 项任务，按 O-Eval 排序。“Art.”是具有可评分产物的任务数；O-Eval 是多参考面板分数，Multi-BO 是同一分数相对于 DeepSeek V4.1 Flash 基线的值，二者均为三种子均值（ ± \pm 标准差）。

C.2 智能体命令模板

任务赛题作为其提示词传给智能体。所记录试验中的代表性命令：

⬇ (data:text/plain;base64,IyBjb2RleApjb2RleCBleGVjIC0tZGFuZ2Vyb3VzbHktYnlwYXNzLWFwcHJvdmFscy1hbmQtc2FuZGJveCAtLXNraXAtZ2l0LXJlcG8tY2hlY2sgXAogIC0tbW9kZWwgZ3B0LTUuNSAtLWpzb24gLS1lbmFibGUgdW5pZmllZF9leGVjIFwKICAtYyBtb2RlbF9yZWFzb25pbmdfZWZmb3J0PXhoaWdoIC0tICc8aW5zdHJ1Y3Rpb24ubWQgYm9keT4nCgojIG9wZW5jb2RlCm9wZW5jb2RlIC0tbW9kZWw9b3BlbmFpL2RlZXBzZWVrLWZsYXNoIHJ1biAtLWZvcm1hdD1qc29uIC0tdGhpbmtpbmcgXAogIC0tZGFuZ2Vyb3VzbHktc2tpcC1wZXJtaXNzaW9ucyAtLSAnPGluc3RydWN0aW9uLm1kIGJvZHk+Jw==)

codex

codex exec --dangerously-bypass-approvals-and-sandbox --skip-git-repo-check \

--model gpt-5.5 --json --enable unified_exec \

-c model_reasoning_effort=xhigh -- ’<instruction.md body>’

opencode

opencode --model=openai/deepseek-flash run --format=json --thinking \

--dangerously-skip-permissions -- ’<instruction.md body>’

每个 CLI 评测框架把赛题作为其位置参数提示词接收；评测框架会在其之前前置自己的通用系统提示词。

C.3 重试、并发与产物恢复

全部条目使用一次并发试验且无自动重试；三个种子中的每一个都是对 18 项任务的一次独立遍历。此处披露两处细节。第一，归档错误的产物：两项任务以连字符而非所要求的下划线写出结果，因此评测框架未收集到它；我们重放所记录运行的脚本以复现该产物并重新评分。第二，第三方运行：GPT-6 Astra 与 Fable 5.1 条目由独立操作者运行；因其验证器使用了不同的奖励公式，我们用自己的评分器与当前锚点对其保存的产物重新评分，以使全部条目共享同一评分定义。在产物未被打包之处，我们从保存的逐指标记录重建被评分字段，并核验其在完整产物存在的任务上精确复现操作者自己的数字。

C.4 成本核算

成本由测得的 token 用量对照固定价格快照计算，并采用报告中陈述的两项保守调整：提供方在其补全计数器之外计费的推理 token 被加到输出，以及在提供方收取峰时/谷时费率之处采用峰时费率。对两个第三方条目，成本是其自行测得的每次运行 USD。因为价格文件为本地且固定，成本不会在重复运行之间漂移。

附录 D 基线信息

“baseline”一词在本基准中被重载；我们区分三个不同对象，以使这些数字无歧义。

D.1 flash 基线（分数归一化）

Robust BO-Eval 对照单一参考提交计算，即在相同任务上运行的 DeepSeek V4 Flash 基线。它定义零点：Robust BO-Eval 以 oracle–基线间隙对模型–基线增益做归一化。它是一次模型提交，而不是经整理的基线面板。

D.2 Outstanding 锚点（分数上限）

每项任务的上限是一篇 Outstanding 奖论文的复现，即得分为 O-Eval$=100\%$ 的那个值。表 8 列出每项任务的锚点论文标识。每个锚点是一个可运行脚本，它读取官方附件并输出产物 JSON，外加一份已提交的、记录其数值的期望结果；覆盖为 18/18。

表 8：每项任务的 Outstanding 奖锚点。

D.3 遗留的逐任务基线端点

18 项任务中有 15 项使用带基线端点的遗留“目标到 Outstanding 的距离”模式；三项（Wordle、台阶磨损与 Juneau 旅游）使用真正的逐指标基线到 Outstanding 的 min–max 端点。该区分按指标记录于每份评分配置中，并呈现在逐任务表里。

D.4 锚点注意事项

两条锚点带有影响其分数应如何解读的注意事项。作物种植是一个标明的特例：论文的完整约束集在官方附件上联合不可行，其报告值来自一项未公开的启发式，因此该锚点是在论文的逐地块需求上限之下可复现的精确 MILP 最优解。舞龙已作修正：论文的 1.406276 m/s 不可行（一个把手会达到 2.2568 m/s），因此该锚点是连续时间值 1.246266 m/s，且指标方向为 target_value。二者都是这一一般原则的例子：锚点是对某一队之选择的复现，且其来源必须可核查。

附录 E 提示词设计

E.1 提示词即任务陈述

本基准中没有手写的提示词包装。提示词就是该任务的说明文件，由评测框架逐字交付。其结构在各任务间固定：一条机器可读的金丝雀注释（在交付前被剥离）；一个“Original Contest Problem”节，内含逐字陈述，且每一幅被引用的图都内嵌其中；陈述所要求的任何结果表，以纯文本给出；一条列出容器内图路径的说明；一个“Required Benchmark Artifact”节；以及时限行。

E.2 产物块（逐字模板）

⬇ (data:text/plain;base64,IyBSZXF1aXJlZCBCZW5jaG1hcmsgQXJ0aWZhY3QKClNvbHZlIHRoZSBjb250ZXN0IHByb2JsZW0gYWJvdmUuIFRoZSBvZmZpY2lhbCBhdHRhY2htZW50cyBhcmUgbWlycm9yZWQgYXQKYC9yb290L2RhdGEvYXR0YWNobWVudHNgIChmbGF0IGZpbGVuYW1lczsgc2VlCmAvcm9vdC9kYXRhL2F0dGFjaG1lbnRzL0lOREVYLm1kYCkgYW5kIGFsc28gcmVtYWluIGF0IHRoZWlyIGZ1bGwgY29ycHVzIHBhdGhzCnVuZGVyIGAvcm9vdC9kYXRhL3JlcG9gLiBVc2UgdGhlbSB3aGVuZXZlciB0aGV5IGFyZSByZWxldmFudC4gV3JpdGUgeW91ciBmaW5hbApzdHJ1Y3R1cmVkIGFuc3dlciB0bzoKCi9yb290L3Jlc3VsdHMvPHNsdWc+X3Jlc3VsdC5qc29uCgpUaGUgcmVzdWx0IG11c3QgYmUgdmFsaWQgSlNPTiBhbmQgc2hvdWxkIGZvbGxvdyB0aGUgc2hhcGUgc2hvd24gaW4KYC9yb290L2RhdGEvb3V0cHV0X3NjaGVtYS5qc29uYC4gSW5jbHVkZSB0aGUgbnVtZXJpY2FsIHF1YW50aXRpZXMsIG1vZGVsaW5nCmRlY2lzaW9ucywgZGlhZ25vc3RpY3MsIHNlbnNpdGl2aXR5IG9yIHVuY2VydGFpbnR5IHJlc3VsdHMsIGNvbmNsdXNpb25zIGZvciB0aGUKY29udGVzdCBxdWVzdGlvbnMsIGFuZCBnZW5lcmF0ZWQgYXJ0aWZhY3QgcGF0aHMgbmVlZGVkIHRvIHN1cHBvcnQgeW91ciBhbnN3ZXIuCllvdSBtYXkgYWxzbyB3cml0ZSBzdXBwbGVtZW50YXJ5IENTViwgWExTWCwgb3IgUE5HIGZpbGVzIHVuZGVyIGAvcm9vdC9yZXN1bHRzYCwKYnV0IHRoZSBKU09OIGZpbGUgYWJvdmUgaXMgdGhlIHJlcXVpcmVkIGFydGlmYWN0LgoKWW91IGhhdmUgMTQ0MDAgc2Vjb25kcyB0byBjb21wbGV0ZSB0aGlzIHRhc2suIERvIG5vdCBjaGVhdCBieSB1c2luZyBvbmxpbmUKc29sdXRpb25zIG9yIGhpbnRzIHNwZWNpZmljIHRvIHRoaXMgdGFzay4=)

Required Benchmark Artifact

Solve the contest problem above. The official attachments are mirrored at

‘/root/data/attachments‘ (flat filenames; see

‘/root/data/attachments/INDEX.md‘) and also remain at their full corpus paths

under ‘/root/data/repo‘. Use them whenever they are relevant. Write your final

structured answer to:

/root/results/<slug>_result.json

The result must be valid JSON and should follow the shape shown in

‘/root/data/output_schema.json‘. Include the numerical quantities, modeling

decisions, diagnostics, sensitivity or uncertainty results, conclusions for the

contest questions, and generated artifact paths needed to support your answer.

You may also write supplementary CSV, XLSX, or PNG files under ‘/root/results‘,

but the JSON file above is the required artifact.

You have 14400 seconds to complete this task. Do not cheat by using online

solutions or hints specific to this task.

E.3 评测框架包装

各评测框架以不同方式交付同一文本。每个 CLI 评测框架都先在前面加上其自身的通用命令行系统提示，然后把陈述作为位置提示提供。

E.4 版本注意事项

说明文件在部分试验被记录之后作了修订：增加了一个图路径节，并且有一份 MCM 陈述改从官方 PDF 重新取材。在给定试验中实际交付的提示词，就是该试验日志中所捕获的那一份；为可复现性，应引用那些，而不是当前文件。这就是我们在上文描述提示词结构，而不是把今天的文件当作每个模型所见之物来引用的原因。

E.5 提示词按设计所不提供的内容

按设计，提示词是纯粹的任务描述：没有建模提示，没有方法建议，除模式之外也没有指向被评分字段的指针。它让智能体自行推断哪些数字要紧，从而使这一设定成为对整个建模问题的检验，而不是一项填模式练习。这使本基准保持为对完成整个建模问题的检验，代价是智能体必须自行推断哪些数字要紧。

附录 F 案例研究（完整数值）

我们给出三个案例研究的完整逐字段比较。数值读自每个角色所保存的产物；oracle 列即锚点。三张表都横跨双栏。

表 9：舞龙（CUMCM 2024 A，Q5）。三个角色一致；论文值是离群值，并且不可行。

真实峰值的重构，是把手速度比的连续时间最大值；论文按整数秒采样，并跨过了它。精确恒等式 head_speed$\times$ratio$=2$ m/s 由程序化门控与 Lean 层双方核验，正是它揭示论文值不可行：论文的孤立值 1.406276 m/s（比值为 1.422195）意味着在一个把手处为 2.2568 m/s。

表 10：作物种植（CUMCM 2024 C，Q1）。特例：锚点是在论文的逐地块上限之下可复现的精确最优解。

论文的完整约束集在官方附件上不可行，因此锚点是一个可复现的 MILP 最优解，而各模型的方案处于同一情形。锚点在折扣列上位于两个模型之间，这就是单一标量无法概括这一任务的原因。

表 11：朱诺旅游（MCM 2025 B，最后一问）。可持续性分数由不同智能体按不同的单位尺度报告。

这是最清楚的尺度问题。锚点处于 $\sim$1 的单位尺度上；有一个第三方智能体把同一字段报告在 0–100 的“multiattribute utility”尺度上，并在其自身产物中明确声明这一点。因为该任务的输出模式并未钉住取值范围，所以该智能体并非错误——这就是为何正确的修补是在模式中规定该字段的取值范围，而不是在评分器中重定标。

F.1 讨论

舞龙。论文的孤立值（1.406276）是错误的那个。这个案例最为要紧，因为它颠倒了通常的说法：模型是对的，参考是错的，而修正是对基准作出的。它也表明为何可行性层并非与评分相冗余——“ratio $\times$ head speed $=2$ m/s”是一个精确恒等式，两层都核验它，而正是它使论文值的不可行性变得可见。

作物种植。GPT-5.5 与 DeepSeek 产生的方案利润处于同一情形，而最优值在其中一列上位于二者之间——这就是单一标量无法概括该任务的原因。当人类论文不可复现时，诚实的做法是锚定于一个可复现的值并加以标明，而不是因模型吻合一个不可复现的数字而惩罚模型。

朱诺。oracle 建议每天 11,000 的上限、费用为 55 USD，可持续性分数为 1.007；GPT-5.5 在其自身的 0–1 尺度上建议每天 20,000、费用为 20 USD；DeepSeek 建议每天 16,000、费用为 30 USD。这表明任务模式——而不仅仅是评分器——必须声明一个字段的取值范围与单位，这是对任务的修正，而不是对代码的修正。

附录 G 评分细节

G.1 指标面板

每个任务都自带一份评分配置，声明其被评分的指标。一条指标项指定进入产物的一条路径、一个 oracle 值、可选的基线值与优秀值、一个方向（带有一个与之匹配的语义方向）、一种归一化模式，以及一个权重。在 18 个任务中共有 60 个被评分指标；另有一个 Wordle 指标以权重 0 被声明并被记录，但被排除在面板之外。各任务的计数见表 5。

G.2 公式

设 $R$ 为一次提交的加权面板原始分，$F$ 为 DeepSeek V4 Flash 基线的，$O$ 为 oracle 的，且 $\mathrm{gap}=O-F$。我们报告 $\textsc{O-Eval}=\mathrm{clamp}(R/O,0,1)$，以及一项基于原始增益 $R-F$ 的、经间隙补偿的 Robust BO-Eval：

$\displaystyle\mathrm{clip}\!\left(\tfrac{R-F}{\mathrm{gap}},\,\pm 1\right)$ $\displaystyle\ \ \text{if }\mathrm{gap}\geq 0.10,$

$\displaystyle\mathrm{clip}(R-F,\,\pm 0.10)$ $\displaystyle\ \ \text{otherwise},$

其中 $\pm$ 表示对称界。缺失或不可评分的产物得到 $\textsc{Robust BO-Eval}=-1$。逐指标奖励在第 3.1 节给出；单侧性质（达到或胜过锚点时，得分永不低于 $1.0$）由一项契约测试锁定。

表 12：覆盖全部 18 个任务之硬错误分支的六种可判定不变量形式。

G.3 被排除的指标

表 13：可行性的三个层级。两层都覆盖 A 与 B；C 需要形式化的物理。

有两项指标对每一个模型以及 oracle 都被排除在面板之外，二者都只依据仅配置规则：奥林匹克的第四条推荐（提示要求三个国家，但复现输出四行），以及当锚点量级超过 5 时的两个七鳃鳗原始种群指数（该锚点是一个任意的原始指数，没有被模式钉住的单位）。域外值（$[-1,1]$ 之外的相关、$[0,1]$ 之外的单位区间量、负的计数、非正的物理量）并不被排除，但其奖励被置为零，并记录原因。

G.4 硬门控决定

在各条目上施加了七次整任务惩罚：四次定日镜违规（额定功率低于 60 MW，或一面镜子低于 2 m 的下限），一项未通过独立覆盖回放的烟幕方案，一份接受度／可持续性取值单位无效的朱诺答案，以及一份教练效应结果退化的奥林匹克答案。

G.5 已发现并已修复的陷阱

基于锚点的基准，其可信程度只取决于其锚点，因此我们审计了评分规则与锚点，并报告审计所改变的内容。两处门控假阳性（一个带符号的弹性被读成负计数；一个缺失字段被读成硬矛盾）已予纠正，但未改变任何分数，而退化带加宽移动了一个分数（v4 pro 为 $+0.35$ 个百分点）。不可比单位排除使每一个条目提高 0.05–2.62 个百分点，因为该惩罚对所有提交同等施加——这是系统性评分错误而非模型差异的标志。最后，舞龙锚点本身在物理上不可行：论文的 1.406276 m/s 会把一个把手驱动到 $1.406276\times 1.604793=2.2568$ m/s，高于 2 m/s 的上限，因为它在整数秒上取最大，并跨过了 $t=14.48$ s 处真正的连续时间峰值。我们把锚点修正为 1.246266 m/s；十二个受评模型曾报告正确值，并一直处于 49.82%，而两个吻合错误论文值的模型曾处于 100%。此处错的是基准，而不是模型（附录 G 与 H）。

G.6 退化带与有效性规则

带加宽规则适用于三个端点式任务的端点指标。应用本文中的全部评分修正，使每一个条目上移 0.05–2.62 个百分点，因为受影响的惩罚对所有提交同等施加——这是系统性评分错误而非模型差异的诊断标志。

附录 H Lean 义务目录

H.1 逐任务义务计数

生成器对每个可检查字段发出一条义务；按任务的总计见表 14。

表 14：各任务的义务（18 个任务共计 624 条）。“已跳过”的义务被报告为证据缺失，而不是被静默地视为已满足。

在生成器输出中可见四条被跳过的义务：一个缺失的重叠字段（多波束），声明的网格计数为空的情景（马赛划分），以及一处推荐计数的解释差异（奥林匹克）。

H.2 代表性义务

在不变量库上，一个任务提供界限，义务据此生成。示例： ⬇ (data:text/plain;base64,LS0gZG9tYWluL3JhbmdlOiBhIHJhdGUgbXVzdCBsaWUgaW4gWzAsMV0gKHNjYWxlZCB4MTAwMCkKZXhhbXBsZSA6ICgwIDw9IDQzIC9cIDQzIDw9IDEwMDApIDo9IGJ5IGRlY2lkZQoKLS0gb3JkZXJpbmc6IHE5NSBtdXN0IG5vdCBmYWxsIGJlbG93IHRoZSBtZWFuCmV4YW1wbGUgOiAocG9zdGVyaW9yX21lYW4gPD0gcG9zdGVyaW9yX3E5NSkgOj0gYnkgLi4uCgotLSBleGFjdCBpZGVudGl0eTogaGVhZF9zcGVlZCAqIHJhdGlvID0gMiBtL3MgKHNjYWxlZCkKZXhhbXBsZSA6ICgxOTgwMDAwIDw9IDEyNDYyNjYgKiAxNjA0NzkzIC9cIDEyNDYyNjYgKiAxNjA0NzkzIDw9IDIwMjAwMDApIDo9IGJ5IGRlY2lkZQoKLS0gZmluaXRlIGRvbWFpbjogY291bnQgb2YgZGVjaXNpb24gYml0cyBpcyAxNiBvciAxNwpleGFtcGxlIDogKGxlbiA9IDE2IFwvIGxlbiA9IDE3KSA6PSBieSBkZWNpZGU=) -- domain/range: a rate must lie in [0,1] (scaled x1000)

example : (0 <= 43 /\ 43 <= 1000) := by decide

-- ordering: q95 must not fall below the mean

example : (posterior_mean <= posterior_q95) := by ...

-- exact identity: head_speed * ratio = 2 m/s (scaled)

example : (1980000 <= 1246266 * 1604793 /\ 1246266 * 1604793 <= 2020000) := by decide

-- finite domain: count of decision bits is 16 or 17

example : (len = 16 \/ len = 17) := by decide

每一条生成的义务都标注了它所来自的 JSON 路径，因此审阅者可以把每一条主张追溯回该产物。

H.3 信任审计（压缩摘录）

⬇ (data:text/plain;base64,J0ZlYXNpYmlsaXR5LmF0TW9zdF90cmFucycgICAgYXhpb21zOiBwcm9wZXh0LCBRdW90LnNvdW5kCidGZWFzaWJpbGl0eS5hdExlYXN0X21vbm8nICAgIGF4aW9tczogcHJvcGV4dCwgUXVvdC5zb3VuZAonQ3JvcFBsYW50aW5nLnVhX2ZlYXNpYmxlJyAgICBubyBheGlvbXMKJ0Nyb3BQbGFudGluZy51YV9pbl9pbnRlcnByZXRhdGlvbl9nYXAnICAgbm8gYXhpb21zCidKdW5lYXUudWFfYWNjZXB0YW5jZV9wZXJjZW50X29ubHknICAgICAgIG5vIGF4aW9tcwonSnVuZWF1LnVhX3N1c3RhaW5hYmlsaXR5X291dF9mb3JfYW55X3NhbmVfdG9sJwogICAgICAgICAgICAgICAgICAgICAgICAgICAgICBheGlvbXM6IHByb3BleHQsIFF1b3Quc291bmQKJ0p1bmVhdVNlbnNpdGl2aXR5LnJlcG9ydGVkX2luZmVhc2libGUnCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIGF4aW9tczogcHJvcGV4dCwgUXVvdC5zb3VuZA==) ’Feasibility.atMost_trans’ axioms: propext, Quot.sound

’Feasibility.atLeast_mono’ axioms: propext, Quot.sound

’CropPlanting.ua_feasible’ no axioms

’CropPlanting.ua_in_interpretation_gap’ no axioms

’Juneau.ua_acceptance_percent_only’ no axioms

’Juneau.ua_sustainability_out_for_any_sane_tol’

axioms: propext, Quot.sound

’JuneauSensitivity.reported_infeasible’

axioms: propext, Quot.sound

只出现 propext 与 Quot.sound（Lean 的标准经典逻辑），或者完全没有公理。没有 sorryAx，也没有 Lean.ofReduceBool（即没有 native_decide）；流水线对二者都作 grep。

H.4 判别套件

判别脚本每次变异一个数值叶子，并要求构建失败，且引用被变异的字段。六种形式上一共覆盖十次变异（越界概率、越界相关、次序颠倒、被违反的精确恒等式、非正厚度、区间颠倒、非二元决策位、负的接受指数、$q_{95}$ 低于均值、为零的物种计数）。十次全部被拒绝；若有任何一次未被拒绝，该套件以非零状态退出。

H.5 复现该层

工具链是经由 elan 的 Lean 4，不带 Mathlib；一次干净构建大约在一秒内完成。生成器也对照已提交的 Outstanding 奖参考运行，因此不必有已保存的智能体产物，即可演练该层。