进入2019年，当杨凯峪在ICML发表那篇关于定理证明自动化的论文时，他或许没有想到，从计算机视觉转向AI4Math的决定，正是叩响人工智能进化的另一扇门。

回顾杨凯峪的学术生涯，仿佛他的每次转折都能切中 AI 的时代脉搏，早年在计算机尚未成为热门方向时，因对编程的热爱，毅然从清华大学电机系转入计算机系；然后，又在ImageNet作者团队的实验室专注于计算机视觉研究。随着AI前沿的不断演进，他再次果断转向“深度学习与定理证明”这一交叉创新领域，持续探索技术的边界。

此后，杨凯峪持续深耕“AI for Math”领域，从算法模型、数据集建设到开源生态，亲历并推动了行业的诸多关键进展。在Meta工作期间，他带领团队攻坚形式化数学推理，在他的视野中，AI与数学的碰撞远不止于解题竞赛，而是用形式化数学锻造AI的“思维钢印”——让AI不断在形式化数学领域“习武”，在一次又一次的高难度推理挑战中锤炼自身的逻辑能力。每一次推理都严格验算，督促AI逐步形成“遇事讲逻辑、推理有依据”的思维方式。

随着大模型在数学推理上的潜力日渐凸显，“把数学交给AI，让AI直面数学”正在逐渐成为AI行业不可忽视的命题。或许正如杨凯峪本人所说，这不仅仅是让AI生成解题过程，更意味着在形式化的舞台上考验模型在复杂环境下的推理能力，一旦这种能力逐步成熟，或许将为更多需要“严格推理”的领域打开新的机遇之窗。

在这个访谈中，我们将进一步剖析杨凯峪从“电气→机器学习→计算机视觉→AI4Math”的心路历程，探寻他在Meta内部的研究思考与生态实践，也将在更广阔的视野下探讨：数学之于AI的意义，究竟是工具、是挑战，还是激发下一轮AI范式的核心火种？

01 

学术经历与研究转折

“兴趣是最好的老师，编程兴趣让我完成了学术方向的转折”

李梦佳：能否介绍您的学术经历，以及有哪些关键转折点？

杨凯峪：2011年我开始在清华读电气工程，主要学习电网、输电和配电等内容。这个专业是我高中时在父母建议下选择的，因为那时我对未来的职业方向并没有清晰想法。

在读电气工程专业的前两年，工科本科生都会学习编程课程，例如 C++。通过这些课程，我发现自己对编程非常感兴趣，逐渐把大量课余时间投入到各类编程比赛和活动。过了一两年，我开始思考：既然对编程这么喜欢，为什么还要继续学电气工程？于是很快下定决心，转到计算机系。

回头来看，这是一个非常好的时机。那会儿清华计算机系的转系名额是15人，而报名人数只有16人。相比之后几年报名人数远超名额的情形，当时还没有那么多人意识到计算机会那么火。

在进入计算机系后，我主要的兴趣点是对机器学习的研究。清华的科研氛围很浓，大家都倾向于想办法做点科研。我最初对密码学感兴趣，觉得听起来很酷，但做了一阵子后发现它实际上非常偏数学，跟我想象的不太一样。

图注：杨凯峪居家 coding，猫咪相伴

后来，我学习了 Andrew Ng 在 Coursera 上的“Machine Learning”课程，由此正式接触了机器学习。当时计算机系有几位老师在做机器学习，比如朱军老师。我在他的课题组里做过一段时间研究，虽然没有产出特别亮眼的成果，但因为这个经历，我认识了后来成为我博士导师的邓嘉。他是李飞飞的学生，也是 ImageNet 的第一作者。

当时邓嘉刚去密歇根大学任教，处于事业起步阶段，正需要学生。他每次回清华访问都会顺便面试潜在的学生。我通过和他联系，得到去密歇根大学实验室实习一个暑假的机会，主要研究计算机视觉，这也是他的研究方向。后来我正式成为他的博士生，继续在他的实验室深造。读博第二年，我跟随导师从密歇根来到普林斯顿大学，我在AI4Math方向上的所有博士阶段工作都是在这里完成的。博士期间，我的研究方向也在不断调整，从最早的计算机视觉到后续工作，一路走来经历了不少变化，也收获了很多宝贵经验。

