ORSMT：用SMT语义验证与修复LLM优化建模

ORSMT用SMT语义验证提升LLM优化建模的模型-代码匹配率。

资讯摘要

论文提出ORSMT，用类型化语义接口和精确SMT关系查询，对LLM生成的优化模型、求解器代码与报告做语义比对，可证明或反驳可行域与目标关系，并定位到相关行或域。作者报告在3,034个问题、六种生成器规模共72个组合上均提升模型-代码匹配率；受保护选择将总体匹配率从43.2%升至88.2%，正确且匹配比例从25.2%升至40.2%。

要点速读

1. ORSMT通过类型化语义接口与精确SMT查询，对齐可观测决策、投影辅助变量，并证明或反驳可行域与目标关系。
2. 作者报告在3,034个问题、六种生成器规模的72个基准与生成器组合上，选择前模型-代码匹配率全部提升。
3. 受保护选择使总体匹配率由43.2%升至88.2%，正确且匹配比例由25.2%升至40.2%；1,905个被反驳输出经认证投票后50.9%正确且匹配。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/23 08:00:11（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。