草莓与AlphaProof：GOFAI*拯救生成式人工智能！

在你错过的情况下...为了前进，人工智能研究正认识到大型语言模型（LLMs）的局限性，并正在与老式符号推理进行混合。

山姆·奥特曼关于OpenAI的草莓项目的诱人暗示[1]，很可能会成为GPT-5，显示了前沿人工智能研究正朝着符号推理的方向发展。让我们希望草莓项目可以准确计算其名称中的R的数量[2]。

对于仍然怀疑、被拟人化和ELIZA效应蒙蔽的人，这是对大型语言模型（LLM）方法在推理方面的局限性的承认。这是许多人，如Yann LeCun，François Chollet和我自己，自ChatGPT首个生成式聊天机器人发布以来一直不知疲倦地重复的事情。

以前被代号Q*（Q星）[6]所熟知，草莓项目预计将提供自主互联网研究（已包含在SearchGPT[7]中）并“相当大幅度”地改善GPT模型的数学推理能力。它被提出作为OpenAI努力创建人工通用智能（AGI）的一部分 — — 一种具有类似人类大脑能力的人工智能。

我期待ChatGPT推理能力的提升，特别是在掌握数学语言方面，这是由于生成示例（合成数据）以弥补数学训练数据不足而产生的。

在这方面，它将是一个大型语言模型（LLM）和一个定理证明器类型的符号推理系统的结合，采用与Deepmind的AlphaProof和AlphaGeometry相同的方法。

在AlphaProof中，DeepMind使用了一个大型语言模型（LLM）和一个定理证明器，重新演绎了旧经典的AI元算法“生成和测试”，但增加了一个“训练”步骤，该步骤使用定理证明器验证的解决方案来对LLM进行微调（见上图）。

候选解决方案形式的数据生成是由LLM执行的。由于生成的解决方案可能不正确或不完整，外部测试者（或验证者），实际上是基于符号逻辑的定理证明器，验证LLM提出的解决方案。验证者还可以在必要时纠正或完善解决方案。最后，经过校正的解决方案通过低秩适应（LoRA）用于训练LLM，避免重新训练整个预训练模型。

在AlphaProof中，使用了两个LLM。首先，一个形式化LLM将自然语言问题描述转换为形式化的数学语言。然后第二个LLM作为解决方案生成器。这些解决方案然后由基于符号逻辑的定理证明器验证。经过校正和完善的证明被用作训练解决方案生成器LLM的数据。

在同一思路下，其他有前途的方法有神经符号人工智能和生成流网络（GFlowNets）。

总的来说，为了取得进展，人工智能研究正在认识到基于深度学习的大语言模型（LLM）存在局限性，并主张与好老式的符号推理相结合。

笔记和参考资料:

*GOFAI：传统人工智能

《OpenAI的草莓项目将成为ChatGPT-5，即将推出，并且据知情人士称，它在数学方面将比任何聊天机器人更优秀》— techradar — 2024年8月28日。
直到最近，简单的查询“草莓这个词中有几个R？”返回的结果是错误的。
"李宇春：元AI，开源，LLM的极限，AGI和人工智能的未来" — 利克斯弗里德曼播客#416 — 2024年3月7日。
« 弗朗索瓦·肖勒 - LLMs不会导致AGI - $ 1,000,000奖金找到真正的解决方案» - Dwarkesh Patel的YouTube频道 - 2024年6月11日。»
「ChatGPT，谨慎的热情是必须的…」— 克劳德·库洛姆（Claude Coulombe）在2022年12月7日发布在LinkedIn上。
这些线索暗示了OpenAI神秘的Q*项目的真实性质 —《连线杂志》—2024年11月30日。
可能只是通过将搜索结果添加到生成对话机器人的推断上下文中来实现。
« 人工智能达到国际数学奥林匹克竞赛问题的银牌水平 » — DeepMind 博客 — 2024年7月25日。