形式化方法公开课之定理证明

形式化方法教育

约束求解公开课

一、公开课总体情况介绍

约束求解作为形式化验证与自动化测试等技术的基础引擎，在保障计算机软硬件的正确性和安全性方面起着不可替代的作用，已经在学术界和产业界产生了广泛深远的影响。

"约束求解公开课"是由中国科学院软件研究所蔡少伟和吴志林研究员联合发起的以约束求解及其应用为主题，面向研究生与青年学者以及相关从业人员的公开课程。2022年举行了第一届，由北京智源研究院承办，中国计算机学会形式化方法专业委员会协办。2022年公开课报名人数达200余人，包括高校师生和产业界人士，公开课在学术界和产业界都产生了积极的影响。

基于2022年公开课的成功经验，2023年"约束求解公开课"继续举行。2023年"约束求解公开课"将由中国计算机学会主办，形式化方法专业委员会和中国科学院软件研究所承办，主题为"SMT算术理论求解与神经网络验证"，时间为每周三上午9:30-12:00（从9月13日开始，预计共35学时），线下线上结合。

2023年的"约束求解公开课"将完全免费，不收取任何费用。希望对约束求解及其应用感兴趣的广大研究生及同仁踊跃报名参加，我们期待该公开课对于约束求解在中国的进一步发展起到积极的推动作用。

二、课程安排

1. 主题：SMT算术理论求解与神经网络验证

2. 时间：每周三上午9：30-12：00 （9月13日开始，节假日休息）

3. 授课老师：

SAT/SMT算法部分：

蔡少伟，中国科学院软件所研究员

夏壁灿，北京大学数学学院教授（学术讲座）

神经网络验证部分：

杨鹏飞中国科学院软件所助理研究员

黄小炜利物浦大学教授（学术讲座）

4. 课程大纲

序号	时间	内容	授课老师	回放链接
1	9.13	约束求解简介	蔡少伟	观看回放
2	9.20	基于SMT求解的神经网络验证	杨鹏飞	观看回放
3	9.27	基于抽象解释的神经网络验证	杨鹏飞	观看回放
4	10.11	基于概率方法的神经网络验证	杨鹏飞	观看回放
5	10.18	神经网络验证：其他方法与案例	杨鹏飞	观看回放
6	10.25	Tutorial: Towards Robust Deep Learning Models: Verification, Falsification, and Rectification	黄小炜	观看回放
7	11.1	SAT Encoding and CDCL Algorithm	蔡少伟	观看回放
8	11.8	SMT Encoding and CDCL(T) Algorithm	蔡少伟	观看回放
9	11.22	非线性理论求解简介	夏壁灿	观看回放
10	11.29	等式理论与混合理论的求解	蔡少伟	观看回放
11	12.06	局部搜索算法与混合求解方法	蔡少伟	观看回放
12	12.13	Hybrid Solvers, Preprocessing, and Parallel Solvers for SAT/SMT	蔡少伟	观看回放
13	12.27	SAT/SMT求解与神经网络验证的前沿和挑战	蔡少伟/杨鹏飞	观看回放

三、授课老师简介

蔡少伟，中国科学院软件研究所研究员/博导，中国科学院优秀导师、智源学者、主持国家优秀青年基金和中国科学院战略先导课题，研究兴趣包括约束求解和硬件验证，多次获得国际SAT比赛和SMT比赛冠军，以及相关国际会议最佳论文奖，研发的求解器被应用于芯片验证和云服务故障检测等实际项目。

黄小炜，英国利物浦大学计算机系教授，成立并主导 “可信自主系统实验室”。是神经网络安全性验证的主要倡导者之一。从2018年起一直在AAAI和IJCAI上组织AI安全研讨会。2023年出版专著“Machine Learning Safety”。在多个领域的国际会议和杂志上发表论文超过100篇。研究兴趣主要包括AI的安全，测试，验证和可解释性。

夏壁灿，北京大学数学科学学院教授。中国工业与应用数学会常务理事、中国数学会计算机数学专委会副主任，曾担任北京大学数学科学学院副院长，北京大学数学科学学院信息科学系主任。研究兴趣包括：符号计算，程序与混成系统验证，自动定理证明。

杨鹏飞，中国科学院软件研究所助理研究员，研究方向为AI安全和形式化验证，开发了多个深度神经网络验证的方法和工具，其技术覆盖了抽象解释、SMT、CEGAR、利普西茨常数、PAC模型学习等，在软件工程、形式化方法顶级国际会议ICSE、ESEC/FSE、ICCV、TACAS、CONCUR、SAS等发表学术论文十余篇。