李梦佳：当时在您在邓嘉的实验室研究的具体方向是？

杨凯峪：我当时研究的是“人类姿态估计”。简单讲，就是在给定一张含有人物的图片时，让模型识别并定位人物各个关键部位，比如头的位置、手的位置、腿的位置等等。

李梦佳：您加入 Meta 之后，研究方向有没有发生变化？还是说与您之前的工作是一脉相承的？

图注：杨凯峪早期的两篇计算机视觉论文

杨凯峪：整体而言，我的研究脉络是连贯的。真正的转折发生在博士早期。当时我主攻计算机视觉，做过一两个项目，但进展并不理想，我的第一个项目被顶会连续拒了四五次才勉强接收。反复碰壁后，我们决定换条赛道，尝试把深度学习用到推理任务上。具体做什么？讨论后选择了“深度学习 + 定理证明”。原因有二：一是定理证明的评价机制清晰；二是这是一项相对纯粹、能够直接衡量推理能力的任务。

图注：2019年杨凯峪在ICML上发表论文，研究如何利用机器学习方法自动与证明助手（proof assistant）交互，实现定理证明自动化。

这项工作后来投到ICML，成了我博士期间第二个项目，也是第一个真正发表的项目。相比之下，最初的视觉方向因为屡投屡拒最终不了了之。

从那以后，我的博士后半程基本都在探索“深度学习× 推理”，包括与符号计算的结合。博士后时期，AI + 数学开始升温：一方面大模型的兴起带来了能力与工具；另一方面，Lean等工具在数学家群体中开始小范围流行，他们在用Lean对数学形式化的过程中也贡献了大量可用数据。使用Lean的数学家对机器学习的开放态度让我们迎来“用 AI 做数学”的绝佳窗口。那段时间，我们发表了一篇影响较大的论文（LeanDojo），正是在做博士后时完成的。

图注：杨凯峪等学者构建了一个基于开源LLM的定理证明

地址：https://leandojo.org/

加入Meta 后，我依旧沿着这条路线走。如今我带着一些更资深的合作者，可以并行推动更多项目。

02 

研究方向与领域进展

“AI 辅助数学，最有价值的不只是自动生成证明”

李梦佳：您是如何意识到“AI + 数学”重要性的？最终怎样确定这一方向？

杨凯峪：要从我们最初在定理证明上的项目说起。定理证明会用到一些工具，比如 Lean、Coq、Isabelle，这些被称为“证明助手”或“交互式定理证明器”，其实也是一种特殊的编程语言。这种语言除了能写一般程序，还能用来描述数学命题，以及计算机系统的某些特性。比如，你可以写程序，然后用这种语言规定它必须没有内存错误、没有恶意行为等。简单来说，这是一种既能描述数学问题，也能描述程序验证需求的通用语言。

图注：杨凯峪在智源分享“AI4Math新前沿”  

回放链接：https://event.baai.ac.cn/activities/884

我们最初把这项技术用在程序验证上，主要是证明和计算计算机系统相关的定理。那时候用的是比较早期的RNN模型，因为还没有现在的大语言模型。后来我做博士后时，随着大语言模型出现、数学领域的数据也变多了，我们就逐渐转向了数学方向。

其实原理差不多，只是模型用的数据不同。当下我们主要关注数学，一是因为数学问题更纯粹、好界定；二是现在很多大模型团队（比如OpenAI）也把数学当作检验复杂推理能力的重要任务。如果模型能在数学上表现好，说明它的推理能力很强。

李梦佳：目前 AI for Math 领域最核心需要解决的问题有哪些？

杨凯峪：从宏观角度来看，有一个值得思考的问题：究竟是“AI for Math”，还是 “Math for AI”？虽然大家普遍更喜欢用 “AI for Math” 这个说法，强调我们是用 AI 作为工具来帮助数学家，但我认为，这其实只是这个领域的一部分。

