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

原標(biāo)題：CMU清華教LLM練成數(shù)學(xué)高手，LeanSTaR訓(xùn)練模型邊思考邊證明，登頂新SOTA
關(guān)鍵字：模型,定理,數(shù)據(jù),思維,策略
文章來源：新智元
內(nèi)容字?jǐn)?shù)：0字

內(nèi)容摘要：

新智元報(bào)道編輯：喬楊 耳朵
【新智元導(dǎo)讀】LLM數(shù)學(xué)水平不及小學(xué)生怎么辦？CMU清華團(tuán)隊(duì)提出了Lean-STaR訓(xùn)練框架，在語言模型進(jìn)行推理的每一步中都植入CoT，提升了模型的定理證明能力，成為miniF2F上的新SOTA。如果想訓(xùn)練LLM證明定理的能力，你會(huì)怎么做？
既然模型可以通過海量語料學(xué)會(huì)生成文本，那如果我們能喂給它足夠數(shù)量的形式證明數(shù)據(jù)，定理證明能力自然水到渠成？
然而，我們看到的事實(shí)是，無論用符號形式還是自然語言，GPT等大模型的推理能力都不如人意。
兩句話，讓LLM邏輯推理瞬間崩潰！最新「愛麗絲夢游仙境」曝出GPT、Claude等重大缺陷
就像GPT-4o自信表示13.11比13.8大一樣，AI再聰明卻依舊會(huì)在簡單的算術(shù)上犯蠢。
然而，LLM的數(shù)學(xué)能力弱，不代表自動(dòng)化的定理證明器對數(shù)學(xué)沒用。
前段時(shí)間剛剛被的「忙碌海貍」問題中，4萬行Coq代碼功不可沒。
陶哲軒也曾在采訪中強(qiáng)調(diào)，使用Lean等自動(dòng)化工具可以徹底顛覆數(shù)學(xué)家們的工作方式。這是一股不可小覷的力量。
最近，CMU和清華的一項(xiàng)研究就致力于讓LLM的「自然語言思維鏈」和Lean的形式化證明結(jié)合在一起。
論文地址

原文鏈接：CMU清華教LLM練成數(shù)學(xué)高手，LeanSTaR訓(xùn)練模型邊思考邊證明，登頂新SOTA

聯(lián)系作者

文章來源：新智元
作者微信：
作者簡介：