原贴链接

众所周知，大型语言模型（LLM）在演绎推理方面表现不佳。是否有任何通用的推理引擎可用（即不仅限于数学等特定领域）。

我想知道是否已经存在这样的系统，它具有一套映射好的推理规则，并且预先加载了通用数据，你可以输入额外的数据进行查询。

这样的系统能够解决三段论，并应用命题逻辑和谓词逻辑：

我有一盘土豆。以下陈述为真： 我的土豆中，没有一个是新的并且被煮过的。 这盘中的所有土豆都是适合食用的。 我的未煮过的土豆都不适合食用。 这盘中是否有新的土豆？

我想你可以使用LLM将这些陈述转换成某种形式，然后由某种推理引擎来解决。

讨论总结

本次讨论主要围绕如何使用替代大型语言模型（LLM）的推理引擎进行演绎推理展开。讨论中涉及了多种技术和方法，包括使用Prolog进行逻辑编程、Z3定理证明器解决复杂逻辑问题、以及“Good Old Fashioned AI”（GOFAI）等。参与者们分享了各自的经验和见解，提出了将LLM与这些推理引擎结合使用的可能性，并探讨了在逻辑推理中面临的挑战和潜在解决方案。总体而言，讨论氛围积极，参与者们对新兴技术和方法表现出浓厚兴趣。

主要观点

  1. 👍 LLM可以用于将逻辑陈述转化为Prolog代码

    • 支持理由：LLM能够处理自然语言，将其转化为适合Prolog处理的代码形式，从而实现逻辑推理。
    • 反对声音：LLM在生成正确谓词和关系代码方面存在挑战，需要进一步优化。

  2. 🔥 Z3定理证明器在逻辑推理中的应用

    • 正方观点：Z3能够处理复杂的逻辑问题，具有强大的推理能力。
    • 反方观点：Z3的使用门槛较高，需要将问题转化为适合其处理的代码形式。

  3. 💡 GOFAI与LLM的结合

    • 支持理由：GOFAI基于规则的推理系统可以与LLM结合，利用LLM作为直觉机器辅助推理，提升推理效率。
    • 反对声音：GOFAI已被大部分人放弃，重新结合可能面临技术和认知上的挑战。

  4. 👍 使用LLM将自然语言转换为逻辑命题

    • 支持理由：LLM能够将自然语言转换为逻辑命题，然后输入到推理系统中，简化推理过程。
    • 反对声音：LLM在处理复杂逻辑命题时可能存在误差，需要进一步验证和优化。

  5. 💡 《A Thousand Brains》对神经科学的启发

    • 支持理由：书中讨论了大脑使用皮质柱生成新参考框架的机制，对人工智能领域有重要启发。
    • 反对声音：实现这一过程在技术上具有极大挑战，目前仍处于理论阶段。

金句与有趣评论

  1. “😂 Use an LLM to turn the statements into Prolog and then solve with Prolog.”

    • 亮点：简洁明了地提出了将LLM与Prolog结合使用的方法，具有实际操作性。

  2. “🤔 I have implemented something in optillm that enables LLMs to use z3 to solve such queries.”

    • 亮点：展示了实际项目中使用Z3定理证明器解决逻辑推理问题的具体实现。

  3. “👀 Look up "good old fashioned AI" (GOFAI). It’s basically what you’re suggesting, but has been largely abandoned.”

    • 亮点：指出了GOFAI的历史地位和现状，引发了对结合LLM的思考。

  4. “😂 Are all the potatoes in the dish yours?”

    • 亮点：直接质疑了推理问题的前提条件，简洁而有力。

  5. “🤔 I recommend A Thousand Brains by Jeff Hawkins.”

    • 亮点：推荐了一本具有启发性的书籍，扩展了讨论的深度。

情感分析

讨论的总体情感倾向积极，参与者们对新兴技术和方法表现出浓厚兴趣。主要分歧点在于LLM在生成正确谓词和关系代码方面的挑战，以及GOFAI与LLM结合的可行性。这些分歧主要源于技术实现上的难度和认知上的差异。

趋势与预测

  • 新兴话题：LLM与传统推理引擎（如Prolog、Z3）的结合应用，以及GOFAI的复兴。
  • 潜在影响：这些技术的发展可能推动人工智能在逻辑推理领域的进步，提升复杂问题的解决能力。

详细内容：

《探索替代 LLM 的演绎推理方案》

在 Reddit 上，有一篇题为“Alternatives to LLM for deductive reasoning”的帖子引起了广泛关注，获得了众多点赞和大量评论。原帖指出 LLM 在演绎推理方面表现不佳，并询问是否存在通用的推理引擎（不限于特定领域，如数学），还提到了一个关于土豆的推理示例。

帖子引发的讨论焦点主要集中在各种可能的解决方案和相关技术。有人提出使用 LLM 将语句转换为 Prolog 然后用 Prolog 解决，并提供了相关链接[https://builtin.com/software-engineering-perspectives/prolog]。有用户分享道：“我在 optillm 中实现了一些东西（https://github.com/codelion/optillm/blob/main/z3_solver.py），使 LLM 能够使用 z3 来解决此类查询。” 还有人表示：“Z3 是微软研究的一个开源定理证明器，基于可满足性模理论（SMT） - https://github.com/Z3Prover/z3 ，它可以轻松解决比这大得多的公式。但挑战在于让 LLM 制定正确的谓词/关系并为其生成代码。”

也有人提到了曾经的“Chain of Thoughts”项目，建议进行调查。还有人推荐了解“good old fashioned AI”（GOFAI），并提供了相关的维基百科链接[https://en.wikipedia.org/wiki/GOFAI]。有人认为既然想避免使用 LLM，其实存在被称为“推理系统”的程序，可以将每个句子转换为一系列逻辑语句，比如在 Prolog 或其他逻辑编程语言中。甚至有人推荐了《A Thousand Brains》一书。

讨论中的共识在于大家都在积极探索替代 LLM 进行演绎推理的有效方法。但争议点在于哪种方法更具可行性和实用性。特别有见地的观点如有人指出语言模型可以根据提示中的明显特征切换到逻辑谜题模式，因为这些谜题的表述基本已经是符号形式。

总之，这次关于替代 LLM 进行演绎推理的讨论充满了各种创新和思考，为相关领域的发展提供了丰富的思路和方向。