当前许多工作试图通过AI自动证明定理来辅助数学家。这有点像用图像生成 AI 去辅助艺术家你说“你不用自己画画了，我可以用AI帮你画出来”，但很多艺术家可能并不买账，因为他们更看重自己的创作过程。其实，很多数学家的想法也是类似的。所以，如果说 AI 要帮助数学家，我们更需要思考数学家真正的需求是什么。以 Lean 社区为例，很多数学家反馈说，他们不是单纯需要一个自动生成证明的工具，而是希望 AI 能帮他们推荐、检索相关文献，从中找到对当前证明有启发或帮助的信息。像这样基于辅助性的功能，反而对数学家更有价值。

图注：Lean 社区主页。

从另一个角度来说，我个人其实更关心一个可以称为“Math for AI” 的方向。也就是说，我们可以把数学作为一个很好的问题域，来研究许多对 AI 极其重要的问题，比如 AI 如何分析和处理大规模信息，如何在庞大的空间里进行推理等。最终的目标其实未必只是让 AI 在数学领域表现得更好，而是希望这些研究能够推动 AI 在更广泛、更实际的应用场景中发挥作用。

图注：杨凯峪发表论文《形式化数学推理：AI的新前沿》，主张形式化数学推理是AI4Math（AI for Mathematics）的重要突破口。

论文地址：https://arxiv.org/pdf/2412.16075

李梦佳：当前大模型在推理任务中展现了一定能力，请问您的研究如何与大模型技术结合？具体在模型推理层面有哪些应用？

杨凯峪：虽然我的核心研究方向是形式化数学（Formal Math），但大语言模型在我们的工作中扮演着关键角色。现在相关工作的主要思路是：先用大语言模型学习 Lean 等形式化语言的语法与用法→再利用学到的知识去生成证明或程序。

如果没有大模型支持（比如我最早用 RNN 做第一个项目时）光让模型生成一段“语法正确”的证明就已经非常困难，更别说保证其有用或正确了。而在大语言模型出现后，语法正确几乎成了“默认配置”，我们终于可以把注意力放在“生成的证明是否有效、是否正确”这些更本质的问题上。因此，无论是我个人的研究，还是我们团队项目，大语言模型都是不可或缺的。

李梦佳：在您看来，当前这个领域最值得关注的进展有哪些？

杨凯峪：我把最近的重要进展分成两类：

1.非形式化（informal math）方向。DeepSeek 的最新工作给数学推理能力带来了显著提升，方法既优雅又系统，更像一篇真正的推理论文，而不仅是技术报告。

2.形式化（formal math）方向。Numina项目获得 AIMO Progress Prize 一等奖。这是一个非营利团队，他们大规模收集数学题、解答及证明过程，并尝试把这些数据转成 Lean 等形式化语言。它解决了开源社区长期缺乏高质量形式化数据的痛点，因为过去大量数据都掌握在几家私有公司手里。

图注：AIMO Progress Prize主页

03

行业生态与开源理念

“几年前，很多公司都能公开发表论文，但最近一两年大家普遍开始收紧。”

李梦佳：海外的研究圈子对 DeepSeek是如何评价的？

杨凯峪：在海外的研究圈子里，对 DeepSeek 的评价非常高。因为在此之前，具备相当或类似能力的模型基本上都掌握在少数几家公司手里。这些公司大多是私营企业，对外披露的细节非常有限。但随着 DeepSeek 的相关论文（包括 V3、R1 等）发布后，美国乃至全球范围内的许多研究机构，甚至一些高校实验室，都通过阅读这些论文来了解大型语言模型的训练过程。这些知识最初只是极少数美国公司私有的，现在 DeepSeek 公开了，这无疑具有非常重要的意义。

李梦佳：谈到开源，我们知道 Meta 也在积极开源一些 AI 工具。您怎么看待开源生态对 AI 行业发展的影响？

图注：Meta 开源的Llama系列大模型节选

杨凯峪：开源生态不仅对 AI，而且对整个计算机科学领域都至关重要。正因为有了开源，计算机科学的研究才能如此快速地推进。比如，昨天有人开源了一个代码库，我今天就能立刻尝试运行，并在这个基础上加入自己的想法，看能否做出更好的成果。

在其他研究领域（如生物、化学），这种现象就比较少见。不同研究小组往往拥有私有数据，互不共享，想要获得它们的数据非常困难。而对于计算机科学社区来说，这种开源文化尤为重要。不过，近几年由于多种原因（比如各大公司之间的竞争、大模型本身需要海量资源），导致越来越多的前沿模型开始闭源。显然，这种闭源倾向实际上在一定程度上阻碍了学术研究和技术创新。

