第三十八期 求解器产学研生态：现状与道路
2026年3月20日-22日
会议日程
3月20日（周五）上午
开幕式、特邀报告 + 主题1：求解器主流算法：现状与局限
主持人：陆品燕
| 时间 | 内容 |
|---|---|
| 09:00-09:20 | 开幕式 |
| 致辞：朱巧明 秀湖会议AC副主席、苏州大学 教授 | |
| 致辞：蔡少伟 秀湖会议执行主席、北京航空航天大学/中科院软件所 教授 | |
| 09:20-10:00 | 特邀报告1：从新的应用中形成新的研究问题 |
| 特邀嘉宾：张健 中国科学院软件研究所 研究员 | |
| 10:00-10:40 | 特邀报告2：集成电路和系统EDA中的数学求解器问题分析和展望 |
| 特邀嘉宾：方君 上海概伦电子股份有限公司 副总裁 | |
| 10:40-11:10 | 茶歇 |
| 11:10-11:30 | 观点报告1：逻辑与理论的博弈：SMT求解器的演进之路 |
| 发言嘉宾：马菲菲 中国科学院软件研究所 研究员 | |
| 11:30-11:50 | 观点报告2：电路仿真求解器的关键技术与挑战 |
| 发言嘉宾：金洲 浙江大学 教授 | |
| 11:50-12:10 | 观点报告3：约束规划求解算法思考与实践 |
| 发言嘉宾：雷震东 华为泰勒实验室 助理首席专家 |
3月20日（周五）下午
主题2：求解器遇见AI
主持人：马菲菲
| 时间 | 内容 |
|---|---|
| 14:30-14:50 | 观点报告1：AI算法学家：用AI辅助算法设计的尝试 |
| 发言嘉宾：卜东波 中国科学院计算技术研究所 研究员 | |
| 14:50-15:10 | 观点报告2：大模型时代求解器研究的探索和思考 |
| 发言嘉宾：蔡少伟 北京航空航天大学/中科院软件所 教授 | |
| 15:10-15:30 | 观点报告3：基于约束求解的AI系统测试 |
| 发言嘉宾：罗川 北京航空航天大学 教授 | |
| 15:30-16:00 | 茶歇 |
| 16:00-17:30 | 分组讨论：主流求解器的瓶颈？AI对求解器研究和产业的影响，如何发展？ |
3月21日（周六）上午
特邀报告 + Panel讨论
主持人：蔡少伟
| 时间 | 内容 |
|---|---|
| 09:00-09:40 | 特邀报告1：数学规划求解器：历史演进、算法范式与未来趋势 |
| 发言嘉宾：叶荫宇 斯坦福大学杰出终身教授 | |
| 09:40-10:20 | 特邀报告2：密码技术与人工智能安全 |
| 发言嘉宾：王小云 中国科学院院士 清华大学教授 | |
| 10:20-11:00 | 合影、茶歇 |
| 11:00-12:00 | Panel专题讨论：叶荫宇、张健、方君、陆品燕、袁明轩、刘伟峰 |
3月21日（周六）下午
主题3：求解器产业应用：挑战与未来
主持人：卜东波
| 时间 | 内容 |
|---|---|
| 13:30-13:50 | 观点报告1：求解器产业应用与结合大模型的技术发展趋势 |
| 发言嘉宾：袁明轩 华为香港诺亚方舟实验室 主任 | |
| 13:50-14:10 | 观点报告2：求解器在工业界的应用 |
| 发言嘉宾：王子卓 杉数科技 首席技术官 | |
| 14:10-14:30 | 观点报告3：从算法能力到产业落地：求解器应用的真实门槛 |
| 发言嘉宾：林锦坤 晞德求索 首席技术官 | |
| 14:30-14:50 | 观点报告4：程序分析与验证中的约束求解 - 以符号执行为例 |
| 发言嘉宾：陈振邦 国防科技大学 教授 | |
| 14:50-15:50 | 集中研讨：求解器应用难点、产研差距与路径 |
| 15:50-19:00 | 户外交流 |
3月22日（周日）上午
主题4：求解器人才培养
主持人：陈振邦
| 时间 | 内容 |
|---|---|
| 09:00-09:20 | 观点报告1：国产多核实时操作系统微内核形式验证 |
| 发言嘉宾：詹乃军 北京大学 教授 | |
| 09:20-09:40 | 观点报告2：最优化算法与理论人才培养 |
| 发言嘉宾：文再文 北京大学 教授 | |
| 09:40-10:00 | 观点报告3：求解器方向人才培养案例分析 |
| 发言嘉宾：俞扬 南京大学 教授 | |
| 10:00-10:20 | 观点报告4：从学术创新到工程落地：解法器人才培养的关键缺环 |
| 发言嘉宾：刘伟峰 中国石油大学(北京) 教授 | |
| 10:20-10:50 | 茶歇 |
| 10:50-12:00 | 集中讨论：人才培养、产学研生态发展 |
3月22日（周日）下午
主持人：蔡少伟、陆品燕
| 时间 | 内容 |
|---|---|
| 14:00-14:40 | 分组研讨—专题报告讨论 |
| 14:40-15:40 | 全体研讨—总体发展报告讨论 |
| 15:40-16:00 | 会议总结与闭幕 |
特邀嘉宾
| 王小云 | 清华大学 | 中国科学院院士 |
| 叶荫宇 | 斯坦福大学杰出终身教授 | 冯·诺依曼理论奖得主 |
| 张健 | 中国科学院软件研究所 | CCF会士 |
| 方君 | 上海概伦电子股份有限公司 | 副总裁 |
参会嘉宾（姓氏拼音排序）
| 卜东波 | 中国科学院计算技术研究所 | 研究员 |
| 陈振邦 | 国防科技大学 | 教授 |
| 金燕 | 华中科技大学 | 副教授 |
| 金洲 | 浙江大学 | 教授 |
| 雷震东 | 华为泰勒实验室 | 助理首席专家 |
| 李宏博 | 东北师范大学 | 副教授 |
| 林锦坤 | 晞德求索 | 首席技术官 |
| 刘伟峰 | 中国石油大学（北京） | 教授 |
| 罗川 | 北京航空航天大学 | 教授 |
| 马菲菲 | 中国科学院软件研究所 | 研究员 |
| 皮良 | 杉数科技 | 技术专家 |
| 王子卓 | 杉数科技 | 首席技术官 |
| 文再文 | 北京大学 | 教授 |
| 俞扬 | 南京大学 | 教授 |
| 袁明轩 | 华为香港诺亚方舟实验室 | 主任 |
| 詹乃军 | 北京大学 | 教授 |
秀湖会议学术委员会（AC）副主席
| 朱巧明 | 苏州大学 | 教授 |
会议执行主席
| 蔡少伟 | 北京航空航天大学/中国科学院软件研究所 | 教授 |
| 陆品燕 | 上海财经大学 | 教授 |
会议工作人员
| 初一 | 中国科学院软件研究所 | 副研究员 |
| 张昕荻 | 中国科学院软件研究所 | 特别研究助理 |
| 陆梦 | 华为泰勒实验室 | 研究员 |
| 侯雯颖 | 华为泰勒实验室 | 研究员 |
赞助单位
秀湖会议年度合作伙伴：OPPO
秀湖会议金牌合作伙伴：联想
特邀嘉宾介绍
 | 叶荫宇，原斯坦福大学李国鼎讲席教授，现任上海交通大学, 上海数学交叉科学院，香港中文大学深圳和香港科技大学访问讲席教授。他的主要研究方向为连续和离散优化，数据科学及应用，数字算法设计及分析，算法博弈及市场均衡，运筹及管理科学等; 他和其他科学家开创了内点优化算法，锥规划模型，分布式鲁棒优化，在线线性规划和学习，强化学习和马可夫过程及 非凸优化算法分析等。他和他的学生多次获得科学奖项: 包括他自己的2006 INFORMS Farkas Prize (首位获奖者)，2009年约翰·冯·洛伊曼理论奖，国际数学规划2012 Tseng Lectureship Prize (首位获奖者每三年) ，2014美国工业及应用数学学会优化奖(每三年), 2025 Constantin Caratheodory Prize of the 全局优化 Congress, 等。 |
 | 王小云，清华大学高等研究院杨振宁讲座教授，中国科学院院士，发展中国家科学院院士，国际密码协会会士，中国密码学会理事长，CCF网络与系统安全专委会主任。主要从事密码理论及相关数学问题研究。提出了密码哈希函数的碰撞攻击理论，破解了包括MD5、SHA-1在内的5个国际通用哈希函数算法；主持设计的哈希函数SM3为国家密码算法标准，并于2018年10月正式成为ISO/IEC国际标准；提出高维格数学难题SVP的二重筛法，证明带Gap格具有理论最优上界的反转定理；带领团队设计了SCloud等性能卓越的后量子密码算法，研发“大圣”区块链共识协议并应用于多边央行数字货币桥项目，支撑数字人民币跨境支付。在国际密码学三大顶会——美密会、欧密会、亚密会上共获得四次最佳论文奖。曾获国家科技进步一等奖，国家自然科学二等奖，北京市突出贡献中关村奖，国际密码协会最具时间价值奖，真实世界密码学奖，世界杰出女科学家奖，未来科学大奖——数学与计算机科学奖。 |
 | 张健，中国科学院软件研究所研究员，中国科学院大学岗位教授，博士生导师。主要研究兴趣包括：软件测试与分析、自动推理、约束求解等。主持了国家杰出青年科学基金、国家973计划等项目。曾先后获中创软件人才奖、国务院政府特殊津贴、中国计算机学会自然科学一等奖等荣誉。目前担任《计算机学报》，Journal of Computer Science and Technology, Frontiers of Computer Science,《计算机科学与探索》等期刊编委。 |
 | 方君，现任上海概伦电子股份有限公司研发副总裁，有20年的的EDA算法研究和从业经验，专注于模拟/射频、数字和混合信号电路仿真，以及集成电路寄生参数提取和电路可靠性分析等领域的前沿研究和产品研发，获得多项EDA技术专利授权。于2007年6月获复旦大学微电子学与固体电子学硕士学位，2007年7月至2010年6月曾任Cadence北京研发中心软件工程师。2022年获上海市科技进步奖二等奖(第一完成人)。 |
