评论一下苹果那篇论文

[牛河梁]

看来我猜对了。

其实我也是同样的观点。

这倒是没错，有用的东西，谁会拿去灌水？

一哥们给公司做的系统，都卖钱了，几十万人刀一份软件包。人家根本对学校职称不感兴趣。

☆ 发自新买提 Android 25.05.07

老牛大学毕业的时候，当时有两派意见。主管研究生的系副主任是当时很少的计算机专业博士，鼓励老牛深造。主管本科教育的系副主任是清华毕业的，让老牛去做工程做实际的东西，不要去搞（什么）理论。

这位清华的对老牛后来人生影响很大。计算机应用到处都是处女地。搞理论的空对空纠结系统不完美没法完美能被骗可能说瞎话。老牛一直对别人说，不追求完美，如果计算机能解决90%的情况，那么人类效率就提高了10倍。如果能解决99%，那么就是100倍大跃进。

人工智能也是如此。就是know-how。老牛（们）当年英语很差。小留们怕是难以想象题都读不懂，是咋混到GRE逻辑和数学满分的。反过来说，题都读不懂，就像金庸小说里不识字的看出了书法里的武功招式，自然看到了其它语言里的现象直接知道答案。

一个问题一个问题地去解决。人知道了该怎么做。就能教计算机怎么做。这些应用（改善）可以是无止境的。下室里琐男每一个小进步，都可能是人类的一大步。

这一点，这些年来清华学风等都歪了。

[hci]

同意。

老牛大学毕业的时候，当时有两派意见。主管研究生的系副主任是当时很少的计算机专业博士，鼓励老牛深造。主管本科教育的系副主任是清华毕业的，让老牛去做工程做实际的东西，不要去搞（什么）理论。

这位清华的对老牛后来人生影响很大。计算机应用到处都是处女地。搞理论的空对空纠结系统不完美没法完美能被骗可能说瞎话。老牛一直对别人说，不追求完美，如果计算机能解决90%的情况，那么人类效率就提高了10倍。如果能解决99%，那么就是100倍大跃进。

人工智能也是如此。就是know-how。老牛（们）当年英语很差。小留们怕是难以想象题都读不懂，是咋混到GRE逻辑和数学满分的。反过来说，题都读不懂，就像金庸小说里不识字的看出了书法里的武功招式，自然看到了其它语言里的现象直接知道答案。

一个问题一个问题地去解决。人知道了该怎么做。就能教计算机怎么做。这些应用（改善）可以是无止境的。下室里琐男每一个小进步，都可能是人类的一大步。

这一点，这些年来清华学风等都歪了。

[Caravel]

看来我猜对了。

其实我也是同样的观点。

老牛那种rule based 效果肯定被现在的LLM吊打

[Caravel]

神经网有输入（输出）窗口长度限制。现在能有几K token，没谁那么无聊绕那么大的圈子才进正题。但20年前没有这么强大的算力。也没有那么大的窗口。如果关键的概念挤不进一个窗口，理解肯定就错了。

相比之下用规则去找/决定一个完整的结构不难。

我相信LLM理解自然语言是走对了路

自然语言理解就是一种高维条件概率

你们那种rule最多只能理解NL的一个比较规则的subset

[牛河梁]

我相信LLM理解自然语言是走对了路

自然语言理解就是一种高维条件概率

你们那种rule最多只能理解NL的一个比较规则的subset

理论留给北大做。（你们）清华的还是脚踏实地多为祖国/人类多做贡献为好。特别是不要发考题当久了，脑子当傻了。

没有实践，就没有发言权。理论上，你这么说没有错似乎没法反驳。实践上，一文不值。

如果你面对的是外星人的语言，或者上帝的语言（如物理实验数据），那么你可能对。

问题是，你面对的是人类的语言。这语言是设计给（一般水平）人类能够阅读理解的。

别说无限规则（图灵机的规则都是有限的没那么牛），就是规则上万，有多少人可以掌握。怕是发明规则的人自己都记不住。

