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.*

写的很好！
你这里解释的只是大模型目前存在的问题，但是并不代表这些问题不能解决，而且在我看来有一些问题通过努力是可以解决的。

举几个例子，大模型经常会出现如下类型的错误：
1. 数据引用错误
2. 张冠李戴错误

对于第一类错误，可以通过定义可信数据来源，包括引入数据库，交叉检验的方式，对于输出信息进行校正是可以解决的。

对于第二类错误，也可以通过大量的人类标记来纠正。

当然目前大模型的逻辑可能是通过用户的交互使用，来二次训练提升信息的准确率。

但是以上的解决办法只能提升大模型的输出信息准确率，无法提升大模型的思考能力和智商水平。

【 在 qtpr 的大作中提到: 】
: 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悖论现象。
: ———————————————————————————————————————————————————————————————————
: ...................
--
FROM 123.115.209.*

这是两回事了，我的意思是准确性的问题能够解决，行业可能用更好的方式解决。
难点在于突破人类的专家水平或者智商，这个方向上似乎现有的模型无法解决。

【 在 qtpr 的大作中提到: 】
: 那人工来找补就又回到了之前“有多少人工就有多少智能”的老路，跟宣传的“数据驱动的突现智能”是两回事了。
: 另外，靠人工弥补只是权宜之计，不可持续发展，我个人不看好。
:
--
FROM 123.115.209.*

我们研究ai的，不需要尝试就知道啊
你这暴露了自己是不理解原理啊

【 在 qtpr 的大作中提到: 】
: 举个例子：让我deepseek尝试证明一个很小的初等代数问题。它假装分析了一通，给出了一个“证明”，在解析证明之外还做了数值验证，看上去煞有介事似乎很严谨。其实证明根本是不成立的，它根本不自知，还骗我说已经证明了（当然它不是有意骗，实际上它根本不知道自己在说什么），呵呵。
:
: [upload=1][/upload][upload=2][/upload]
--
FROM 223.104.151.*

你懂个屁原理，你只懂怎么吹牛

【 在 hut 的大作中提到: 】
: 我们研究ai的，不需要尝试就知道啊
: 你这暴露了自己是不理解原理啊
--
FROM 111.167.232.*