SLAI seminar

11月16日（星期日）上午，来自北京大学的董彬教授受深圳河套学院邀请，在B411阶梯教室举办学术报告讲座。本次讲座由王本友教授主持，董彬教授以“AI for Mathematics: From Digitization to Intelligentization”为主题，深入探讨了人工智能如何解决数学研究中的效率瓶颈问题。

董彬 教授

· 北京大学博雅特聘教授

· 北京大学国际数学研究中心教授

· 北京大学国际机器学习研究中心副主任

· 北京中关村学院常务副院长

· 北京大学长沙计算与数字经济研究院副院长

讲座简介

数学研究长期面临验证繁琐与语义检索困难的效率瓶颈。本次报告中，董彬教授分析了专用模型与通用大模型在数学探索中的优劣，指出“形式化”是将自然语言数学转化为可验证代码、提升AI推理能力的关键途径。他分享了团队在自动形式化、Lean Search检索引擎及代数评测基准（FATE）构建方面的进展，并展望了AI通过分担机械性工作，让人类回归数学“理解”本质的愿景。

讲座内容

在人工智能深度赋能基础科学的浪潮下，董彬教授详细分析了数学研究中长期存在的“效率瓶颈”，并提出通过“数字化”（形式化）连接自然语言数学与机器推理的进阶路径，旨在培养AI成为数学家的智能学徒。

讲座重点剖析了传统数学研究模式的核心挑战。首先是自然语言表述的模糊性与验证难题。非形式化语言容易掩盖证明过程中的细微错误，即便是顶尖数学家如Andrew Wiles在证明费马大定理初期也未能幸免。其次是语义检索困境，复杂的数学定义使得字面搜索难以精准定位已有成果，导致研究者难以有效“站在巨人的肩膀上”，重复造轮子现象普遍。

针对这些痛点，董彬教授比较了当前AI的两大范式。专用模型虽能在纽结理论等领域提供直觉，将“大海捞针”简化为“鱼缸捞针”，但通用性不足；通用模型泛化能力强，但在处理严谨数学时存在推理幻觉和不稳定性。

对此，团队提出了以“形式化”为核心的数字化方案。通过将模糊的自然语言转化为计算机可编译、可验证的形式化语言，不仅实现了绝对正确的验证，更为AI训练提供了精准的反馈信号，从而解决了大模型逻辑推理的可信度问题。

基于该理念，团队取得多项成果：开发了Lean Search检索引擎，解决了形式化过程中寻找前置定理的痛点；提出了基于依赖图分解的自动形式化方法，有效提升了复杂定理的转化效率；并构建了涵盖本科至专家级难度的FATE评测基准。最后，董彬教授引用Bill Thurston的观点，强调数学核心在于理解而非单纯证明，展望AI未来将接管机械性工作，释放人类精力以追求宏观洞察。

在交流环节，与会师生就多模态模型在几何推理中的短板、形式化方法在密码学中的应用边界，以及强化学习奖励机制设计等前沿问题与董彬教授进行了深入探讨。