实践上，每加一条新规则，等于系统加一条公理。人类的几何、集合论才几条公理。老牛可以说，当规则达到20左右，正确率已经高于人类的行业专家阅读水平了。

受过高等教育的专家当然懂更多的（英语）规则/惯例，但实践上有多少case是需要这么罕见的语言规则的。

[bihai]

这种诡辩毫无意义。注意楼上老牛认为的第一点：

1/ 人脑（智能）如语言，并没有超过计算机科学/理论的极限。

人工智能受哥德尔定理限制。（可数脑细胞的）人脑也同样受哥德尔定理限制。这不是人工智能超不过人脑智能的理由。

你了解哥德尔的证明啊？我不是很懂啊。前天看了一下，浑身不舒服。

哥德尔给出了12个符号，然后又有一个subst函数。这个函数不是12个符号里的？那在什么地方用的啊？

[Caravel]

理论留给北大做。（你们）清华的还是脚踏实地多为祖国/人类多做贡献为好。特别是不要发考题当久了，脑子当傻了。

没有实践，就没有发言权。理论上，你这么说没有错似乎没法反驳。实践上，一文不值。

如果你面对的是外星人的语言，或者上帝的语言（如物理实验数据），那么你可能对。

问题是，你面对的是人类的语言。这语言是设计给（一般水平）人类能够阅读理解的。

别说无限规则（图灵机的规则都是有限的没那么牛），就是规则上万，有多少人可以掌握。怕是发明规则的人自己都记不住。

实践上，每加一条新规则，等于系统加一条公理。人类的几何、集合论才几条公理。老牛可以说，当规则达到20左右，正确率已经高于人类的行业专家阅读水平了。

受过高等教育的专家当然懂更多的（英语）规则/惯例，但实践上有多少case是需要这么罕见的语言规则的。

“老牛可以说，当规则达到20左右，正确率已经高于人类的行业专家阅读水平了。”

别吹了，你能写出20条规则，能识别那10个手写数字，超过人类水平，那就一辈子吃穿不愁了

[牛河梁]

你了解哥德尔的证明啊？我不是很懂啊。前天看了一下，浑身不舒服。

哥德尔给出了12个符号，然后又有一个subst函数。这个函数不是12个符号里的？那在什么地方用的啊？

不要太拘泥于哥德尔的具体逻辑系统，就像不需要太拘泥于图灵机怎么样一样。

哥德尔定理的核心是，将就着看不是论文，一个可数有限数值（如真假）（所以可以映射为整数表示），可数有限运算（如与或非）（所以可以映射为整数表示），以上值和运算组合成的定理集合（可以视为函数）。这些无限可能定理是可数的。每一条定理都可以对应一个整数（哥德尔数，自己看维基）。

知道这些定理是可数的，就可以用康托尔的对角线法构造一个反例。存在一个不可数的定理（不可在有限步骤里被证明）。

图灵机类似。图灵机的符号规则都是可数有限的，所以每一个图灵机可以用一个整数表示（code、码工的代码）。所以图灵机总数是可数的。然后就可以构建一个不可数的问题。图灵机不能（在有限步骤）解决。

[牛河梁]

“老牛可以说，当规则达到20左右，正确率已经高于人类的行业专家阅读水平了。”

别吹了，你能写出20条规则，能识别那10个手写数字，超过人类水平，那就一辈子吃穿不愁了

老牛早就不愁吃喝。

你说这这话没意义。

识别数字其实不难。

毕竟只有十种情况。

[Caravel]

老牛早就不愁吃喝。

你说这这话没意义。

识别数字其实不难。

毕竟只有十种情况。

10个数字，手写体也是千变万化，这是乐村的成名作。这么简单的任务rule，rule base也不是神经网络对手

[牛河梁]

