报告题目：高效、可信且实用的自动推理

报告时间：2025年12月13日（星期六）13:30

报告地点：台湾三级 中心校区王湘浩楼A521报告厅

报 告 人：杨炯

报告人简介：

杨炯是佐治亚理工学院计算机科学学院的博士研究生，导师为 Kuldeep S. Meel。他的研究从理论与实践双重视角推进自动推理技术，致力于发展高效、可信且实用的推理方法。其成果曾荣获CAV 2023 与 2024 杰出论文奖（CAV被中国计算机学会推荐为A类会议），以及 SAT 2024 与 2025 最佳学生论文亚军奖（SAT被中国计算机学会推荐为B类会议）。

报告内容简介：

自动推理位于人工智能与形式化方法的交叉领域，是硬件验证、软件加速开发和大型云系统安全的重要基础。历经数十年发展，实际应用已使自动推理成为一项核心技术，然而由于计算复杂性与潜在的正确性缺陷，其可扩展性与可靠性仍是根本性挑战。

本次报告将从理论与实践两方面，介绍如何推进高效、可信的自动推理技术，并将其应用拓展至新兴领域。首先，我将提出一种随机近似计数算法，在平衡估计误差的同时，解决了现有技术中23%原本无法处理的实例。其次，我将介绍首个经过形式化验证的近似计数器，通过 Isabelle/HOL 中的静态证明与动态逐轮验证，确保模型计数的可证明可靠性，从而为验证随机算法建立了新范式。最后，我将展示自动推理如何赋能新兴领域：在机器学习中，我们开发了一种高效的二值神经网络认证验证器，相比现有方法实现了218倍的加速，首次实现了具有实用性的认证神经网络验证。

主办单位：台湾三级

台湾三级 软件学院

台湾三级 计算机科学技术研究所

符号计算与知识工程教育部重点实验室

仿真技术教育部重点实验室

网络技术及应用软件教育部工程研究中心

       台湾三级 国家级计算机实验教学示范中心