DeepSeek開源數(shù)學(xué)大模型，高中、大學(xué)定理證明新SOTA

AIGC動(dòng)態(tài)歡迎閱讀

原標(biāo)題：DeepSeek開源數(shù)學(xué)大模型，高中、大學(xué)定理證明新SOTA
關(guān)鍵字：報(bào)告,定理,模型,策略,研究者
文章來源：機(jī)器之心
內(nèi)容字?jǐn)?shù)：0字

內(nèi)容摘要：

機(jī)器之心報(bào)道
機(jī)器之心編輯部DeepSeek-Prover-V1.5 通過結(jié)合強(qiáng)化學(xué)習(xí)和蒙特卡洛樹搜索，顯著提升了證明生成的效率和準(zhǔn)確性。AI 技術(shù)與數(shù)學(xué)發(fā)現(xiàn)的進(jìn)展，正前所未有地交織在一起。
前段時(shí)間，著名數(shù)學(xué)家陶哲軒在牛津數(shù)學(xué)公開講座中做了主題為「AI 在科學(xué)和數(shù)學(xué)中的潛力」的主題分享。他指出，將 AI 整合到數(shù)學(xué)領(lǐng)域?qū)⑹剐问交C明的編寫速度超過人類證明（人類證明容易出錯(cuò)）。這將成為一個(gè)關(guān)鍵轉(zhuǎn)折點(diǎn)，意味著形式化證明的使用將不僅限于驗(yàn)證現(xiàn)有的證明，還將用于創(chuàng)造新的數(shù)學(xué)知識(shí)。這將通過廣泛的人類數(shù)學(xué)家與 AI 數(shù)學(xué)家之間的協(xié)作來實(shí)現(xiàn)。我們將迎來一個(gè)「大數(shù)學(xué)」時(shí)代！正如陶哲軒所說，將 AI 應(yīng)用于形式化定理證明已經(jīng)成為數(shù)學(xué)家的日常操作。在另一頭，AI 科學(xué)家們也在努力提高 AI 在形式化定理證明中的性能和效率，比如 DeepSeek 剛剛推出的新模型 ——DeepSeek-Prover-V1.5。DeepSeek-Prover-V1.5 是一個(gè) 70 億參數(shù)的開源模型。它通過結(jié)合強(qiáng)化學(xué)習(xí)（基于證明助手反饋的強(qiáng)化學(xué)習(xí)，RLPAF）和蒙特卡洛樹搜索（特別是提出的 RMaxTS 變體），顯著提升了

原文鏈接：DeepSeek開源數(shù)學(xué)大模型，高中、大學(xué)定理證明新SOTA

聯(lián)系作者

文章來源：機(jī)器之心
作者微信：
作者簡介：