目前，大模型被越来越多地运用在逻辑推理和数学证明当中。但是，它们在推理方面的能力仍不能尽如人意。
要想实现目前顶尖大模型所表现出的数学推理和数学证明水平，大模型需要使用 3000 亿 token 的数据来做训练。但是，其所展现出来的能力，远远不如经过更小数据训练的人类。
造成这一现象的原因之一是：人类所使用的训练数据和大模型所使用的训练数据，表面上看是一致的（比如课本、论文等），但是实际上是不一致的。
人类在使用课本学习的时候，会在脑海中进行试错和纠正。这一试错和纠正的训练数据，基本没有被囊括在大模型的训练数据中。几乎所有的课本和论文内容都只包含定理正确的证明，不包含试错和纠错信息。
当人类做推理和数学证明任务时，这种试错和纠正的能力至关重要。而大模型的训练数据中显然缺乏帮助其学会是错和纠错能力的信息。这一观点同样被著名数学家、菲尔兹奖得主陶哲轩认同[1]。
一个自然而然的猜想是：如果大模型训练数据中包含了试错信息和纠正信息，那么大模型的表现会更好。
为了证明这一猜想，美国加州圣地亚哥分校（UCSD，University of California，San Diego）数学系博士生 Chenyang An 及其在 UCSD 和美国卡耐基梅隆大学的合作者们开展了一项研究。
图 | Chenyang An（来源：Chenyang An）
要想完成本次研究，必须首先获得试错信息和纠正信息。但是，目前数学证明的公开数据库中，并不包含试错信息和纠正信息。
为此，他们选择在直觉主义命题逻辑体系中，制造自造证明数据和证明中的试错数据来供大模型训练。
对于本次论文 OpenReview 的审稿人认为：将错误的搜索路径暴露给大模型，并指导其如何纠正有着重要意义。
因为，大模型在实际推理过程中会经常犯错。目前，针对大模型在推理过程中犯错的通用解决办法是，使用外在的机制去撤回大模型的错误推理，从而返回到之前的推理步骤。
而该团队的办法有助于让大模型学会识别错误路径，以及学会如何纠正错误路径，从而提高推理的正确性。
（来源：ACL 2024）
Chenyang An 补充称：“我们这次成果是一个大项目中的一部分。这个大项目始于这样一个假设：目前大模型在推理任务和数学证明任务上表现不佳的本质原因，是由于训练数据中没有包含帮助大模型学会识别错误和纠正错误的信息。”
因此，这个大项目旨在从各个角度，挖掘出推理数据和证明数据中的所有试错信息和纠错信息，并将大模型训练在其之上。
如果这个假设是正确的，倘若我们能够获得大量的试错纠错数据，在未来的 1-3 年内就能看到大模型推理能力的大幅上升。
“我个人对此是乐观的。当然，另一种可能是大模型的推理能力受限于其目前的架构和训练方法，而非训练数据。”Chenyang An 说。
日前，相关论文以《从失败中学习：用试错-纠错数据对大模型进行微调以证明直觉主义命题逻辑定理》（Learn from Failure：Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving）为题发在 2024 年国际计算语言学年会（ACL，Annual Meeting of the Association for Computational Linguistics ）[2]。
图 | 相关论文（来源： 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
排版：刘雅坤
01/ 浙大校友将Cas9基因编辑效率提升百倍，打造基因编辑通用型改造策略，助力治疗基因疾病
02/ 中科大团队打造摩擦静电镊，提出新型液滴操控技术，可用于操作细胞液体和太空实验
03/ 助力解决自动驾驶商用难题：科学家提出等效加速测试方法，提升仿真与实车测试速度1000倍
04/ 复旦与上科大团队基于超导视网膜打造新型红外探测器，有望用于AI机器视觉和加密通讯
05/ 为30年待解之谜画上句号：科学家用哈伯德模型研究铜氧化物超导性，助力揭示高温超导本质