CMU清華教LLM練成數學高手，LeanSTaR訓練模型邊思考邊證明，登頂新SOTA

AIGC動態歡迎閱讀

原標題：CMU清華教LLM練成數學高手，LeanSTaR訓練模型邊思考邊證明，登頂新SOTA
關鍵字：模型,定理,數據,思維,策略
文章來源：新智元
內容字數：0字

內容摘要：

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

原文鏈接：CMU清華教LLM練成數學高手，LeanSTaR訓練模型邊思考邊證明，登頂新SOTA