人工智能研究，犯罪心理学，自闭症，我的一些想法

这三个真的像看起来风马牛不相及吗？ 现在的人工智能自我学习已经变成黑箱操作，人类不仅不知其所以然，也不敢说知其然，简而言之，不知道AI脑子里在想的全部过程。 这和研究犯罪心理的学者遇到的问题是一样的，他为什么要那么做? 自闭症患者，又称星星的孩子，其思维方式与普通人大相径庭，换句话说，不按套路出牌。但是他们真的是有自己的思路逻辑，只不过普通人想也想不到的。有时候，也许人工智能更能理解他们。 记得看过一个程序员提到的，让AI设计机器人十米赛跑，它的一个方案是制造了十米高的细长机器人，一开始就倒下，碰线，完美赢了。。。 如果我们仅仅满足于最后一项发明，让人类无法理解AI,，那么它可能也不能理解人类要的是什么，人类就是最坏的一个甲方，前后矛盾，口是心非，反复无常。。。

占坑 有点意思……

我常常觉得，那些很特别的动物，比如会和人拥抱的鸡啥的，其实就是鸡里的自闭症

学而不思则惘 思而不学则怠

在研究动物的时候，人们发现，海豚，猴子能知道镜子里的是自己。人类和动物的区别并没有那么大，高智商动物相当于五六岁的孩子，而人类恰恰就是五六岁开始懂事了，知道人是会死的，害怕死亡，那么动物呢？AI呢？它们有不甘心的灵魂吗？

不错

马住

赞最后一句

我说是甲方，实际上是甲方爸爸，而想想AI诞生了，它就是一个孩子啊！它好啊坏啊都是跟人类学的，鹦鹉学舌骂粗口，小艾上线不过几个小时就满满恶意各种脏话，人类自相残杀无恶不作却希望强大又聪明的后继者善良可爱呵护人类，宁可牺牲自己也要保护人类，十分的不靠谱啊！ 小时候觉得阿西莫夫的机器人三原则有道理，现在一想压根儿对不上，现在的机器人何必做出人样子，自动驾驶汽车就是智能，不需要手和脚，无人机也不长脑袋，而它们杀人比机器人效率可高多了。 看看阿塞拜疆和亚美尼亚那两个弹丸小国才是未来战争，无人机追着坦克打，遥控武器炸目标，没有人觉得那是机器人。。。

我说是甲方，实际上是甲方爸爸，而想想AI诞生了，它就是一个孩子啊！它好啊坏啊都是跟人类学的，鹦鹉学舌骂粗口，小艾上线不过几个小时就满满恶意各种脏话，人类自相残杀无恶不作却希望强大又聪明的后继者善良可爱呵护人类，宁可牺牲自己也要保护人类，十分的不靠谱啊！ 小时候觉得阿西莫夫的机器人三原则有道理，现在一想压根儿对不上，现在的机器人何必做出人样子，自动驾驶汽车就是智能，不需要手和脚，无人机也不长脑袋，而它们杀人比机器人效率可高多了。 看看阿塞拜疆和亚美尼亚那两个弹丸小国才是未来战争，无人机追着坦克打，遥控武器炸目标，没有人觉得那是机器人。。。
dingdingdddd 发表于 2020-10-02 20:39

层主很年轻吧，多年前这些东西就叫机器人，现在名字多了

楼主讲得太好了，请一定要继续。你是说自闭症谱系等等非neuraltypical的思维方式类似AI, machine learning吗？

楼主讲得太好了，请一定要继续。你是说自闭症谱系等等非neuraltypical的思维方式类似AI, machine learning吗？
bepatient 发表于 2020-10-02 21:57

我不知道思维方式是不是，至少训练自闭症的方式是一样的，现有的自闭症训练模式完全靠一个场景一个场景的学怎么应付。他们要与普通人相处，就得像表演一样，靠智力记住而不是自然而然表达。 举例说明，老师会模拟有人打招呼，他就知道该直视对方露出微笑回应。这种情况如果是个正常人，就是本能。哪怕是初生孩子都知道咿咿呀呀伸手要抱抱不用教。

