基于神经符号交互的形式化及定理证明
发布时间:2023年11月13日
浏览次数:1587
发布者: 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等媒体报道。