我不知道你脱离具体问题的事例在抽象层面上夸夸其谈有什么益处，只知道我拿我的领域里头但我不熟悉的东西问大模型，它的回答的准确性非常高，像已经在那个方向做了很久的很有经验的学者。我问的问题非常具体深入还有各种变量符号，相信训练内容里头没有现成答案。也许大语言模型背后的确就是模式匹配，线性拟合和局域最小值，但最终的返回的结果却让我感觉对面不是一台机器，而是出现了人类的智能。

不针对版主。但法考题和攻城狮的确不同。法考题们习惯了批判性精神。啥出来都要批判一通。攻城狮遇到新鲜事物，首先想到的是（对自己）有没有用，怎么用，当然也要了解一下缺陷。谁管黑盒里是扔骰子还是藏着个印度人。抓到老鼠就是好猫。

老牛就觉得GPT们很好用。别说（辅助）证明定理。举例说最近老牛要设计/改进后院浇水灌溉系统，GPT威力就很大。省了老牛很多放狗和计算时间。给出所有尺寸参数，GPT像模像样搞出一整套方案，还用文字符号画图给出不同部件的规格及安装在何处。

有些东西放狗找出来的页面那个人如果他也不知道的，自然也不会写，老牛也就不会知道unknown-unknown。

[牛河梁]

10个数字，手写体也是千变万化，这是乐村的成名作。这么简单的任务rule，rule base也不是神经网络对手

你还是先恶补一下Ai，别开口就是笑话。

你的人工神经网靠的也是“规则”去识别图像。区别在于这些“规则”是“机器学习”机器自己总结出来的。老牛的语言规则是人学习总结出来的。

想想你看汉字怎么认字的。汉字变化不更多。

[bihai]

不要太拘泥于哥德尔的具体逻辑系统，就像不需要太拘泥于图灵机怎么样一样。

哥德尔定理的核心是，将就着看不是论文，一个可数有限数值（如真假）（所以可以映射为整数表示），可数有限运算（如与或非）（所以可以映射为整数表示），以上值和运算组合成的定理集合（可以视为函数）。这些无限可能定理是可数的。每一条定理都可以对应一个整数（哥德尔数，自己看维基）。

知道这些定理是可数的，就可以用康托尔的对角线法构造一个反例。存在一个不可数的定理（不可在有限步骤里被证明）。

图灵机类似。图灵机的符号规则都是可数有限的，所以每一个图灵机可以用一个整数表示（code、码工的代码）。所以图灵机总数是可数的。然后就可以构建一个不可数的问题。图灵机不能（在有限步骤）解决。

十年前我突然对计算机验证定理证明感兴趣。就是比如在ipad上有个app，可以让小孩手动证明几何题目，其证明过程要图形化，拖拽模块，然后把已知条件和证明过的条件拽入其中，然后由app来验证次证明是对的。

这个关键是，如何验证呢？我知道机器证明早就实现了，不过我还是卡住了。我不知道该如何描述定理，和动态保存新的定理。我现在重新看哥德尔定理，也是下获取一些灵感。我刚才重新看了一下哥德尔定理的解释，目前卡在这里

“存在某个哥德尔数为x的公式序列，可以证明哥德尔数为k的公式”，或者简言之，“哥德尔数为k的公式可以被证明”。

我不清楚这个东西是怎么用哥德尔的12个符号描述的。

[牛河梁]

十年前我突然对计算机验证定理证明感兴趣。就是比如在ipad上有个app，可以让小孩手动证明几何题目，其证明过程要图形化，拖拽模块，然后把已知条件和证明过的条件拽入其中，然后由app来验证次证明是对的。

这个关键是，如何验证呢？我知道机器证明早就实现了，不过我还是卡住了。我不知道该如何描述定理，和动态保存新的定理。我现在重新看哥德尔定理，也是下获取一些灵感。我刚才重新看了一下哥德尔定理的解释，目前卡在这里

“存在某个哥德尔数为x的公式序列，可以证明哥德尔数为k的公式”，或者简言之，“哥德尔数为k的公式可以被证明”。

我不清楚这个东西是怎么用哥德尔的12个符号描述的。

