Moravec悖论的诘问是：为何AI能够完成一些在人看来很困难的任务，例如战胜国际象棋世界冠军，却经常在一些对普通人而言很简单的任务上失败？就数学证明而言，Moravec悖论依然成立。对人来说，发现并形式构造一个非琐碎数学命题的证明过程往往不容易；作为对比，如果已有一个证明过程，检查其是否正确往往相对容易得多。有趣的是，大模型（LLM）的表现似乎恰好相反—通常能够快速生成符合基本形式规范的“证明过程”，但无论是自查还是互查，LLM都无法以足够高的准确率判定证明过程的正确性。出现这种反差的原因实际上并不难理解，只需了解LLM的基本工作原理。

LLM生成证明的方式与生成文本的机制是基本相同的，其算法框架都可归结为早已有之的统计语言模型（SLM）。SLM的核心计算是估计条件概率Pr(wn+1|wn,…,w1)，即在给定上文n个单词（wn,…,w1）的条件下，估计单词wn+1出现的概率。这个概率的计算一般需要基于大量文本的统计信息。对于文本类任务（例如机器翻译或问答系统）来说，按照这个概率来顺序地生成一个词序列，并将其作为任务模型的输出（即译文或对提问的回答）是问题不大的。如此生成的任务输出虽然经常也会出现一些瑕疵，但它们至少看上去都可接受。因为他们的生成毕竟都基于大量人类文本的统计规律；并且，文本类任务的输出往往是开放性的，经常没有严格的对错标准，所以模型的输出即使有一些反常之处，也在一定程度上可以被理解为个性的表达方式。但对于定理证明而言，上述依赖于统计的工作方式经常会导致灾难性的后果，因为它完全不理解（甚至根本不关注）文本（包括数学符号）间的统计相关是否等于逻辑关系，以及上述逻辑关系的适用条件。考虑如下假想的例子：某LLM为证明“A蕴含C”，构造了如下的证明序列——“A蕴含B，B蕴含C”。显然，此证明序列之所以可能被LLM生成，是因为在其语料库中，分别存在“A蕴含B”和“B蕴含C”的文本。但是，如果LLM不能理解语料上下文中所给出的“A蕴含B”和“B蕴含C”的适用条件，而仅凭这两个符号串曾分别在若干语料中出现过这个观察就生成了这样一个证明序列，往往会得到一个无效的证明。现实中的情况甚至可能更糟糕，因为在很多语料中，有些基本前提是隐而不述，例如初等数学文献中一般不会明确地说“若l1和l2是平行线，则两者不相交”的前提是只考虑欧几里得几何。所以，如果LLM在解一个黎曼几何中的问题时错误地使用了“若l1和l2是平行线，则两者不相交”这个结果，完全不令人惊讶。这是因为LLM的语料中可能混杂着欧几里得几何和黎曼几何的文献，但建立在统计相关估计机制上的LLM没有能力，甚至也并不太关注如何去建模和理解数学概念之间的复杂逻辑谱系，因此就无法准确判断数学结果之间的相容性。所以，它在构造“证明序列”时很可能只基于文本片段在语料库中的出现频次而将并不相容的数学结果错误地连接起来，生成完全无意义的“证明序列”。这样的大模型不具备真正的逻辑理解和推理能力，自然也就无法基于逻辑检查一个证明的对错，即表现出了典型的Moravec悖论现象。

———————————————————————————————————————————————————————————————————

当然，现在有很多人是在夸大宣传大模型。这些人中，有些是利益相关的从业者，有些则是发自真心的fans。第一类人先不论；在我看来之所有有第二类人存在，不外乎是两个原因：1 知识储备严重不足，不求甚解，所以容易似被是而非甚至有硬伤的东西唬住了；2 关注的问题太简单，用信息检索增强（大模型功能的一个子集）就能搜到正确答案。实际上，如果你多用用大模型，并且有一定的知识基础和分析能力，就很容易发现：对于稍有难度的问题，大模型所给出的靠谱答案基本都是搬运而来的，而非自主生成（分析推理）出来的。
--
修改:qtpr FROM 111.167.232.*
FROM 111.167.232.*