李梦佳：说到您加入 Meta，当时相比于谷歌 AI 等公司的选择，是什么原因让您更偏向 Meta 呢？您认为：Meta 的研究侧重点与谷歌 AI 等相比，有哪些不同？

杨凯峪：如果把 Meta 旗下的 FAIR（Facebook AI Research）和 OpenAI、Google 等其他美国大型科技公司的研究实验室相比，我个人更喜欢 FAIR 。首先，这里可以对研究成果公开发表论文。几年前，很多公司（比如 DeepMind，甚至一度包括 OpenAI）都能公开发表论文，但最近一两年大家普遍开始收紧。尤其是 Google DeepMind 与 Google Brain 合并后，如果你的研究和他们的核心业务（Gemini）相关，想发表就会比较困难。不过在FAIR,至少目前为止，主要的研究工作都是可以被发表的。

图注：2023年谷歌 CEO Sundar Pichai发给谷歌员工的内部信表示：Google DeepMind 新团队汇集Google Research 的 Brain 团队和 DeepMind

我本人很乐意让自己做的研究被更多人看到，希望能给外部世界带来一些价值，也期待各方的评价——不管是积极还是消极——因为从这些反馈中也能有所收获。

其次，FAIR 除了支持论文发表，还鼓励开源代码，这和公开发表论文的理念相似。再者，FAIR 对研究课题的选择方式相对自下而上。与一些组织自上而下地提出几个大方向、大项目并让成员分头贡献不同，在 FAIR，研究科学家和研究工程师之间的合作相对更“有机”。比如，我们在闲聊中碰到一个想法，如果大家都觉得有意义和兴趣，就能自然地组队合作。即使彼此不在同一个团队，也不存在上下级关系，只要我们对同一个问题感兴趣，就能一起去做，然后把成果展示出来，也会得到认可。我个人非常喜欢这种合作模式。

李梦佳：你所在的团队的整体研究机制是怎样的？

杨凯峪：其实这和我们刚才谈到的工作模式是同一个问题的两个方面。好处在于：我们每个人可以自由决定自己要做什么，不必被迫参加大型项目。坏处则是：你很难去说服别人和你一起合作，或者来帮你做具体的工作。因为大家都是独立的研究员，如果你需要对方的帮助，就得花很多精力去说服他，而对方是否有足够的时间和精力来参与，也要看他自己正在做的项目安排。

目前的情况是，在我所在的团队中，至少对于全职研究人员而言，大家做研究都比较独立。比如，我可能每年会招一位实习生（intern），或者偶尔会有一些合作项目，比如和 NYU（纽约大学）的研究生一起合作。但除了这些情况，我们并没有一个大规模、紧密协作的团队结构，更多是各自独立进行研究。

04 

未来展望与对青年建议

“如果我们常为研究项目会被别人抢先而焦虑，其实反应了更深层的问题：我们做的研究是否真的有意义？”

李梦佳：您当前的研究规划是怎样的？打算在哪些领域继续深入，或者在新领域做探索？

杨凯峪：从中期乃至更长远的角度来说，我的研究计划主要还是围绕“AI 如何解决数学问题”这个主题，以及由此衍生的若干相邻方向。我现在特别感兴趣的有以下几点：

1.AI 的假设生成（Conjecturing）。目前大多数研究都是“给 AI 一条定理，然后让 AI 去证明”。但我希望 AI 能够自己提出一些定理假设，这就包含两方面：一方面是尝试去证明这些定理；另一方面是寻找反例，验证定理的有效性。通过不断地提出并验证假设，AI 就可以在庞大的数学知识体系中进行自主探索。

2.形式化数学与其他领域的交互。比如，AI for Math（特别是形式化数学）、代码生成、程序验证和自然语言推理之间有很多相似和交叉的地方。随着代码生成工具变得越来越强，未来大部分代码可能都会由AI生成。但这样一来，我们就很难逐行检查这些代码是否正确。所以，需要AI模型在生成代码的同时，自己进行某种推理，确保代码的功能和正确性。这些推理或验证的方法，其实和我们在形式化数学中用的工具很像。

