CMU清华教LLM练成数学高手，LeanSTaR训练模型边思考边证明，登顶新SOTA

文章预览

   新智元报道   编辑：乔杨 耳朵 【新智元导读】 LLM数学水平不及小学生怎么办？CMU清华团队提出了Lean-STaR训练框架，在语言模型进行推理的每一步中都植入CoT，提升了模型的定理证明能力，成为miniF2F上的新SOTA。 如果想训练LLM证明定理的能力，你会怎么做？ 既然模型可以通过海量语料学会生成文本，那如果我们能喂给它足够数量的形式证明数据，定理证明能力自然水到渠成？ 然而，我们看到的事实是，无论用符号形式还是自然语言，GPT等大模型的推理能力都不如人意。 两句话，让LLM逻辑推理瞬间崩溃！最新「爱丽丝梦游仙境」曝出GPT、Claude等重大缺陷 就像 GPT-4o自信表示13.11比13.8大 一样，AI再聪明却依旧会在简单的算术上犯蠢。 然而，LLM的数学能力弱，不代表自动化的定理证明器对数学没用。 前段时间 刚刚被破解的「忙碌海狸」问题中，4 ………………………………