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

文章预览

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