不要太拘泥于哥德尔的表达。哥德尔比较早。现代用的是后来香农提倡的布尔代数。

对你的问题就是一堆已知为真的公理定理积木。然后一些逻辑算符。

当然，这些积木不是都能被逻辑算符连接起来，需要有条件。如关于三角形的定理和正方形不能接起来。

当小孩们搭建好了一个结构（公式），你算起真值就行了。

取决于你怎么设计App。举例说你搞成像拼图。三角形的部件（定理/公理/定义）不能放进正方形的框里。

[bihai]

不要太拘泥于哥德尔的表达。哥德尔比较早。现代用的是后来香农提倡的布尔代数。

对你的问题就是一堆已知为真的公理定理积木。然后一些逻辑算符。

当然，这些积木不是都能被逻辑算符连接起来，需要有条件。如关于三角形的定理和正方形不能接起来。

当小孩们搭建好了一个结构（公式），你算起真值就行了。

取决于你怎么设计App。举例说你搞成像拼图。三角形的部件（定理/公理/定义）不能放进正方形的框里。

行那我找找现代的表达方式。

我那个需求对我来说问题不是UI，而是如何用数据结构存储定理。定理里面的条件和结论都如何描述？比如怎么表示“存在”，“共线”，“任意一点”。对于用户推理出来的定理如何存储，如何利用，如何验证推理过程。

数据结构，用map吗？用调节对表示推理({条件几何},{结论几何})？

[bsmile]

啥？＂运行的逻辑我们不能完全理解＂= ＂拟人的智能＂？

你脑子里漿糊太多了。

你根本就没看懂我说什么，和你争论毫无价值。

我的意思是现在的大模型出来的结果已经不再是由它的算法表面上看起来的简单的排列组合和内容提取，如果从反馈的结果来看，已经可以看到人的思维的影子，好像一个很有经验的研究者在对面逐条地启迪你帮助你。正如爱因斯坦的广义相对论的等效原理，如果只是让你感觉的话，你在重力场和在加速上升的电梯里头是等价的，所以你区分不了你是在重力场中，还是在加速上升的电梯中，所以你可以拿加速度去研究重力。同样地，如果只是让你感觉反馈在屏幕上的回答，你区分不了是人还是机器，所以我叫它拟“人”的“智能”。

[hci]

你表达的，就是＂处女生子＂的magic thinking。

看你的用词＂看到．．的影子＂，与看到了神有什么区别？＂感觉＂如何如何，都它妈的宗教用语。

我不在与你争论，在指出你思维的问题，思维要能具体化，你不能。

你根本就没看懂我说什么，和你争论毫无价值。

我的意思是现在的大模型出来的结果已经不再是由它的算法表面上看起来的简单的排列组合和内容提取，如果从反馈的结果来看，已经可以看到人的思维的影子，好像一个很有经验的研究者在对面逐条地启迪你帮助你。正如爱因斯坦的广义相对论的等效原理，如果只是让你感觉的话，你在重力场和在加速上升的电梯里头是等价的，所以你区分不了你是在重力场中，还是在加速上升的电梯中，所以你可以拿加速度去研究重力。同样地，如果只是让你感觉反馈在屏幕上的回答，你区分不了是人还是机器，所以我叫它拟“人”的“智能”。

[bsmile]

你表达的，就是＂处女生子＂的magic thinking。

看你的用词＂看到．．的影子＂，与看到了神有什么区别？＂感觉＂如何如何，都它妈的宗教用语。

我不在与你争论，在指出你思维的问题，思维要能具体化，你不能。

和你说不清楚，爱因斯坦的联想没问题，我的联想就有问题？不再回复

[bihai]

有点像BoW



☆ 发自新买提 Android 25.05.07

是的，我记得是在bow或者是rainbow，我写了一个函数，替代那个tokenizer，因为原来的不能处理特殊西班牙语符号。然后我用C++替代MATLAB的矩阵乘法，用了多线程。当时是接近4GB内存都用满了。