首页 » 人工智能 »

符号主义

2018年5月20日 / 85次阅读

打开支付宝首页,搜索“529018372”,即可领取红包!可重复领。

对符号主义是做什么的不甚了解,下文转自知乎顾险峰的文字,链接:https://zhuanlan.zhihu.com/p/20648971

 

人工智能中,符号主义的一个代表就是机器定理证明,其巅峰之作是吴文俊先生创立的吴文俊方法。目前机器定理证明的理论根基是希尔伯特定理:多元多项式环中的理想都是有限生成的。我们首先将一个几何命题的条件转换成代数多项式,同时把结论也转换成多项式,然后证明条件多项式生成的理想包含结论对应的多项式,即将定理证明转换为理想成员判定问题。一般而言,多项式理想的基底并不唯一,Grobner基方法和吴方法可以生成满足特定条件的理想基底,因此都可以自动判定理想成员问题。因此理论上代数范畴的机器定理证明可以被完成。但是,实际中这种方法有重重困难。

首先,从哲学层面上讲,希尔伯特希望用公理化方法彻底严密化数学基础。哥德尔证明了对于任何一个包含算术系统的公理体系,都存在一个命题,其真伪无法在此公理体系中判定。换言之,这一命题的成立与否都与此公理体系相容。这意味着我们无法建立包罗万象的公理体系,无论如何,总存在真理游离在有限公理体系之外;另一方面,这也意味着对于真理的探索过程永无止境。

其次,从计算角度而言,Grobner基方法和吴方法的复杂度都是超指数级别的,即便对于简单的几何命题,其机器证明过程都可能引发存储空间的指数爆炸,这揭示了机器证明的本质难度。

第三,能够用理想生成的框架证明的数学命题,其本身应该是已经被代数化了。例如所有的欧几里得几何命题,初等的解析几何命题。微分几何中的许多问题的代数化,本身就是非常具有挑战性。例如黎曼流形的陈省身-高斯-博内定理:流形的总曲率是拓扑不变量。如果没有嘉当发明的外微分和活动标架法,这一定理的证明无法被代数化。拓扑学中的许多命题的代数化本身也是非常困难的,比如众所周知的布劳威尔不动点定理:我们用咖啡勺缓慢均匀搅拌咖啡,然后抽离咖啡勺,待咖啡静止后,必有一个分子,其搅拌前和搅拌后的位置重合。这一命题的严格代数化是一个非常困难的问题。吴先生的高徒,高小山研究员突破的微分结式理论,系统地将这种机器证明方法从代数范畴推广到微分范畴。

最后,机器定理证明过程中推导出的大量符号公式,人类无法理解其内在的几何含义,无法建立几何直觉。而几何直觉和审美,实际上是指导数学家在几何天地中开疆拓土的最主要的原则。机器无法抽象出几何直觉,也无法建立审美观念,因此虽然机器定理证明经常对于已知的定理给出令人匪夷所思的新颖证明方法,但是迄今为止,机器并没有自行发现深刻的未知数学定理。

比如,人类借助计算机完成了地图四色定理的证明,但是对于这一证明的意义一直富有争议。首先,是人类将所有可能情形进行分类,由机器验证各类情形;其次,这种暴力证明方法没有提出新的概念,新的方法;再次,这个证明没有将这个问题和其它数学分支发生深刻内在的联系。数学中,命题猜测的证明本身并不重要,真正重要的是证明所引发的概念思想,内在联系和理论体系。因此,许多人认为地图四色定理的证明实际上“验证”了一个事实,而非“证明”了一个定理。

因此,和人类智慧相比,人工智能的符号主义方法依然处于相对幼稚的阶段。

本文链接:http://www.maixj.net/ai/fuhaozhuyi-18014
云上小悟 麦新杰(QQ:1093023102)

评论是美德

无力满足评论实名制,评论对非实名注册用户关闭,有事QQ:1093023102.


前一篇:
后一篇:

栏目精选

云上小悟,麦新杰的独立博客

Ctrl+D 收藏本页

栏目

AD

ppdai

©Copyright 麦新杰 Since 2014 云上小悟独立博客版权所有 备案号:苏ICP备14045477号-1。云上小悟网站部分内容来源于网络,转载目的是为了整合信息,收藏学习,服务大家,有些转载内容也难以判断是否有侵权问题,如果侵犯了您的权益,请及时联系站长,我会立即删除。

网站二维码
go to top