< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">

形式化证明与大模型：共创可验证的AI数学未来｜量子位直播

林樾 2025-05-27 11:25:24 来源：量子位

本周四晚20:00，一起来聊聊AI数学吧～

林樾发自凹非寺
量子位｜公众号 QbitAI

就在5月，前有DeepSeek Prover V2发布，后有陶哲轩的AI数学直播，还有谷歌最新发布的AlphaEvolve。

大模型“解数学题”的能力已经是衡量AI「智能天花板」的一种方式，正吸引着无数团队争相挑战。

为了更好地评估AI完成数学推理的能力，近期发布的FormalMATH基准测试也备受关注。

现在，AI完成自动定理证明的表现与挑战究竟如何？主流的技术路径是什么？AI完成形式化证明的能力，又将对大模型应用带来怎样的影响？

为了回答这些问题，5月29日20:00，我们与2077AI开源基金会共同邀请到了来自FormalMath、Kimina等项目团队的成员，一同来讨论大语言模型形式化证明前沿探索。

欢迎在量子位视频号预约直播：形式化证明、大模型与AI数学未来

直播嘉宾

付杰，上海人工智能实验室青年科学家，上海创智学院博士导师

李祎哲，浙江大学博士生，数学领域青年研究者

刘明皓，资深算法工程师，2077AI核心发起人、贡献者

刘威杨，香港中文大学博士生导师，助理教授

刘征瀛，月之暗面（Moonshot AI）研究员，Kimina Co-author

王海明，月之暗面（Moonshot AI）研究员，Kimina Co-author

辛华剑，爱丁堡大学博士生，字节跳动Seed实习生

郁昼亮，香港中文大学博士生

* 顺序按首字母音序排列。

本周四晚20:00，一起来聊聊AI数学吧～