我现在已经掌握了所有必要的事实依据。ReLoop (Lian et al., 2026, arXiv:2602.15983) 是最接近的现有工作，发表于 2026 年 2 月，本文发表于 2026 年 7 月——时间跨度约为 5 个月，因此它不属于同期工作，构成了合理的创新性比较。我已经阅读了完整的 PDF（32 页）和完整的 HTML 全文（81KB 纯文本）。我已具备输出审稿所需的一切材料。

Paper Review: Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits

论文类型: 问题定义型 + 分析型（理论驱动的验证框架，兼具方法型贡献）

公理审查结果

公理一：对象公理

• 判定: ✅
• 分数: 9
• 依据: 论文研究的对象是真实且重要的。LLM 生成优化模型时的静默失败（silent failure）是已被多个独立工作证实的现实问题：(1) 同一模型在教科书问题上达 85%、在工业问题上降至 38%（Huang et al. 2025）；(2) 公共基准标签本身存在文档记录的错误（Chen et al. 2025b 需在评测前修正 NL4OPT 和 IndustryOR 标签）；(3) 组合问题上的求解可行性与语义正确性差距高达 90 个百分点（Lian et al. 2026）。论文定义的核心概念均可操作化：slot 是文本中的数值量，qtype ∈ {capacity, requirement, rate, cost, reward, ratio} 有明确的语义映射规则（Def 3.1），role-faithfulness 给出了可检验的数学定义（每个 slot 只出现在其断言位置上）。验证目标（无参考模型、无标签的 falsification）与部署场景一致——部署时确实没有 ground-truth。claim 外延受 Section 5 的 detection limits 约束，论文明确承认 blind set 非空且不可消除（Prop 5.2 orbit-redundancy、Prop 5.3 single-slot reparametrization）。
• Wiki 证据: OMC Wiki 三次查询均无记录（”LLM optimization model verification falsification”、”NL4OPT benchmark”、”sound test battery”）。free-search 确认 NL4OPT 是 NeurIPS 2023 竞赛，ORLM、OptMATH 等后续工作均依赖 execution accuracy，验证了论文对现有评测范式缺口的判断。ReLoop (arXiv:2602.15983, 2026-02) 是唯一直接前驱工作，也确认了 behavioral verification 路线的现实需求。

公理二：识别公理

• 判定: ✅
• 分数: 8
• 依据: 论文的因果识别清晰。核心 claim 是”用优化理论的必要条件（对偶、比较静态、多面体极限）作为 falsifier 比阈值启发式更强”，证据链支持这一归因：(1) Prop 5.7 证明任何固定阈值 τ>0 都存在一族 faithful 候选使 FP 率为 1，而 certified crush (A4) 对同一族不触发——这是直接对比，隔离了”阈值 vs 证书”这一单一变量；(2) 实验中 battery 的 0.0% FP 率 vs threshold 的 54.9% FP 率，在同一 IR、同一 slot table、同一 solver 上测得，控制了数据绑定和求解器差异；(3) detectability matrix（Table 7.1）的 class-by-error 预测由 Theorem 5.6 的 case 分析导出，实验复现包括零检测率（M8 gauge、M9 orbit-redundant），这是理论预测的直接验证而非事后解释。可能的扣分点：ablation 缺少对 two-pass interface (Section 6) vs free-form generation 的消融（论文在 7.6 承认），因此无法完全隔离”接口改进”和”battery 本身”对 pipeline 层面 27.6% 检出率的贡献。
• Wiki 证据: OMC Wiki 无”最简 baseline”和”ablation 消融”记录。free-search 确认 ReLoop 是唯一切近的 solver-trusting baseline，论文对其进行了严格慈善的重实现（继承精确 binding 而非依赖 LLM 编辑）。

公理三：独立性公理