李梦佳：AI 在数学上的应用似乎还不如 AI 用于文本或图像生成那样直观、见效快。那么，AI 在形式化推理或者定理证明上的能力，今后可能应用到哪些领域呢？

杨凯峪：我觉得凡是需要“严格推理”的场景，都可以。现在很多非形式化的数学解题方式都面临一个问题：如果题目最终只要求算出一个数，就可以验证答案对不对，却没法验证中间推理是否正确。如果是证明题，这个问题就更显著。我们肯定希望 AI 做到“可靠且严格”的推理，而一个非常重要的方法就是把推理落实到某种形式化语言里。因此我们认为，未来 AI 在所有需要推理的任务中，形式化系统可能都有很大的潜力和前景。

很多实际场景中都有数学成分。举个例子：我们订机票或者酒店等行程时，其实可以把这个过程“数学化”，把它抽象为一个满足各种约束条件的问题。只要涉及到机票、酒店、行程之间不冲突等等，这些约束都需要被满足。这其实就是一个“约束优化”或“约束满足”的问题。

图注：杨凯峪候机间隙，柴犬作陪

其实，人类处理这类问题时，本质上也是在进行数学抽象。虽然我们不总是把它写成公式，但脑中一定有对应的抽象概念。理想情况下，我们希望AI能像人一样理解数学，从现实问题中识别出需要推理的部分，提取出其中的数学内容，并用数学思维去解决。这种能力将来会非常有用。

李梦佳：您对同行或者更年轻的研究者有什么建议吗？比如如何做好研究、怎么选择适合自己的研究方向等？

杨凯峪：要分不同阶段来看，对于还在读博的同学，我最重要的建议是：多和其他研究者进行交流。说实话，这是我读博期间的一大教训。博二到博四那段时间，我几乎每天都在家写代码，做自己的研究，而没怎么去外面开会或和其他研究者交流、合作。后来回头看，我发现那段时间虽然高效率地完成了不少项目，但是其实有些项目并不是朝着能产生最大学术影响力的方向。

举例来说，我曾经有个项目，自己觉得很漂亮、很满意，但事后才发现它的前景并不像我想象的那么广阔。如果当时多跟其他研究者交流，就可能更早地认识到这点，从而及时对研究方向做出调整。

第二点也与此相关：项目的选择很重要。我们都知道，现在很多学生，无论是本科生还是博士生，都在承受论文“通货膨胀”的压力，为了进入理想的博士项目或者工作岗位而大量发表论文。可如果你去看那些最终能在美国顶尖院校拿到教职，或者在一流工业研究机构找到职位的人，他们并不是论文最多的，而是拥有一两篇真正产生重大影响的工作。也就是说，找到重要的方向并做出有重要意义的研究，往往比做三四个普通项目更有价值。因此，如何选择项目，可能需要你投入更多的思考和精力。要分辨清楚哪些方向值得深耕，避免在缺乏长远价值的项目上投入过多时间。这样的选择往往比你想象中更关键。

李梦佳：如果在外面交流时说了自己的想法，别人要是拿去做了，会不会变成竞争对手？

杨凯峪：确实有这种可能，热门领域更要谨慎。不过，大多数在头脑风暴中的随机想法，在被验证之前价值有限，难的是把想法做出来。真正有价值的是实践中遇到的细节和关键发现，这些别人很难靠听你讲就复制。

比如我做过一个项目，思路很普通，别人也做过类似的，但我们在实践中发现并解决了关键问题。如果我们常为研究项目会被别人抢先而焦虑，其实反应了更深层的问题：我们做的研究是否真的有意义？如果一个项目，即使我们不去做，短期内也会被其他团队以十分类似的方法做出来，那它额外的社会价值就有限。我更希望能够通过自己的研究来为整个领域带来一点有个人色彩的独特见解，这种工作“撞车”的风险自然低。

其实不必过度强调 “保密”，开放交流才是根本。补充一点，不是说想法不重要，而是真正有价值的想法往往不是 “想” 出来的，而是在 “做” 的过程中经反复打磨、验证、修改才成型的，常需大量投入。这个过程积累的经验和深度理解，很难通过对话就被窃取复制。就像现在大语言模型原理不是秘密，但并非所有公司都能轻易训练出好模型——这就是实践壁垒。