基于神经符号交互的形式化及定理证明
发布时间：2023年11月13日
浏览次数：767
发布者: Ying Hao
主讲人： 张宪 （微软亚洲研究院）
活动时间： 从 2023-11-17 10:00 到 11:00
场地： 北京国际数学研究中心，镜春园78号院（怀新园）77201室
摘要：随着Lean及Isabelle等定理证明器(theorem prover)的发展，形式化证明(formal proof)在数学界得到了越来越多的关注，例如Peter Scholze以及Terence Tao等都使用过Lean来辅助验证自己的研究。但是由于形式化语言陈述(statement)与自然语言陈述的差异、以及形式化证明和自然语言证明的差异，形式化的过程中依然需要较高的专家知识以及大量的人力介入。本次分享中，我将介绍一个基于神经符号交互的框架，即大语言模型和定理证明器构成的反馈回路加上一系列相关技术，来有效增加形式化过程中的自动化程度。
主讲人简介：张宪，微软亚洲研究院系统组高级研究员，主要研究方向是系统安全、形式化方法以及机器学习隐私保护。2013年及2018年获得北京大学信息科学技术学院的本科及博士学位。有数十篇工作发表在国际会议及期刊上，包括计算机系统领域的顶级会议SOSP, ISCA, MICRO等。长期担任系统和安全领域国际会议DSN的程序委员会成员。参与了微软内部多个研究及产品项目，相关工作被Business Insider, Yahoo! Finance以及CNBC等媒体报道。
