Formalization and theorem proving based on neural-symbolic interaction -

Formalization and theorem proving based on neural-symbolic interaction

Time: 2023-11-13 Published By: Ying Hao

Speaker(s): Xian Zhang (Microsoft Research Asia)

Time: 10:00-11:00 November 17, 2023

Venue: Room 77201, Jingchunyuan 78, BICMR

Abstract: With the development of theorem provers like Lean and Isabelle, formal proof has garnered increasing attention in the mathematics community, with prominent figures such as Peter Scholze and Terence Tao using Lean to assist in validating their research. However, due to the differences between formal language statements and natural language statements, as well as the differences between formal proofs and natural language proofs, the formalization process still requires significant expert knowledge and substantial human intervention. In this talk, I will introduce a framework based on neural-symbolic interaction, which consists of a feedback loop between large language models and theorem provers, augmented with a series of related techniques, to effectively increase the automation level in the formalization process.

Bio: Xian Zhang is a Senior Researcher in the Systems Group at Microsoft Research Asia, with a primary focus on system security, formal methods, and privacy protection in machine learning. He earned his bachelor's and doctoral degrees from the School of Electronics Engineering and Computer Science at Peking University in 2013 and 2018, respectively. He has dozens of works published in international conferences and journals, including top conferences in the field of computer systems such as SOSP, ISCA, MICRO, etc. He has long served as a program committee member for the international conference DSN in the systems and security field. He has participated in several research and product projects within Microsoft, and his work has been covered by media outlets such as Business Insider, Yahoo! Finance, and CNBC.