形式化證明與大模型：共創(chuàng)可驗(yàn)證的AI數(shù)學(xué)未來｜量子位直播
本周四晚20:00，一起來聊聊AI數(shù)學(xué)吧～
林樾 發(fā)自 凹非寺
量子位｜公眾號(hào) QbitAI
就在5月，前有DeepSeek Prover V2發(fā)布，后有陶哲軒的AI數(shù)學(xué)直播，還有谷歌最新發(fā)布的AlphaEvolve。
大模型“解數(shù)學(xué)題”的能力已經(jīng)是衡量AI「智能天花板」的一種方式，正吸引著無數(shù)團(tuán)隊(duì)爭(zhēng)相挑戰(zhàn)。
為了更好地評(píng)估AI完成數(shù)學(xué)推理的能力，近期發(fā)布的FormalMATH基準(zhǔn)測(cè)試也備受關(guān)注。
現(xiàn)在，AI完成自動(dòng)定理證明的表現(xiàn)與挑戰(zhàn)究竟如何？主流的技術(shù)路徑是什么？AI完成形式化證明的能力，又將對(duì)大模型應(yīng)用帶來怎樣的影響？
為了回答這些問題，5月29日20:00，我們與2077AI開源基金會(huì)共同邀請(qǐng)到了來自FormalMath、Kimina等項(xiàng)目團(tuán)隊(duì)的成員，一同來討論大語言模型形式化證明前沿探索。
歡迎在量子位視頻號(hào)預(yù)約直播：形式化證明、大模型與AI數(shù)學(xué)未來
直播嘉賓
付杰，上海人工智能實(shí)驗(yàn)室青年科學(xué)家，上海創(chuàng)智學(xué)院博士導(dǎo)師
李祎哲，浙江大學(xué)博士生，數(shù)學(xué)領(lǐng)域青年研究者
劉明皓，資深算法工程師，2077AI核心發(fā)起人、貢獻(xiàn)者
劉威楊，香港中文大學(xué)博士生導(dǎo)師，助理教授
劉征瀛，月之暗面（Moonshot AI）研究員，Kimina Co-author
王海明，月之暗面（Moonshot AI）研究員，Kimina Co-author
辛華劍，愛丁堡大學(xué)博士生，字節(jié)跳動(dòng)Seed實(shí)習(xí)生
郁晝亮，香港中文大學(xué)博士生
* 順序按首字母音序排列。
直播議程
學(xué)直播預(yù)告v2.png)
本周四晚20:00，一起來聊聊AI數(shù)學(xué)吧～
- AI Agent，搞投資?｜量子位AI沙龍2025-08-20
- AI Coding如何重構(gòu)開發(fā)，模型×IDE×Agent深度對(duì)話｜量子位AI沙龍2025-08-02
- 聊聊AI Coding的現(xiàn)狀與未來｜沙龍招募2025-07-22
- Data Agent如何幫助企業(yè)打造懂你的“電子牛馬”？｜數(shù)勢(shì)xSelectDB2025-07-22
相關(guān)閱讀
AI七個(gè)月突破數(shù)學(xué)家“圍剿”反超人類！14位數(shù)學(xué)家深挖原始推理token：不靠死記硬背靠直覺
也有局限性：缺乏創(chuàng)造力和理解深度
天津大學(xué)火速解聘學(xué)術(shù)不端教授！退學(xué)研究生123頁P(yáng)DF實(shí)名舉報(bào)，控訴利用職權(quán)為女兒留學(xué)鋪路
大量數(shù)據(jù)造假、圖片PS
