形式化證明與大模型：共創(chuàng)可驗證的AI數(shù)學未來｜量子位直播
本周四晚20:00，一起來聊聊AI數(shù)學吧～
林樾 發(fā)自 凹非寺
量子位｜公眾號 QbitAI
就在5月，前有DeepSeek Prover V2發(fā)布，后有陶哲軒的AI數(shù)學直播，還有谷歌最新發(fā)布的AlphaEvolve。
大模型“解數(shù)學題”的能力已經(jīng)是衡量AI「智能天花板」的一種方式，正吸引著無數(shù)團隊爭相挑戰(zhàn)。
為了更好地評估AI完成數(shù)學推理的能力，近期發(fā)布的FormalMATH基準測試也備受關注。
現(xiàn)在，AI完成自動定理證明的表現(xiàn)與挑戰(zhàn)究竟如何？主流的技術路徑是什么？AI完成形式化證明的能力，又將對大模型應用帶來怎樣的影響？
為了回答這些問題，5月29日20:00，我們與2077AI開源基金會共同邀請到了來自FormalMath、Kimina等項目團隊的成員，一同來討論大語言模型形式化證明前沿探索。
歡迎在量子位視頻號預約直播：形式化證明、大模型與AI數(shù)學未來
直播嘉賓
付杰，上海人工智能實驗室青年科學家，上海創(chuàng)智學院博士導師
李祎哲，浙江大學博士生，數(shù)學領域青年研究者
劉明皓，資深算法工程師，2077AI核心發(fā)起人、貢獻者
劉威楊，香港中文大學博士生導師，助理教授
劉征瀛，月之暗面（Moonshot AI）研究員，Kimina Co-author
王海明，月之暗面（Moonshot AI）研究員，Kimina Co-author
辛華劍，愛丁堡大學博士生，字節(jié)跳動Seed實習生
郁晝亮，香港中文大學博士生
* 順序按首字母音序排列。
直播議程
學直播預告v2.png)
本周四晚20:00，一起來聊聊AI數(shù)學吧～
版權所有，未經(jīng)授權不得以任何形式轉載及使用，違者必究。
- AI Agent，搞投資?｜量子位AI沙龍2025-08-20
- AI Coding如何重構開發(fā)，模型×IDE×Agent深度對話｜量子位AI沙龍2025-08-02
- 聊聊AI Coding的現(xiàn)狀與未來｜沙龍招募2025-07-22
- Data Agent如何幫助企業(yè)打造懂你的“電子牛馬”？｜數(shù)勢xSelectDB2025-07-22
相關閱讀