• 判定: ✅
• 分数: 9
• 依据: 评测独立性是本文的一个结构性优势。battery 不依赖任何参考模型、标签或参考最优值（Def 3.3 oracle-freeness）。326 个 faithful seeds 来自 NL4OPT 的 declared ground-truth formulations，但 battery 对这些 seeds 的判定完全通过 solver call 和结构谓词进行，不与标签比较。mutation study 中，mutants 由确定性算子生成（11 类算子），battery 的判定与 mutant 生成过程独立。LLM-as-judge baselines 使用 Qwen2.5-7B 和 DeepSeek-R1-Distill-Qwen-7B，与 generator (Qwen2.5-7B) 存在家族重叠，但论文将 judge 定位为 baseline 而非主方法的验证手段，且明确指出 self-critique 的不可靠性。唯一的轻微依赖：deployment mode 的 assertions 来自 LLM extraction pass，论文承认”extraction is short, structured, and votable, but not infallible”（7.6），但这是一个诚实的局限性声明而非隐藏的循环。
• Wiki 证据: OMC Wiki 无”judge 独立性”或”synthetic 人类校验”记录。论文的 assertion extraction 是否有独立人类校验未明确——在 annotated mode 中 assertions 来自 NL4OPT 的 ground-truth declarations（机械提取），在 deployment mode 中来自 LLM extraction pass，后者缺少独立人类验证，但这不影响 annotated mode 的核心实验结论。

公理四：压缩公理

• 判定: ✅
• 分数: 9
• 依据: 论文的核心压缩价值极高。它将五十年的灵敏度分析、对偶理论、比较静态学重新定位为验证技术，用一个统一框架（typed slots + oracle-free tests）替代了 ad hoc 的阈值调参。六个测试类（A1-A7）加四个 coherence 测试（B1-B4）全部从少数几个经典定理（LP duality、set inclusion、Topkis 单调性、relabeling symmetry）导出，不是模块堆叠。detection limits（Section 5）与 detectability（Theorem 5.6）的正反两面构成一个 falsifiable prediction（detectability matrix），实验复现包括零点——这是理论压缩的直接证据。命名精确：slot、role-faithfulness、crush probe、prohibitive limit、exchange、orbit——每个术语对应明确的数学对象，无命名膨胀。与 ReLoop 的关系是严格推广（presence check = crush test 的退化情形，Prop 5.7 给出不可能性结果解释了为何 ReLoop 的阈值不可调好）。唯一可讨论点：two-scale criterion (Remark 4.5) 引入了一个工程近似，但它被明确标注为 probe-scale-relative，且有 verifiable boundary condition。
• Wiki 证据: OMC Wiki 无”各模块已有方法”或”标准做法等价”记录。free-search 确认 metamorphic testing 在 SE 领域已有大量工作（Chen et al. 2018, Segura et al. 2016），但论文明确指出优化是”rare domain where sensitivity analysis, duality, and symmetry supply an inexhaustible stock of provably valid metamorphic relations”——这一判断是准确的，因为一般 metamorphic testing 的 relation 来源是 guessed/mined/crowd-sourced，而本文的 relation 是定理。

公理五：效用公理

• 判定: ⚠️
• 分数: 7
• 依据: 效用评估需要区分两个场景。作为 auditor（验证器），battery 表现出色：0.0% FP vs 54.9% (threshold)、47.7% recall at 0% FP on panel、Youden J=0.48 排名第一、40.4% 检出 execution-blind mutants。这些绝对值在”无参考模型验证”这一设定下是可用的。作为 selector（选择器），battery 表现参差：在 NL4OPT 上不优于 plain majority（weighted vote 38.5% vs majority 39.7%），在 MAMO EasyLP/ComplexLP 上 hard filtering 反而降低准确率（8.4% vs majority 5.1% 在 EasyLP；6.2% vs 4.7% 在 ComplexLP），只有在 IndustryOR 上 hard filtering 胜出（+8.0 点）。论文诚实地报告了这一 trade-off 并解释了原因（27.6% label-matching candidates 携带 certified role violation，即 metric 奖励了错误结构）。但问题在于：作为 selector 时，battery 在 3/4 benchmark 上未带来净正效用，这限制了它的实际部署价值。此外，所有实验仅基于单一 7B generator（Qwen2.5-7B），未测试更大模型或不同家族，utility 的泛化性存疑。benchmark pool 中三个使用 prefix subset（MAMO EasyLP 297/652, ComplexLP 128/211），覆盖率不足。
• Wiki 证据: OMC Wiki 无 SOTA 记录。free-search 确认 ORLM、OptMATH、OptiBench 等后续工作均以 execution accuracy 为核心指标，本文是首个以 verification（而非 generation quality）为目标的系统性工作，因此不存在直接的效用 SOTA 对比对象。ReLoop 是唯一切近的 baseline，论文对其进行了严格慈善的重实现。

公理六：新颖性公理

