arXiv:2607.29431cs.AI2026-07

用多维度标准评估大模型生成的优化模型,发现单一评分会掩盖关键差异。

ModelEquivBench: Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models

  • 构建六层语义匹配体系,逐项验证模型等价性
  • 3个模型在173道题中各有49/35/25处误判为有效但实际不等价
  • 支持可复现证据,避免盲目猜测,适合模型评测与可信推理研究者

大语言模型越来越多地从自然语言生成优化模型,但现有评估常简化为是否等价或执行成功,这类标签既不可独立验证,也无法反映两种建模方案可能存在的多种一致性。本文提出ModelEquivBench,一个可认证、多关系的评估系统,对每对模型输出报告包含E0–E6共七项的语义谱系:模型构建与精确输入(E0)、验证后的表示对齐(E1)、同空间及投影可行集关系(E2、E3)、目标顺序等价(E4)、最优值相等(E5)和求解器集等价(E6)。每项结论均附有可独立复核的证据:可重放轨迹或显式映射(E0–E1),精确有理数证书(正向结论E2–E6),以及反例证明(负向支持)。若映射搜索不完整、结构不支持或资源受限,则返回类型化的UNKNOWN或N/A,前提不足则标记为ABSENT。在无修复协议下,对三个模型快照(GPT-5.4、Claude Sonnet 4.6、Qwen3.5-397B-A17B)在173个固定问题(每模型346个单元)上的评估显示,粗粒度基准无法揭示的差异:分别有49、35、25个单元虽可执行却在至少一项关系上被证伪;另有25、8、18次结构拒绝发生于经验证映射下可行集相等的配对。三模型失败阶段各异,故不能简单归结为单一准确率。

原文摘要 · Abstract (English)

Large language models increasingly generate optimization models from natural language, but existing evaluation often reduces a generated model and its ground truth to a single equivalent/not-equivalent verdict or an execution-success rate--labels that are neither independently checkable nor faithful to the multiple distinct senses in which two formulations can agree. We present ModelEquivBench, a certifying, multi-relational evaluation system that reports a per-pair semantic profile E0--E6: model construction and exact ingestion (E0), verified representation alignment (E1), same-space and projected feasible-set relations (E2, E3), objective-order equivalence (E4), optimal-value equality (E5), and optimizer-set equivalence (E6). Each decided entry carries relation-appropriate, independently re-checkable evidence: replayable traces or explicit maps for E0--E1, exact-rational certificates for positive E2--E6 conclusions, and explicit witnesses for supported negatives. Incomplete mapping search, unsupported structure, and resource limits produce typed UNKNOWN or N/A outcomes rather than guesses, while unmet prerequisites are reported as ABSENT. Using ModelEquivBench to evaluate three model snapshots--GPT-5.4, Claude Sonnet 4.6, and Qwen3.5-397B-A17B--on the same frozen cohort of 173 base problems (346 cells per model) under a no-repair protocol, the resulting profiles expose distinctions that coarse baselines do not represent: 49, 35, and 25 cells contain executable candidates that are nevertheless certified negative on at least one supported relation, and 25, 8, and 18 structural rejections occur on pairs for which E2 certifies mapped feasible-set equality under a verified map. The three model snapshots fail at different stages of the profile and therefore cannot be meaningfully reduced to a single accuracy score.

大模型评估优化模型形式化验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。