观点报告嘉宾介绍
 | 卜东波，中科院计算所研究员，研究兴趣包括生物信息学、计算机算法。在Nature子刊、AC、NAR、RECOMB/ISMB等期刊和会议发表论文100余篇，著有《算法讲义》；带领六名“计算所二代”小学生组成小SIGMA数学特别兴趣组，讲授数学思维和计算思维，并与之合著《少儿计算思维养成记---六个小孩的编程学习笔记》。研制了“用人工智能技术辅助算法设计”的AIA系统，设计并领导了PEARL“珍珠计划”，首次获得了中国高校人际近距离物理接触真实数据，发现了不同于scale-free/small-world的特有接触模式；设计并领导了LAMP计划，获得了迁徙过程中人类肠道菌群真实数据，发现了肠道菌群的“高弹性”；设计了蛋白质结构预测算法ProFOLD与蛋白质序列设计算法ProDESIGN；与基因组所等合作研制了 DNA 活字存储喷墨打印机“毕昇一号”，将文本、图像、音频、视频多类型数据存储入DNA，进而转入大肠杆菌存储，实现100%成功读取。 |
 | 陈振邦，国防科技大学计算机学院教授、博士生导师，主要研究方向为程序分析、形式化方法及其在不同背景下的应用。近年来主要围绕符号执行相关的理论、技术和应用开展研究，成果发表在OOPSLA、FM、ICSE、FSE、ISSTA、ASE、TOSEM等重要国际会议或期刊上，获ACM SIGSOFT杰出论文奖3次。获国家科技进步二等奖1项、省部级科学技术进步一等奖1项、二等奖2项，获NASAC青年软件创新奖。 |
 | 金洲，浙江大学百人计划研究员，博导，入选国家高层次青年人才计划，CCF集成电路设计专委会副秘书长。主要从事集成电路设计自动化（EDA）方面的研究工作，发表DAC、SC、TCAD、ICCAD、DATE等国际高水平学术会议期刊论文70余篇，获SC’23最佳论文奖（中国首次）、SC’24、PPoPP’26、DATE’26最佳论文提名，及WAI’25、HPEC’25、ISEDA’23等多项最佳论文奖，首届EDA2青年科技奖（全国唯一）、IEEJ九州支部长奖、北京前沿学术成果等。主持国家自然科学基金数学天元基金交叉重点青年专项、重大研究计划培育项目、青年项目、重点研发计划子课题、华大九天／中科曙光等头部企业横向课题等20余项。 |
 | 雷震东，华为泰勒实验室研究员，智能决策团队负责人。当前主要研究方向包括求运筹优化与解器技术，机制设计，以及与AI的结合等。有10年求解器研发经验，以第一作者在AAAI/IJCAI等顶级会议发表多篇论文，在国际MaxSAT求解器比赛中连续获得多次冠军（2021-2023），曾获得国际逻辑联合会议颁发的奥林匹克金牌，中科院院长特别奖，华为金牌个人等荣誉。 |
 | 林锦坤，晞德求索公司联合创始人、首席技术官，海英人才，中国计算机学会集成电路专委会执行委员，北京大学计算机软件与理论博士。主要研究方向为约束求解器和软件工程，在人工智能、软件工程顶级学术会议和期刊发表多篇论文，所参与研发的 SMT 求解器获得国际 SMT 比赛金牌，整数规划求解器在 MIPLIB 基准测试中累计刷新超过 10 个公开实例的世界纪录。 |
 | 刘伟峰，中国石油大学（北京）教授、博士生导师、欧盟玛丽居里学者，2002年和2006年于中国石油大学（北京）计算机系获学士与硕士学位；2006年至2012年在中国石化石油勘探开发研究院从事高性能地球物理算法研究；2016年于丹麦哥本哈根大学获计算科学博士学位。主要研究高性能数值线性代数，尤其关注稀疏矩阵的领域专用架构、数据结构、并行与分布式算法和解法器数学软件。研究工作发表于SC、PPoPP、ASPLOS、DAC、ICS、IPDPS、ICPP和TPDS等重要国际会议和期刊，获得了SC 2023最佳论文奖、SC 2017、2024和PPoPP 2026最佳论文提名奖，以及HiPEAC论文奖等奖项。他担任了SC、PPoPP、ICS、IPDPS和ICPP等会议的程序委员会委员和TPDS等期刊的审稿人。他是CCF高性能计算专业委员会委员、IEEE高级会员、CCF高级会员，以及ACM和SIAM会员。 |
 | 罗川，北京航空航天大学教授，博士研究生导师，国家自然科学基金青年科学基金项目（B类）负责人，北航软件学院关键基础软件所副所长。围绕约束求解研究方向，开展了一系列创新的学术研究工作。已入选中国科协青年人才托举工程。迄今总计发表CCF-A类论文超过40篇。担任多个国际学术会议的领域主席、（资深）程序委员会成员。作为负责人主持多项国家级科研项目，包括国家重点研发计划课题、国家自然科学基金项目等。在国际知名约束求解竞赛中多次获得冠军，包括来自亚洲参赛者的首个冠军。研究工作获得国际知名学者（包括诺贝尔奖得主）实际使用或正面评价。研究成果被国家电网、航天科工集团、华为、微软成功应用，有效提升了云系统、编译器、体系设计软件等关键系统软件的性能和可靠性。 |
 | 马菲菲，中国科学院软件研究所研究员，博导，中国科学院大学岗位教授。研究方向为自动推理和约束求解，系统研究了SMT及其优化问题和解计数问题，并研发了相应求解器。成果发表于IJCAR、ISSAC、CP、SAT、TCS、IJCAI、AAAI、JAIR、NeurIPS、ICCV、EMNLP、ISSTA、ASE等国际高水平会议或期刊上。曾获中国科学院青年创新促进会优秀会员，ACM SIGSOFT杰出论文奖，省部级一等奖一项，省部级二等奖一项。 |
 | 王子卓，香港中文大学（深圳）数据科学学院教授、副院长，同时为杉数科技联合创始人、首席技术官。王子卓本科毕业于清华大学数学系，2012年获斯坦福大学管理科学与工程博士学位。王子卓曾为明尼苏达大学工业与系统工程系终身教授。现担任广东省人工智能数理基础重点实验室主任，为国家海外高层人才青年项目、国家杰出青年项目获得者。王子卓教授的主要研究方向为机器学习及运营管理。在运筹学和管理科学国际顶尖杂志上发表过超过60篇文章，并担任运营管理方面国际顶尖杂志MS, OR, MSOM, POMS等编委。2016年起，王子卓与他人共同创立杉数科技并担任CTO，过去九年在国内为超过三百家企业做智能决策方面的咨询与服务，客户包括京东，顺丰，滴滴，华为，南航等国内领头企业。 |
 | 文再文，北京大学北京国际数学研究中心长聘教授，北京大学博雅特聘教授，主要研究最优化算法与理论、机器学习、人工智能。2016年获中国青年科技奖。2020年获国家万人计划科技创新领军人才，入选2023年度教育部长江学者特聘教授，现为中国运筹学会副理事长。《最优化：建模、算法与理论》入选十四五国家重点出版物出版规划项目，《最优化方法与理论》入选教育部101计划核心教材和十四五普通高等教育本科国家级规划教材，该系列教材累计印刷13次超3.2万册。 |
 | 俞扬，南京大学人工智能学院教授，副院长。主要从事人工智能、机器学习、强化学习方向的研究，提出演化学习理论与开放环境强化学习方法，工作获5项国际论文奖、3项国际算法竞赛冠军。曾获全国优秀博士学位论文奖，中国计算机学会优秀博士学位论文奖。入选国家青年人才计划、IEEE Intelligent Systems “AI’s 10 to Watch”，获CCF-IEEE青年科学家奖，首届亚太数据挖掘“青年成就奖”，并受邀在国际人工智能联合大会 IJCAI 2018上作“青年亮点报告”。 |
 | 袁明轩，当前担任华为诺亚方舟实验室高级研究员和香港诺亚方舟实验室主任。他博士毕业于香港科技大学，研究兴趣包括学习优化、AI求解器、AI4EDA和大模型应用等。他曾担任华为AI应用创新实验室主任，并主导负责企业智能（供应链优化与企业服务等）、AI4EDA、AI求解器和行业智能项目， 带领团队完成了行业大模型应用、供应链（排产引擎、物流数字化装箱装柜、仓库仿真与调度等）、自研求解器替代、求解器AI特性、存储智能调度、港口水平调度、EDA自研工具系列算法（比如DSE、逻辑综合、ATPG、LEC、2D/3D布局等等）和电信大数据时空数据分析引擎、用户离网预测等算法与模型研发上线与产品化。 |
 | 詹乃军，北京大学计算机学院博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科学院大学岗位教授，计算机科学国家重点实验室执行主任。分别在南京大学数学系（1989-1993）和南京大学计算机系（1993-1996）获得学士和硕士学位，在中国科学院软件研究所获得博士学位（1997-2000）。研究方向包括：形式化方法，实时、嵌入式、混成系统，程序验证等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》《电子学报》、《前瞻科技》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如形式化方法旗舰会议FM 2021 和验证领域顶级会议TACAS 2027）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文150多篇，出版专著2部，编著4部，国际国内著名杂志专刊7辑等。现任CCF形式化方法专委主任。 |
