加州大学团队用“错误搜索路径及纠错数据”训练大模型，以提高其推理能力

来源：DeepTech深科技

目前，大模型被越来越多地运用在逻辑推理和数学证明当中。但是，它们在推理方面的能力仍不能尽如人意。

要想实现目前顶尖大模型所表现出的数学推理和数学证明水平，大模型需要使用 3000 亿 token 的数据来做训练。但是，其所展现出来的能力，远远不如经过更小数据训练的人类。

造成这一现象的原因之一是：人类所使用的训练数据和大模型所使用的训练数据，表面上看是一致的（比如课本、论文等），但是实际上是不一致的。

人类在使用课本学习的时候，会在脑海中进行试错和纠正。这一试错和纠正的训练数据，基本没有被囊括在大模型的训练数据中。几乎所有的课本和论文内容都只包含定理正确的证明，不包含试错和纠错信息。

当人类做推理和数学证明任务时，这种试错和纠正的能力至关重要。而大模型的训练数据中显然缺乏帮助其学会是错和纠错能力的信息。这一观点同样被著名数学家、菲尔兹奖得主陶哲轩认同[1]。

一个自然而然的猜想是：如果大模型训练数据中包含了试错信息和纠正信息，那么大模型的表现会更好。

为了证明这一猜想，美国加州圣地亚哥分校（UCSD，University of California，San Diego）数学系博士生 Chenyang An 及其在 UCSD 和美国卡耐基梅隆大学的合作者们开展了一项研究。

图 | Chenyang An（来源：Chenyang An）

要想完成本次研究，必须首先获得试错信息和纠正信息。但是，目前数学证明的公开数据库中，并不包含试错信息和纠正信息。

为此，他们选择在直觉主义命题逻辑体系中，制造自造证明数据和证明中的试错数据来供大模型训练。

对于本次论文 OpenReview 的审稿人认为：将错误的搜索路径暴露给大模型，并指导其如何纠正有着重要意义。

因为，大模型在实际推理过程中会经常犯错。目前，针对大模型在推理过程中犯错的通用解决办法是，使用外在的机制去撤回大模型的错误推理，从而返回到之前的推理步骤。 

而该团队的办法有助于让大模型学会识别错误路径，以及学会如何纠正错误路径，从而提高推理的正确性。

（来源：ACL 2024）

Chenyang An 表示，大模型正在帮助学者们更快地掌握不同领域的知识。例如，他说自己之前的博士研究方向是数学物理，和计算机没有直接关系。

“编程、Linux 等方面经验也是几乎为零。我能在比较短的时间内做好实验设计和完成实验验证，很大一部分程度上归功于 GPT-4。”其表示。在研究期间，诸如 Copilot 这样的编程工具也变得更加好用。

Chenyang An 认为，诸如 Lean 这样的形式化验证系统，将为数学界的合作带来全新的可能。

从此可以相信，一段由陌生人发现的经过形式化系统验证过的证明是正确的（即使这段证明没有发表在任何期刊上，没有经过同行评议），从而能在他人的工作基础上进行新的研究。

而在另一方面，随着自动形式化（autoformalization）研究领域的发展，越来越多的由自然语言描述的证明将会快速地被形式化语言化，从而为进一步提高大模型的训练数据质量提供基础。

最终，数学证明生成任务可能将成为代码生成任务（code-generation）的分支。

谈到计算机程序与数学证明之间的关系时，Chenyang An 表示有一条定理指出：数学证明和计算机程序是等价的。

“从这个角度来讲，数学证明的研究和发现，在几十年中一直是计算机领域的细分研究方向。

而大模型提供了一件研究数学定理自动证明的强大武器。又或许以后数学证明的发现，将取决于算力和训练，而非人类的灵光一闪。”Chenyang  An 说道。

而在后续，他和所在团队将研究能否通过改变现有推理训练数据的范式，从而提高大模型在推理训练数据上的训练效率，以及加深人们对于大模型推理能力的理解。

此外，他还表示：“我对 AI 最终能否造福人类这一问题持审慎态度。”

其认为，AI 在人类社会生产活动中所占的比重势必会影响到人在其所占的比重，带来的效应之一就是人类劳动所产生的相对价值将进一步减小。

就目前的情况看，以大模型为基础的 AI 创新并不会推动社会分配的公平进程，因为大模型的训练成本过高，导致只有大公司才能拥有。

另一方面，通过使用 AI 工具，负责任的和不负责任的机构都将获得前所未有的能力。因此，对未来的盲目乐观是绝不可取的。

Chenyang An 认为，倘若 AI 真的能解决数学难题，进行有效的推理和研究，人类需要重新对自身进行价值定位。智力资源在人类社会中将变得不再稀缺。这是好事，也是坏事。

Chenyang An 最后表示，有对本次技术感兴趣的伙伴，欢迎邮件联系进行讨论 c5an@ucsd.edu。

参考资料：

1.https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/

2.https://arxiv.org/pdf/2404.07382

排版：刘雅坤