• 判定: ✅
• 分数: 8
• 依据: 新颖性是真实的理论增量，不是已有方法的换名或拼装。与最切近前驱 ReLoop (Lian et al. 2026, arXiv:2602.15983, 2026-02-17) 的区别是本质性的：(1) ReLoop 用阈值 τ=5% 判断目标值是否移动，论文证明任何固定阈值不可能同时 sound 和 nontrivial（Prop 5.7），并用 certified crush 替代；(2) ReLoop 只检查 presence（约束是否存在），论文导出六个结构测试类，每个基于不同的优化理论工具（对偶、单调性、多面体极限、对称性）；(3) ReLoop 没有 soundness statement、没有 detection limit characterization、没有 detectability map，论文提供了全部三者。理论贡献（Theorem 5.6 class-by-error detectability + Prop 5.1-5.3 impossibility results）在 LLM-for-optimization 领域是首次。跨领域迁移（灵敏度分析 → 验证）不是简单搬运——传统灵敏度分析假设模型正确、用于解释；本文反转为模型可疑、用于 falsification，且需要处理 typed slots 和 oracle-free 约束。扣分点：Section 6 的 two-pass JSON IR interface 与 ReLoop 的 structured modeling 有概念重叠，虽然论文将其定位为”making data binding first-class”而非新方法，但这一部分的增量贡献较弱。
• Wiki 证据: OMC Wiki 无”核心 idea 是否已有”记录。free-search 确认 ReLoop (2026-02) 与本文 (2026-07) 间隔约 5 个月，不构成 concurrent work。metamorphic testing 在优化领域的应用未见先例——现有 metamorphic testing 工作集中在 DL 模型、Datalog 引擎、轨迹预测等，未涉及 LP/MILP 的 duality-based verification。

公理七：可复现公理

• 判定: ✅
• 分数: 8
• 依据: 论文声明”All code, data, and an open-source verifier accompany the paper”，且 Section 7 明确指出”Every number in this section is reproducible from a named artifact file, and the CPU stages, from the battery and the mutation study to the audits and post-processing, reproduce identically end to end on a second, independent machine.”。使用公开数据（NL4OPT, MAMO, IndustryOR）、公开 solver（HiGHS）、local open-weight model（Qwen2.5-7B-Instruct），无闭源 API 依赖。实验细节充分：N=8 candidates（1 greedy + 7 at temp 0.8）、prefix subset 定义、solver time-limit rule、per-run JSON artifacts。probe 复杂度有明确分析（Prop 5.8: O(p+E²+R) solver calls, 实测 ~25 solves, 0.01s/model）。扣分点：(1) 代码链接在论文中未给出具体 URL（仅 textual statement）；(2) 三个 benchmark pool 使用 prefix subset，完整 benchmark 的扩展脚本虽包含在 replication package 中，但未实际运行；(3) LLM-judge baselines 仅在 full panel 上评测，未在所有 benchmark 上运行。
• Wiki 证据: OMC Wiki 无”可复现”相关记录。论文的 reproducibility 声明具体且可验证（named artifact files, second-machine replication），但需要实际获取代码包确认。

总评

• 科学价值: 高 — 首次为 LLM 生成优化模型的验证提供了形式化理论框架，包含 soundness 保证、detection limit characterization 和 class-by-error detectability map，且理论预测被实验复现包括零点。
• 方法价值: 高 — 从经典优化理论导出的六类结构测试 + 四类 coherence 测试构成一个完整且可扩展的验证 battery，two-scale criterion 解决了 prohibitive limit 的实现问题且 probe-scale boundary 可验证。
• 社区价值: 高 — 直接解决了 LLM-for-optimization 领域的 adoption bottleneck（无参考模型时的验证），open-source verifier 可被下游工作直接使用，且作为 by-product 发现了公共基准的标签缺陷。

日报摘要

• Strength: 从 LP 对偶、比较静态和多面体极限导出六类 sound 结构测试，0.0% 假阳性 vs ReLoop 阈值法的 54.9%，并在 326 个 NL4OPT faithful seeds 上复现了理论的 class-by-error detectability matrix 包括其零点。
• Weakness: 作为选择器在 4 个 benchmark 中 3 个未超过 plain majority voting，且全部实验仅基于单一 Qwen2.5-7B generator，三个 benchmark pool 使用 prefix subset，utility 泛化性证据不足。

打分

加权总分: 7.7/10（加权分之和 77.0 / 权重之和 9.5） 最终建议: Weak Accept