本次报告聚焦AI4Math，探讨如何提升AI的数学能力，这不仅具有智力吸引力，还在AI驱动的系统设计与验证中至关重要。报告将介绍一种与自然语言处理技术互补的路径：形式化数学推理，通过Lean等形式系统验证推理的正确性并提供自动反馈。这种方法有望推动AI在数学、形式化验证和可验证代码生成等任务中取得进展。报告人杨凯峪将介绍利用机器学习处理定理证明和自动形式化两项关键子任务，并讨论形式化数学推理中的开放问题和关键里程碑。

💡AI4Math研究旨在提升AI的数学能力，对AI驱动的系统设计与验证具有关键作用。

📚形式化数学推理是一种重要路径，通过Lean等形式系统验证推理正确性并提供反馈，与NLP技术互补。

🤖报告将介绍如何利用机器学习，特别是大型语言模型，处理定理证明（从定理陈述生成形式化证明）和自动形式化（将非形式化的数学转化为形式化数学）两项关键子任务。

👨‍🔬报告嘉宾杨凯峪是Meta FAIR的研究科学家，专注于通过Lean等形式系统增强AI的数学推理能力，研究问题包括数学猜想生成、定理证明以及自然语言与形式语言结合的推理。