计算与应用讨论班——Towards an AI Mathematician

来源：数学科学学院发布时间：2024-10-04 10

报告人：Kaiyu Yang（Meta Fundamental AI Research (FAIR) team）

时间：2024年10月4日上午10:00

地点：https://meeting.tencent.com/dm/cC3EArPcmTBL

#腾讯会议：371-435-370

摘要：Mathematics is a hallmark of human intelligence and a long-standing goal of AI. It involves analyzing complex information, identifying patterns, forming conjectures, and performing logical deduction. Many of these capabilities are beyond the reach of current AI, and unlocking them can revolutionize AI applications in scientific discovery, formal verification, and beyond. In this talk, I will present initial steps towards the grand vision of AI mathematicians, taking an approach that combines the generative power of large language models (LLMs) with the logical rigor of formal methods.

Specifically, I will cover our works using LLMs to (1) prove formal theorems in proof assistants such as Coq and Lean and (2) automatically translate human-written mathematics into formal theorems and proofs—a task called autoformalization. For theorem proving, we introduce the entire system for extracting data, training LLMs to generate proof steps, interacting with proof assistants to search for proofs, and deploying the model to assist human users. For autoformalization, using Euclidean geometry as an example domain, we introduce a neuro-symbolic framework that combines LLMs with SMT solvers and domain knowledge. Finally, we discuss future directions for AI mathematicians beyond theorem proving and autoformalization.

个人简历：Kaiyu Yang is a research scientist in Meta Fundamental AI Research (FAIR) team. His research aims to build AI that can understand and reason about mathematics. To that end, he has focused on using machine learning, especially large language models, to prove theorems in formal systems such as Coq and Lean. Before joining FAIR, he was a postdoctoral scholar at Caltech. He received a Ph.D. in computer science from Princeton University and bachelor's degrees in computer science and mathematics from Tsinghua University.

联系人：席亚昆（yakunxi@zju.edu.cn）