AI for Math - 大语言模型在定理证明与数学形式化上的一些实践

摘要：

近期，基于大语言模型的AI技术 ChatGPT 尤其是 GPT-4 的推出，让世人惊叹通用人工智能（Artificial General Intelligence, AGI）的时代是否已经提前到来。的确，ChatGPT 已经在文本分类“机器翻译、文本摘要、常识问答等大多数自然语言处理的传统任务上达到了类人甚至超人的效果。然而，在符号推理、数学推理等任务上，ChatGPT 仍然具有较大的改进空间。在这次演讲中，我将介绍近期我们应用大语言模型在自动定理证明与数学形式化等问题上的一些结果，并探讨未来使用AI辅助进行数学研究的一些可能。

主讲人简介：

 

刘征瀛，华为诺亚方舟实验室AI基础理论团队研究员，研究方向为神经定理证明（Neural Theorem Proving）及 AI4Math。博士毕业于巴黎萨克雷大学（Université Paris-Saclay）人工智能方向，师从 Isabelle Guyon （SVM算法提出者之一、2017年 NeurIPS 大会主席、AutoML 研究的先驱和倡导者），博士主攻方向是自动化深度学习，研究如何把 AutoML 技术应用到深度学习领域（比如自动设计神经网络架构）。研究成果发表在 CCF A类期刊 IEEE TPAMI、A类会议 NeurIPS、PMLR 和 Elsevier PRL 等期刊及会议上。硕士学位在巴黎综合理工学校（Ecole polytechnique）获得，基础数学和计算机科学双学位。本科毕业于北京大学元培学院，获得物理和数学双学位。