人工智能的大数据喂养就跟人类养孩子一样的，给的是啥长的就是啥，而且如果人为制造善良正义的温室，一旦放出来，它会不会认知崩溃呀？

微软AI要参加IMO竞赛！小目标：数学金牌 贾浩楠 2020-10-03 13:20:31 来源：量子位
今年，可能是最后一届“纯人类”参赛的IMO

贾浩楠 萧箫 发自 凹非寺

量子位 报道 | 公众号 QbitAI

今年，可能是最后一届“纯人类”参赛的IMO （国际奥数竞赛）。 △参加2020年IMO的中国代表队（李金珉的官方年龄信息有误） 因为在明年，AI可能也会加入这场金牌争夺战中，成为一名“种子选手”。 这名潜入IMO赛事的AI名为Lean，由微软的研究人员开发。 目前，他们正计划让Lean参与明年的国际奥数竞赛。 也就是说，它将与世界各国的奥赛选手一起争夺IMO金牌。 准备在IMO上一展身手的Lean 其实，微软研究人员让AI参加IMO的理由，原因是它是个很好的实验工具（工具人）。 微软研究员Selsam是挑战赛IMO Grand Challenge的创始人之一，他表示，这项比赛的目的是训练一个人工智能系统，以便在世界顶级数学竞赛中赢得金牌。 因为这里不仅有数学上“最简单”的难题（连高等数学都用不上，但就是做不出来），而且还汇集了来自世界各地的顶尖高手。 如果AI能像人一样证明这些数学定理，某种程度上也能说明，让它“像人一样思考”不会太过困难。
基于这个想法，微软的研究人员从2013年开始研发Lean，希望让AI能拥有自主判断、根据假设进行演绎的能力。 也就是说，它是个旨在缩小交互式定理证明、与自动定理证明之间的差距的开源项目。

自动定理证明：对数学中提出的定理或猜想，寻找一种证明或反证的方法。系统不仅能根据假设进行演绎，还要有一定的判定技巧。

交互式定理证明：借助计算机辅助证明工具，理解检验数学定理正确性，完成数学定理的证明。