秀湖会议学术委员会（AC）副主席介绍
 | 朱巧明， 博士，苏州大学计算机科学与技术学院博士生导师、二级教授，现任江苏省大数据智能工程实验室主任，苏州大学人工智能研究院院长，中国中文信息学会常务理事，中国计算机学会系统软件专业委员会、自然语言处理技术专委和和信息系统专委会委员、《中文信息学报》第五届编委；长期从事计算机中文信息处理技术研究，目前主要研究方向：人工智能、自然语言处理和知识图谱。 曾获江苏省“333新世纪科学技术带头人培养工程”培养对象，苏州大学中青年学术带头人。1999年获江苏省科技进步三等奖，2001年获江苏省优秀教学成果一等奖，2003年获苏州市“十大”杰出青年称号，2005年获苏州大学首届教学名师，2006年获江苏省教学名师。2011年获教育科技进步二等奖，2015年获江苏省科技进步三等奖。先后主持完成国家863项目1项，国家自然基金重点项目1项，面上项目3项目、教育部博士点基金项目2项，江苏省自然基金2项目、江苏省前瞻性研究项目2项，合作出版学术著作2部， 在国内外核心学术期刊上发表论文100篇。 |
会议执行主席介绍
 | 蔡少伟， 北京航空航天大学教授，中科院软件所兼职研究员，主要研究约束求解及其应用，主持国家自然科学基金重点项目和青年B项目。获得领域顶级会议CAV、CP和SAT的最佳论文奖/杰出论文奖，多次获得国际SAT比赛和SMT比赛冠军，为混合整数规划榜单MIPLIB/MINLPLIB/QPLIB刷新了50多个求解记录，华为鸿蒙创新大赛一等奖，与山东大学合作获得强网杯密码数学专项赛冠军。其求解器被集成到英伟达、微软、英特尔、华大九天等公司的软件中，应用于EDA、操作系统验证、云平台故障检测、以及工业调度。担任SAT 2027会议程序委员会共同主席，EDA^2形式化验证标准组组长，《EDA技术白皮书》形式化验证方向主编，曾在FMCAD、CP和SOCS等国际会议做特邀报告。 |
 | 陆品燕，上海财经大学“长江学者”特聘教授。他的主要研究方向 是理论计算机，并注重与其它学科的交叉，特别是计算机与经济 学的交叉。他在理论计算机的三大会议 STOC/FOCS/SODA 共发 表论文 30 余篇，在计算经济学的两大顶级会议 EC/WINE 共发 表论文 20 余篇。荣获 ICALP2007、FAW2010、ISAAC2010、 AAMAS2024、WINE2025 等重要国际会议最佳论文奖/杰出论文 奖。曾荣获 ACM 杰出科学家奖(2019)、第八届世界华人数学家 大会 ICCM 数学奖(原晨兴数学奖)银奖(2019)、中国计算机 学会青年科学家(2014)等荣誉。 |
会议工作人员介绍
 | 初一，中国科学院软件研究所副研究员，研究方向为约束优化问题求解。研究成果发表于AAAI、SAT、CP等国际会议，在2022年和2023年国际MaxSAT比赛中获非完备赛道冠军。 |
 | 张昕荻，中国科学院软件研究所特别研究助理，研究兴趣为约束求解及EDA形式化验证，于CAV、DAC、SAT、FM等会议及期刊发表学术论文20余篇。其研究工作获评国际SAT协会“最佳博士学位论文奖”（亚洲首个）、国际SAT会议“最佳论文奖”（亚洲首个）、中国科学院优秀博士学位论文等。 |
 | 陆梦，华为泰勒实验室求解器研究员，目前从事对称性算法开发和求解器硬件加速方向研究、在预处理、单纯形、内点法等求解器方向有着多年实战经验。 |
 | 侯雯颖，华为泰勒实验室求解器研究员，目前从事MIP、CP求解器的启发式算法研究，在局部搜索算法、元启发式算法设计上有多年的实战经验。 |
京公网安备 11010802032778号