2026年7月25日，在国际联合逻辑大会(FLoC 2026)上公布了第21届国际可满足性模理论求解竞赛(SMT-COMP)的结果。中国科学院工业人工智能研究所可信智能软件团队研发的Z3++求解器荣获多项冠军，其中包括非线性整数理论(QF_NIA)和数据类型理论(QF_DT)两个分赛道冠军，并获得一项总成绩冠军。主要完成人是助理研究员李博涵和实习生焦世豪。

SMT-COMP始于2005年，是SMT领域历史最悠久、影响力最广泛的年度赛事。SMT求解器是形式化验证和可信软件保障的核心基础约束求解引擎。本届赛事吸引了来自斯坦福大学、剑桥大学、微软研究院、国际斯坦福研究所等全球顶尖高校和研究机构的团队参与。

Z3++求解器是基于国际主流求解器Z3的衍生求解器，此前已多次获得SMT-COMP冠军，并且其多项主要创新技术已经被集成进Z3。今年的比赛中，可信智能软件团队基于自研的大模型自动算法演化框架，进一步显著提升了求解性能。