报告题目：Large Language Models for Automated Theorem Proving
报告人：李泽南 博士
邀请人：何星星
时间：2026年6月12日（星期五）晚上18:30
腾讯会议：554-832-061
报告摘要：本报告围绕“大语言模型在自动定理证明中的应用”展开，重点讨论从形式化数学证明到代码验证的技术演进与方法迁移。报告首先介绍形式化定理证明、Lean 证明助手以及自动化证明的基本背景，说明机器可检查证明在数学、软件可靠性和 AI 推理评测中的重要意义。随后，报告梳理了 LLM for ATP 的发展路线：从符号化 hammer、前提检索、逐步证明生成，到完整证明生成与高层证明规划，展示大语言模型如何逐步改变形式化证明的自动化范式。
在此基础上，报告进一步讨论形式化数学与代码验证之间的联系与差异，并探索如何将 LLM 的推理、规划和反馈修正能力用于程序正确性证明。报告提出以“问题分解”和“证明补全”为核心的代码验证框架， 将复杂验证目标拆解为更易处理的子任务，再结合 Lean 的形式化检查机制完成可靠证明，从而为 LLM 驱动的软件验证提供一种可扩展的研究方向。
主讲人简介：李泽南目前在苏黎世联邦理工学院计算机科学系从事博士后研究，合作导师为 Zhendong Su 教授。李泽南的研究方向集中在神经符号人工智能、定理证明、数学推理和形式化验证。他本科就读于茄子视频
数学与应用数学专业，2017 年毕业后进入南京大学继续深造，先后获得软件工程硕士学位和计算机科学博士学位，博士期间师从马晓星教授和吕建教授。博士阶段，他曾在微软亚洲研究院系统研究组实习，由杨凡博士指导。
李泽南的研究兴趣最初围绕深度学习与软件工程展开，包括深度学习模型质量保障、基于深度学习的软件工程自动化。随着大语言模型的发展，他的研究逐渐转向神经符号 AI，重点关注如何结合大语言模型与形式化方法，提升机器在数学推理、自动定理证明和程序验证任务中的高效性和可靠性。
