paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Validating Mixed-Integer Programming Solvers

验证混合整数规划求解器
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 2/10 · 论文研究MIP求解器的正确性测试,属于软件测试与验证范畴,但与用户核心关注的静态分析、LLM/Agent辅助分析、浮点程序分析及贝叶斯程序分析均无直接关联,仅与形式化验证大领域有微弱交集。引用 0 inbox
Xintong Zhou, Zhenyang Xu, Chengnian Sun
crossref: 2026-09-12

AI 速览

一句话:提出可行性驱动的实例生成技术并实现工具 Flip,系统测试 MIP 求解器,发现 67 个真实缺陷。

混合整数规划(MIP)广泛应用于金融、工程与管理科学,MIP 求解器是其计算核心。求解器一旦出错,例如误判可行性或返回错误解,可能造成严重后果;然而,求解器正确性的验证在理论与实践上仍基本空白。本文首次系统性地研究该问题,提出“可行性驱动的实例生成”技术:通过构造可证明为可行或不可行的随机 MIP 实例,将其输入求解器以检测潜在缺陷。作者将该方法实现为工具 Flip,并在五个广泛使用的开源与商业 MIP 求解器上进行评估。截至目前,Flip 共发现 67 个已确认的缺陷,其中 54 个已被开发者迅速修复,相关工作与发现获得 MIP 求解器社区的认可。

问题
MIP 求解器被广泛使用,但其正确性验证在理论与实践中都几乎没有被系统研究,错误结果可能带来严重后果。
方法
提出可行性驱动的实例生成技术,通过构造可证明可行或不可行的随机 MIP 实例来测试求解器,并实现工具 Flip。
评估
在五个广泛使用的开源与商业 MIP 求解器上运行 Flip,共发现 67 个已确认缺陷,其中 54 个已被修复,并获得社区认可。
原文摘要(Abstract)

Mixed-integer programming (MIP) is a fundamental class of mathematical optimization problems with broad applications in various domains such as finance, engineering, and management science. MIP solvers, software systems that automatically solve MIP problems, serve as the computational backbone for these applications. Given their widespread use, ensuring the correctness of MIP solvers is crucial, as incorrect results, such as falsely determining feasibility or returning incorrect solutions, can lead to serious real-world consequences. Despite its importance, validating the correctness of MIP solvers remains largely unexplored in both theory and practice. This paper presents the first systematic effort to address this problem. We propose feasibility-driven instance generation, a simple yet effective technique to generate random MIP instances for testing solver correctness. The core idea is to systematically synthesize MIP instances that are provably feasible or infeasible by construction. These instances are then fed to MIP solvers to detect potential bugs. We realize this methodology in Flip. To date, Flip has uncovered 67 confirmed bugs in five widely used MIP solvers, spanning both open-source and commercial systems. Among these, 54 have been promptly fixed by the developers. Our efforts and findings have been well acknowledged by the MIP solver community.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot11730,
  title = {Validating Mixed-Integer Programming Solvers},
  author = {Xintong Zhou and Zhenyang Xu and Chengnian Sun},
  booktitle = {ICSE},
  year = {2026},
  doi = {10.1145/3744916.3787827}
}