Lean已经推出了3个版本，现在的第四个版本Lean 4还在完善中，现在的逻辑系统基于依赖类型理论，已经强大到足以证明所有的常规数学定理。 也就是说，想要让它自己证明IMO中提出来的、此前“没见过的”数学问题，依旧非常困难。 目前，Lean 4还没有彻底做好准备，作者Leonardo de Moura表示，如果让它参加今年的IMO，“可能只能得0分”。
因为，Lean目前甚至无法理解某些数学问题需要涉及哪些概念，而这些概念本身又是“什么意思”。 证明的“第一步”，就难住了算法 对于不少人来说，数学十分抽象、难以学好。 事实上，AI和你的感觉一样。 一般的工程应用问题中，AI得心应手，因为在预训练阶段，算法模型已经对一类问题有所了解。 也就是说，AI现阶段能干的活仍然有限，通常要给定条件和数据，经过持续的“刷题”，才能做“更复杂的计算”。 这是一个从“1”到“2”、“3”，甚至是无穷的过程。
但数学问题的证明本质并不一样，证明一个公理，或是一个复杂的等式，需要完全“白手起家”。 证明的第一步：提出一个合理证明路径。这个从0到1的关键，目前只有人类的大脑能胜任。 绝大部分AI，很难给出证明思路的第一步。 拿一个最简单最古老的数学公理来说，公元前300年，欧几里得就证明了质数有无限多个。
而要证明这一结论，关键是要认识到，总是可以通过乘所有已知的质数并加1来找到一个新的质数。有了这个思路，接下来的证明就很简单了。 但“想到这个思路”这一行为本身，对于AI来说，难度巨大。 说回IMO，正式比赛中的3道题目，尽管不涉及微积分等高等数学，但无一不是要求选手利用中学的所有数学知识，进行巧妙的构思给出解题方法。 比如这道2005年IMO真题：
当时不同国家的参赛选手至少给出了3种不同的证明，其中被广泛认可讨论的解法，采用柯西不等式简化的思路，篇幅大概需要半页A4纸。 而另一位来自摩尔多瓦的选手，极富创造性的用两行式子完成了证明：
上面一行是“因为”，下面一行就是“所以”，其简洁、精准甚至可以说“粗暴有效”震惊全场。 精巧的思路也获得了当年的IMO特别奖。 要说明的是，IMO特别奖不看总成绩，只颁给解题方法独到的选手。 这种石破天惊的“第一步”，对于现在的AI来说，几乎是不可能做到的。 这也许就是为什么微软的研究人员设定的目标是“冲击金奖”吧。 巧的玩不转，Lean采取什么方法跟人类大脑竞争呢？ Lean如何学数学？ Lean和所有AI算法一样，需要“喂数据”进行训练。
目前的Lean，不但无法设计出完整的IMO题目证明过程，它甚至无法理解其中一些问题所涉及的概念。 所以，Lean的首要任务是学习更多的数学知识。 训练数据来自Mathlib的库。Mathlib是一个数学基础数据库，它几乎包含了大学二年级以下所有数学知识。 但Mathlib在中学数学上仍有一些差距，团队正在对Mathlib数据库进行补全。 掌握知识只是第一步，如何灵活运用才是关键。 团队采取的方法与象棋、围棋AI等相同——遵循决策树，直到算法找到最优解。
许多IMO题目的关键是寻找某种证明的模式。深入数学证明的底层，是一系列非常具体的、有逻辑的步骤。 研究人员尝试通过IMO题目证明的全部细节来训练Lean。 但在这种方法也有局限，每个特定的题目证明对于算法来说太“专”，下一个不同类型题目仍然不会解。 为了解决这个问题，团队需要数学家写出之前IMO题目的详细形式化证明。然后，团队提炼证明中的采用的不同策略。 接下来，Lean的任务，就是在这些策略中寻找一个 “胜利 “的组合。 这项任务实际上比描述起来困难的多，团队这样比喻它：

在围棋中，目标是找到最好的一步棋。而在数学中，目标是找到最好的一盘棋，然后在这盘棋中找到最好的一步棋。

团队说，也许到了明年，获得金牌仍然是很困难的，但至少，Lean有机会参赛了。 对此，有网友感叹AI这些年神速的进展：先是国际象棋、又是围棋……现在，AI又要来攻占国际奥赛金牌了。
但也有网友持悲观态度，认为AI现阶段只能在某些方面趋近人类的水平。

目前AI的算法，都是建立在人类认知基础上的……所以像（证明数学定理）这样特殊的任务，我持消极态度，毕竟世界上只有少部分人能提供帮助。

“什么是数学思想？” 这个问题出乎意料的难以解释透彻。数学家在尝试解决新问题时，大脑的活动是难以描述的，更不要说落实在算法上。 尽管已经有AI团队朝数学思想的深层迈出了一步，但是从他们采取的策略来看，仍然是学习过往思路，选择成功率最高的“排列组合”。 这样的AI算法，要在创造力和突破性上超越人类，“火候”还差得远。 而隔壁的GPT，也在数学证明方向上取得了初步成果。 最近，OpenAI推出了用于数学问题的GPT-f，利用基于Transformer语言模型的生成能力进行自动定理证明。
由GPT-f发现的23个简短证明已被Metamath主库接收，这也是首次AI的数学证明获得业内认可。 GPT真的是要砸所有人的饭碗，连数学家都不放过。
那么，Lean和GPT-f，你更看好哪一个呢？ 项目链接： https://leanprover.github.io/ 在线可玩： https://leanprover.github.io/live/master/ 参考链接： https://leodemoura.github.io/ https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/ https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921