形式化證明與大模型:共創可驗證的AI數學未來|量子位直播
本周四晚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數學吧~
版權所有,未經授權不得以任何形式轉載及使用,違者必究。
- 嘉賓全陣容揭曉!張亞勤孫茂松,百度小米商湯谷歌都要來MEET20262025-12-04
- 下周三!量子位的這件大事就要來了|MEET20262025-12-04
- 第三波嘉賓來襲!等你一起MEET2026,速戳報名2025-11-28
- 搶先報名!第二波嘉賓亮相,百度京東高通亞馬遜都來了|MEET20262025-11-20




