明日直播｜AI4Math，Meta科学家杨凯峪分享形式化数学推理

报告主题：AI4Math，形式化数学推理，人工智能新前沿

报告日期：02月25日（本周二）10:30-11:30

报告要点:

提升AI的数学能力（AI4Math）不仅在智力上极具吸引力，并且在AI驱动的系统设计与验证中起到关键作用。AI4Math的研究广泛借鉴了自然语言处理（NLP）的技术，尤其是精心收集数学文本数据集，用来训练大型语言模型。本次演讲将讨论一种与之互补但较少被探索的技术路径：形式化数学推理，即通过Lean等形式系统来验证推理的正确性并提供自动反馈。形式化数学推理有可能帮助AI在数学、形式化验证以及可验证的代码生成等任务中取得重大进展。本次，我将介绍利用机器学习（特别是大型语言模型）处理两项关键的子任务：定理证明（从定理陈述生成形式化证明）和自动形式化（将非形式化的数学转化为形式化数学）。最后，我将讨论形式化数学推理中的开放问题和关键里程碑。

报告嘉宾：

杨凯峪是Meta基础人工智能研究团队（FAIR）的研究科学家。他的主要研究方向是通过Lean等形式系统来增强AI在数学推理方面的能力，具体研究问题包括：使用机器学习和大型语言模型生成数学猜想、证明定理，并进行自然语言与形式语言结合的推理。在加入FAIR之前，他本科毕业于清华大学，于普林斯顿大学取得博士学位，并在加州理工学院进行博士后研究。

更多热门报告