c*n
2 楼
是啊 尤其是有人推断这是给alphago对练的ai 不喂棋谱 纯训练练出来的
w*g
8 楼
我们有生之年应该能看到电脑自动写程序吧。
现在engineering的关键是怎么把人类面对的各种稀奇古怪的
task自动转换成固定的类似下棋的套路。这个并不容易。
打个比方,通用计算机take over之前,有各种机器,
比如电视机,CD机,电话机,打字机,还有各种专业的
DSP芯片啥的啥的。现在的人智其实就处于这么一种
状态,有图像识别人智,下棋人智,等等。有一个新
的任务过来,目前可以达到人类用现有的轮子可以做到
超过人类的水平。但是“用轮子”这一步还需要人,
虽然这一步已经变得比较容易了。或者说,有了接口
后,其实对AI都容易,但是定义接口还需要人类。
还有就是目前基于CNN的人智其实没啥逻辑能力。
所以下棋其实不是纯人智,而是人智+超大规模暴力
搜索。或者说,目前人类已经找到了一种办法,
可以用人智来大规模加速暴力搜索。
我个人预测,下一步被攻克的将是数学定理证明。
纯数学家将会先于马公失业。定理证明和下棋一样,
都属于接口定义非常简单明确,但是问题复杂性
很高的那种问题。有一小撮脑子好使的人类非常
推崇这一类问题。AI对这一小撮人将会是非常大
的打击。
【在 p**r 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 连车尾灯都看不见的那种绝尘而去?
: 那应用在其他方面也是分分秒秒的事吧?
现在engineering的关键是怎么把人类面对的各种稀奇古怪的
task自动转换成固定的类似下棋的套路。这个并不容易。
打个比方,通用计算机take over之前,有各种机器,
比如电视机,CD机,电话机,打字机,还有各种专业的
DSP芯片啥的啥的。现在的人智其实就处于这么一种
状态,有图像识别人智,下棋人智,等等。有一个新
的任务过来,目前可以达到人类用现有的轮子可以做到
超过人类的水平。但是“用轮子”这一步还需要人,
虽然这一步已经变得比较容易了。或者说,有了接口
后,其实对AI都容易,但是定义接口还需要人类。
还有就是目前基于CNN的人智其实没啥逻辑能力。
所以下棋其实不是纯人智,而是人智+超大规模暴力
搜索。或者说,目前人类已经找到了一种办法,
可以用人智来大规模加速暴力搜索。
我个人预测,下一步被攻克的将是数学定理证明。
纯数学家将会先于马公失业。定理证明和下棋一样,
都属于接口定义非常简单明确,但是问题复杂性
很高的那种问题。有一小撮脑子好使的人类非常
推崇这一类问题。AI对这一小撮人将会是非常大
的打击。
【在 p**r 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 连车尾灯都看不见的那种绝尘而去?
: 那应用在其他方面也是分分秒秒的事吧?
l*m
9 楼
现在数学定律大部分是asymptotic, 估计数学家应该ok
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
l*n
12 楼
这种说法完全抹杀了人类的创造力,不可能
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
p*r
14 楼
今天最有意义的事情,
就是看了楼上各位大神的说法。
就是看了楼上各位大神的说法。
g*t
15 楼
我干过AI项目,也干过硬计算项目。在广阔的计算领域。
我觉得AI只是偶尔有用。
说发现了加速大规模暴力搜索的一般方法,
是不是为时过早了?
例如 PDE.
我有个师兄在chevron根据超声波图算在哪儿打
油井成本低。我不太相信ann能有用。
另外更简单的例子,天气预报是军事和商业双重重要的
重要项目。AI能赢现有方法吗?
说AI取代数学家这个可能性我觉得更小。数学家会调整
方向的,研究AI不就完了。既然停机问题无解,这就是
数学家的空间啊。
另外人类会发明新方法,前几年有传费马定理有一步用了特殊的逻辑方法,
实际上和现有公里不一回事。
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
我觉得AI只是偶尔有用。
说发现了加速大规模暴力搜索的一般方法,
是不是为时过早了?
例如 PDE.
我有个师兄在chevron根据超声波图算在哪儿打
油井成本低。我不太相信ann能有用。
另外更简单的例子,天气预报是军事和商业双重重要的
重要项目。AI能赢现有方法吗?
说AI取代数学家这个可能性我觉得更小。数学家会调整
方向的,研究AI不就完了。既然停机问题无解,这就是
数学家的空间啊。
另外人类会发明新方法,前几年有传费马定理有一步用了特殊的逻辑方法,
实际上和现有公里不一回事。
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
w*z
17 楼
很好奇第一个有实用性的,就是和人们日常生活密切相关的应用会是什么?
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
w*g
21 楼
天气预报如果plug-in AI,我觉得可以干的过传统方法。
但是纯AI肯定不行,得有一个人想出来的结合AI的方法。
打油井估计也可以,但我估计着training data可能不够。
这个其实都算不上AI。只是多层线性模型通过
discriminative training暴力拟合通常比基于
物理模型的传统方法(generative model)要好。
【在 g****t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我干过AI项目,也干过硬计算项目。在广阔的计算领域。
: 我觉得AI只是偶尔有用。
: 说发现了加速大规模暴力搜索的一般方法,
: 是不是为时过早了?
: 例如 PDE.
: 我有个师兄在chevron根据超声波图算在哪儿打
: 油井成本低。我不太相信ann能有用。
: 另外更简单的例子,天气预报是军事和商业双重重要的
: 重要项目。AI能赢现有方法吗?
: 说AI取代数学家这个可能性我觉得更小。数学家会调整
但是纯AI肯定不行,得有一个人想出来的结合AI的方法。
打油井估计也可以,但我估计着training data可能不够。
这个其实都算不上AI。只是多层线性模型通过
discriminative training暴力拟合通常比基于
物理模型的传统方法(generative model)要好。
【在 g****t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我干过AI项目,也干过硬计算项目。在广阔的计算领域。
: 我觉得AI只是偶尔有用。
: 说发现了加速大规模暴力搜索的一般方法,
: 是不是为时过早了?
: 例如 PDE.
: 我有个师兄在chevron根据超声波图算在哪儿打
: 油井成本低。我不太相信ann能有用。
: 另外更简单的例子,天气预报是军事和商业双重重要的
: 重要项目。AI能赢现有方法吗?
: 说AI取代数学家这个可能性我觉得更小。数学家会调整
g*t
22 楼
PDE计算流体力学什么的,估计很多人没
有实际经验。就先不谈。
(实际上ai+pde也是一个方向。尽管不主流。)
ODE也不谈。
就说最简单的,2变量f(x,y)=0
代数方程求根,ai方法我不认为能赢正交函数展开算矩阵。
其实谁也不是傻子,要不然矩阵特征根为啥
不用ai,现有的库不都是cholesky之类的方法。
我再举个例子。不用硬件乘法,来实现浮点数乘法,
AI能赢CORDIC吗?
越是基本的问题,
in near future, 越是long way to go。
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 天气预报如果plug-in AI,我觉得可以干的过传统方法。
: 但是纯AI肯定不行,得有一个人想出来的结合AI的方法。
: 打油井估计也可以,但我估计着training data可能不够。
: 这个其实都算不上AI。只是多层线性模型通过
: discriminative training暴力拟合通常比基于
: 物理模型的传统方法(generative model)要好。
有实际经验。就先不谈。
(实际上ai+pde也是一个方向。尽管不主流。)
ODE也不谈。
就说最简单的,2变量f(x,y)=0
代数方程求根,ai方法我不认为能赢正交函数展开算矩阵。
其实谁也不是傻子,要不然矩阵特征根为啥
不用ai,现有的库不都是cholesky之类的方法。
我再举个例子。不用硬件乘法,来实现浮点数乘法,
AI能赢CORDIC吗?
越是基本的问题,
in near future, 越是long way to go。
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 天气预报如果plug-in AI,我觉得可以干的过传统方法。
: 但是纯AI肯定不行,得有一个人想出来的结合AI的方法。
: 打油井估计也可以,但我估计着training data可能不够。
: 这个其实都算不上AI。只是多层线性模型通过
: discriminative training暴力拟合通常比基于
: 物理模型的传统方法(generative model)要好。
w*g
23 楼
你想的大方向不对。AI方法能超越传统方法,无非就是两条
1. 人类对问题本身理解有局限,所以传统model也有局限。
这个包括图像识别,语音识别等等。
2. 虽然传统model可能考虑得比较周全,但是数据noisy,
测量不精确,所以model有等于无。你说的PDE我觉得是这
一类。(其实还是model有局限.)
这两类共同点,就是评测时用的是采集的数据,而不是
拿一个计算结果和另一个计算结果对比。
这种情况下暴力拟合有可能超过传统model。也就是说AI
起的作用其实是abstraction。 方程求根也好,或者是
解释运行python程序也好,AI要能学习会干这个还有很
长的路要走。
【在 g****t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: PDE计算流体力学什么的,估计很多人没
: 有实际经验。就先不谈。
: (实际上ai+pde也是一个方向。尽管不主流。)
: ODE也不谈。
: 就说最简单的,2变量f(x,y)=0
: 代数方程求根,ai方法我不认为能赢正交函数展开算矩阵。
: 其实谁也不是傻子,要不然矩阵特征根为啥
: 不用ai,现有的库不都是cholesky之类的方法。
: 我再举个例子。不用硬件乘法,来实现浮点数乘法,
: AI能赢CORDIC吗?
1. 人类对问题本身理解有局限,所以传统model也有局限。
这个包括图像识别,语音识别等等。
2. 虽然传统model可能考虑得比较周全,但是数据noisy,
测量不精确,所以model有等于无。你说的PDE我觉得是这
一类。(其实还是model有局限.)
这两类共同点,就是评测时用的是采集的数据,而不是
拿一个计算结果和另一个计算结果对比。
这种情况下暴力拟合有可能超过传统model。也就是说AI
起的作用其实是abstraction。 方程求根也好,或者是
解释运行python程序也好,AI要能学习会干这个还有很
长的路要走。
【在 g****t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: PDE计算流体力学什么的,估计很多人没
: 有实际经验。就先不谈。
: (实际上ai+pde也是一个方向。尽管不主流。)
: ODE也不谈。
: 就说最简单的,2变量f(x,y)=0
: 代数方程求根,ai方法我不认为能赢正交函数展开算矩阵。
: 其实谁也不是傻子,要不然矩阵特征根为啥
: 不用ai,现有的库不都是cholesky之类的方法。
: 我再举个例子。不用硬件乘法,来实现浮点数乘法,
: AI能赢CORDIC吗?
g*t
24 楼
(1)
说计算方面。就是给定一个PDE边值问题,
求数值解。ai能赢有限元?
ai连代数方程都有难度。ode,pde恐怕还早。
(2)
model方面,
AI model可能在某些方面超过ODE/PDE/... model,这点我同意.
AI有自己的数据结构.
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 你想的大方向不对。AI方法能超越传统方法,无非就是两条
: 1. 人类对问题本身理解有局限,所以传统model也有局限。
: 这个包括图像识别,语音识别等等。
: 2. 虽然传统model可能考虑得比较周全,但是数据noisy,
: 测量不精确,所以model有等于无。你说的PDE我觉得是这
: 一类。(其实还是model有局限.)
: 这两类共同点,就是评测时用的是采集的数据,而不是
: 拿一个计算结果和另一个计算结果对比。
: 这种情况下暴力拟合有可能超过传统model。也就是说AI
: 起的作用其实是abstraction。 方程求根也好,或者是
说计算方面。就是给定一个PDE边值问题,
求数值解。ai能赢有限元?
ai连代数方程都有难度。ode,pde恐怕还早。
(2)
model方面,
AI model可能在某些方面超过ODE/PDE/... model,这点我同意.
AI有自己的数据结构.
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 你想的大方向不对。AI方法能超越传统方法,无非就是两条
: 1. 人类对问题本身理解有局限,所以传统model也有局限。
: 这个包括图像识别,语音识别等等。
: 2. 虽然传统model可能考虑得比较周全,但是数据noisy,
: 测量不精确,所以model有等于无。你说的PDE我觉得是这
: 一类。(其实还是model有局限.)
: 这两类共同点,就是评测时用的是采集的数据,而不是
: 拿一个计算结果和另一个计算结果对比。
: 这种情况下暴力拟合有可能超过传统model。也就是说AI
: 起的作用其实是abstraction。 方程求根也好,或者是
d*r
25 楼
"""
我个人预测,下一步被攻克的将是数学定理证明。
纯数学家将会先于马公失业。定理证明和下棋一样,
都属于接口定义非常简单明确,但是问题复杂性
很高的那种问题。有一小撮脑子好使的人类非常
推崇这一类问题。AI对这一小撮人将会是非常大
的打击。
"""
同意数学证明可能被AI干翻,特别是那些套路相对固定的.
要 AI 编程其实挺难,因为那个本质上是人给 high-level 的要求,AI 去具体实现.
这个过程可验证性和容错度太低, 除非全面严格定义和升级人类的自然语言 (不是现在
NLP 那种玩法).
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
我个人预测,下一步被攻克的将是数学定理证明。
纯数学家将会先于马公失业。定理证明和下棋一样,
都属于接口定义非常简单明确,但是问题复杂性
很高的那种问题。有一小撮脑子好使的人类非常
推崇这一类问题。AI对这一小撮人将会是非常大
的打击。
"""
同意数学证明可能被AI干翻,特别是那些套路相对固定的.
要 AI 编程其实挺难,因为那个本质上是人给 high-level 的要求,AI 去具体实现.
这个过程可验证性和容错度太低, 除非全面严格定义和升级人类的自然语言 (不是现在
NLP 那种玩法).
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
j*g
26 楼
我觉得AI都还没有完全定义清楚呢,而且AI的定义也非常模糊。
谷歌狗可以下棋横扫全球。不过怎么能让它从0开始build一个像围棋一样的game呢?
至于碾压数学,估计还早。而且就算可以搞数学工作了,还有艺术,法律,社会公平这
些用数学没法解决的问题。
至于自动编程,好像10年前MS就有自动生成编程的程序了。
谷歌狗可以下棋横扫全球。不过怎么能让它从0开始build一个像围棋一样的game呢?
至于碾压数学,估计还早。而且就算可以搞数学工作了,还有艺术,法律,社会公平这
些用数学没法解决的问题。
至于自动编程,好像10年前MS就有自动生成编程的程序了。
g*t
28 楼
数学定理很多就是判断一个程序是不是停机。
例如费马定理等于是判断下面four running indices的
程序是否停机
for x++
for y++
for z++
for n++
IF X^n+Y^n=Z^n THEN STOP
判断一个程序是不是停机,ai够呛
因为分析tool什么的越强,人写的程序就越强
【在 d*******r 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: """
: 我个人预测,下一步被攻克的将是数学定理证明。
: 纯数学家将会先于马公失业。定理证明和下棋一样,
: 都属于接口定义非常简单明确,但是问题复杂性
: 很高的那种问题。有一小撮脑子好使的人类非常
: 推崇这一类问题。AI对这一小撮人将会是非常大
: 的打击。
: """
: 同意数学证明可能被AI干翻,特别是那些套路相对固定的.
: 要 AI 编程其实挺难,因为那个本质上是人给 high-level 的要求,AI 去具体实现.
例如费马定理等于是判断下面four running indices的
程序是否停机
for x++
for y++
for z++
for n++
IF X^n+Y^n=Z^n THEN STOP
判断一个程序是不是停机,ai够呛
因为分析tool什么的越强,人写的程序就越强
【在 d*******r 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: """
: 我个人预测,下一步被攻克的将是数学定理证明。
: 纯数学家将会先于马公失业。定理证明和下棋一样,
: 都属于接口定义非常简单明确,但是问题复杂性
: 很高的那种问题。有一小撮脑子好使的人类非常
: 推崇这一类问题。AI对这一小撮人将会是非常大
: 的打击。
: """
: 同意数学证明可能被AI干翻,特别是那些套路相对固定的.
: 要 AI 编程其实挺难,因为那个本质上是人给 high-level 的要求,AI 去具体实现.
t*n
35 楼
据哥德尔不完全定理,不是所有truth可以被推导出来。
所以电脑还是没戏
电脑只不过把人的推导加快
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
所以电脑还是没戏
电脑只不过把人的推导加快
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
m*s
38 楼
你是只会中学数学么
去瞅一眼费马最后定理和Poincare猜想的证明,像是AI能干的事情么
再说了,就算纯暴力,AI能用来分解质因数?能用来解矩阵方程?
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
去瞅一眼费马最后定理和Poincare猜想的证明,像是AI能干的事情么
再说了,就算纯暴力,AI能用来分解质因数?能用来解矩阵方程?
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
w*g
39 楼
可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
【在 m*********s 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 你是只会中学数学么
: 去瞅一眼费马最后定理和Poincare猜想的证明,像是AI能干的事情么
: 再说了,就算纯暴力,AI能用来分解质因数?能用来解矩阵方程?
这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
【在 m*********s 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 你是只会中学数学么
: 去瞅一眼费马最后定理和Poincare猜想的证明,像是AI能干的事情么
: 再说了,就算纯暴力,AI能用来分解质因数?能用来解矩阵方程?
g*t
40 楼
没有程序可以辨认所有程序是否停机。
不存在一个程序,可以证明所有的数学定理。
这两点是数学事实.
narrow down to如下问题:
‘某类程序有无bug可以用另一个程序来判断“
本身也是数学定理。
这个判断程序还可以考虑有别的判断的判断的程序来判断。
越走越高阶。人类可以继续往前走。
不追求全部解决数学定理。AI解决一部分是完全可以的。
例如数字电路的逻辑验证.
其实可以认为定理证明能力机器早就超过人类了。
但是,例如,机器能解决的那些数字电路的逻辑问题,人类不再认为是
有价值的问题了。价值观掌握在人类手中。机器还是输。
可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
AI
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
: 这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
: 其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
: 在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
: 上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
: 。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
: 从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
不存在一个程序,可以证明所有的数学定理。
这两点是数学事实.
narrow down to如下问题:
‘某类程序有无bug可以用另一个程序来判断“
本身也是数学定理。
这个判断程序还可以考虑有别的判断的判断的程序来判断。
越走越高阶。人类可以继续往前走。
不追求全部解决数学定理。AI解决一部分是完全可以的。
例如数字电路的逻辑验证.
其实可以认为定理证明能力机器早就超过人类了。
但是,例如,机器能解决的那些数字电路的逻辑问题,人类不再认为是
有价值的问题了。价值观掌握在人类手中。机器还是输。
可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
AI
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
: 这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
: 其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
: 在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
: 上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
: 。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
: 从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
m*s
42 楼
果然是在说做中学数学题
AI
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
: 这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
: 其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
: 在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
: 上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
: 。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
: 从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
AI
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 可能用攻克一词不合适。定理证明是np难的,AI改变不了这个现实。我的意思定理证明
: 这事AI将超越人类。下围棋AI也找不出最优解,只是超越了人类而已。定理证明的研究
: 其实早就有了,而且有一些工业界的应用。只是在组合爆炸下走不了几部就完蛋了。AI
: 在定理证明中的作用应该是进行方向性的指导,类似于添辅助线。人类在定理证明这事
: 上其实做得很艰难。之所以目前远超机器是因为有经验,直觉,能看大势一次走一大步
: 。我觉得现在机器已经开始有了这个能力。一开始肯定不会直接解决p vs np,估计会
: 从证奥赛题开始。那个知道能证出来,至少不会陷入悖论停不了机。
j*g
43 楼
现在DL的强是指在确定有解的情况下能够好于暴力搜索的情况下找到解。
不考虑图灵测试的情况下,如果说喂给计算机(1+2+3+...+n),能不能解出n*(n+1)/2?
还是觉得计算机肯定在很多方面会比人强,只是不知道能强多少,还有哪些方面没法比
人类强。
不考虑图灵测试的情况下,如果说喂给计算机(1+2+3+...+n),能不能解出n*(n+1)/2?
还是觉得计算机肯定在很多方面会比人强,只是不知道能强多少,还有哪些方面没法比
人类强。
w*g
44 楼
http://reference.wolfram.com/language/tutorial/SummationOfSeries.html
符号计算其实机器做得很牛了。
guvest说的对,人类可以改价值观。
/2?
【在 j********g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 现在DL的强是指在确定有解的情况下能够好于暴力搜索的情况下找到解。
: 不考虑图灵测试的情况下,如果说喂给计算机(1+2+3+...+n),能不能解出n*(n+1)/2?
: 还是觉得计算机肯定在很多方面会比人强,只是不知道能强多少,还有哪些方面没法比
: 人类强。
符号计算其实机器做得很牛了。
guvest说的对,人类可以改价值观。
/2?
【在 j********g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 现在DL的强是指在确定有解的情况下能够好于暴力搜索的情况下找到解。
: 不考虑图灵测试的情况下,如果说喂给计算机(1+2+3+...+n),能不能解出n*(n+1)/2?
: 还是觉得计算机肯定在很多方面会比人强,只是不知道能强多少,还有哪些方面没法比
: 人类强。
d*r
45 楼
计算机或者人做数学证明,都是用的一种启发式的搜索算法(注意不是穷举).
这种算法往前探索, 需要的所谓“直觉”,其实也是一些好用的pattern的组合.
如果能把问题的描述,pattern的描述(甚至改进)都定义好给计算机,
并且不断改进和修订启发式算法, 计算机为什么不能很好地做数学证明?
这种算法往前探索, 需要的所谓“直觉”,其实也是一些好用的pattern的组合.
如果能把问题的描述,pattern的描述(甚至改进)都定义好给计算机,
并且不断改进和修订启发式算法, 计算机为什么不能很好地做数学证明?
n*w
48 楼
没人知道哪天具有自我意识的ai会造出来。
n*w
58 楼
这次master走出不少人类想不到的棋。珂洁说人类都是错的。
d*r
62 楼
"你得创立新体系,发现新公理体系才能证明那些定理
电脑程序很简单,无法自己发现或加入公理"
你这个观点不一定对啊, 人为了某种需求, 创造新体系,加入新公理,
这个过程不也是人脑为了某目标,运行启发式搜索算法, 找到新套路的结果.
我们并不能说,以后机器就没有这种能力啊.
【在 t*****n 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 不可能
: 歌德尔定理说的是无论你的公理集合是啥,总有不能证明的定理存在。也就是说,无论
: 你给程序的初始值是啥,新体系它也组合不出来。你得创立新体系,发现新公理体系才
: 能证明那些定理
: 电脑程序很简单,无法自己发现或加入公理。
: 而人似乎不同。人有这个能力。而人的能力从何而来,原理是啥完全没有头绪
: 所以现有图灵机基础上的程序产生智能完全不可能。
电脑程序很简单,无法自己发现或加入公理"
你这个观点不一定对啊, 人为了某种需求, 创造新体系,加入新公理,
这个过程不也是人脑为了某目标,运行启发式搜索算法, 找到新套路的结果.
我们并不能说,以后机器就没有这种能力啊.
【在 t*****n 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 不可能
: 歌德尔定理说的是无论你的公理集合是啥,总有不能证明的定理存在。也就是说,无论
: 你给程序的初始值是啥,新体系它也组合不出来。你得创立新体系,发现新公理体系才
: 能证明那些定理
: 电脑程序很简单,无法自己发现或加入公理。
: 而人似乎不同。人有这个能力。而人的能力从何而来,原理是啥完全没有头绪
: 所以现有图灵机基础上的程序产生智能完全不可能。
v*e
71 楼
人会的,也都是你事先告诉他的,或者从这些事先告诉的东西通过有限步推导出来的。
机器可以观察外界本身就是真命题;你给机器安装上眼睛(摄像机),耳朵(麦克风)
,就行了。你只需要记住一件事:人能做的,机器都能做,而且比人做得更好;人不能
做的,机器也能做,比如装上alpha粒子探测仪,装上GPS。你对“理解”不理解而已,
理解不是什么神秘的东西,机器也可以理解。机器也很快能适应未知事物,人能做到的
,马上来到的AI机器都能做到。
【在 t*****n 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 机器会的,都是你事先告诉它的,或者从这些事先告诉的东西通过有限步推导出来的。
: 机器可以观察外界本身就是伪命题。外界有但事先不告诉机器的它永远“理解”不了。
: 人不同。人很快能适应未知事物。
w*g
72 楼
人能做的,机器都能做。机器现在不能做的,将来也能做。
生物进化在宇宙中的意义到人类已经完结了。人类和别的生物
要不了多久就可以退休了。
【在 v*******e 的大作中提到】![](/moin_static193/solenoid/img/up.png)
:
: 人会的,也都是你事先告诉他的,或者从这些事先告诉的东西通过有限步推导出来的。
: 机器可以观察外界本身就是真命题;你给机器安装上眼睛(摄像机),耳朵(麦克风)
: ,就行了。你只需要记住一件事:人能做的,机器都能做,而且比人做得更好;人不能
: 做的,机器也能做,比如装上alpha粒子探测仪,装上GPS。你对“理解”不理解而已,
: 理解不是什么神秘的东西,机器也可以理解。机器也很快能适应未知事物,人能做到的
: ,马上来到的AI机器都能做到。
生物进化在宇宙中的意义到人类已经完结了。人类和别的生物
要不了多久就可以退休了。
【在 v*******e 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
:
: 人会的,也都是你事先告诉他的,或者从这些事先告诉的东西通过有限步推导出来的。
: 机器可以观察外界本身就是真命题;你给机器安装上眼睛(摄像机),耳朵(麦克风)
: ,就行了。你只需要记住一件事:人能做的,机器都能做,而且比人做得更好;人不能
: 做的,机器也能做,比如装上alpha粒子探测仪,装上GPS。你对“理解”不理解而已,
: 理解不是什么神秘的东西,机器也可以理解。机器也很快能适应未知事物,人能做到的
: ,马上来到的AI机器都能做到。
n*t
74 楼
這種事情,很多程度上是東方人沒有比賽,遊戲規則的概念導致的。正常情況下,根本
就不該和這種系統來比,因為不公平。
所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
事實 - 高度重複實現確定的事情,人很少能和機器比。
既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
否則跑短跑的咋不去和汽車比誰跑得快呢?
【在 p**r 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 新闻看得我整个人都不好了,
: 本来过年滑雪滑得很hi的,回家看到新闻。
: 阿尔法狗你为什么要这样子,
: 我蓝瘦,我香菇。
就不該和這種系統來比,因為不公平。
所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
事實 - 高度重複實現確定的事情,人很少能和機器比。
既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
否則跑短跑的咋不去和汽車比誰跑得快呢?
【在 p**r 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 新闻看得我整个人都不好了,
: 本来过年滑雪滑得很hi的,回家看到新闻。
: 阿尔法狗你为什么要这样子,
: 我蓝瘦,我香菇。
x*u
76 楼
乱评论
AlphaGo搜索是一方面,但其对局面的大局观是远胜人类的,这个靠傻算毫无用处,同
样算法弄到1998年也做得到
第一版AlphaGo就是看棋谱学棋感的思路,和职业棋手一样,不过人家第一次碰九段就
灭了九段
【在 n******t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 這種事情,很多程度上是東方人沒有比賽,遊戲規則的概念導致的。正常情況下,根本
: 就不該和這種系統來比,因為不公平。
: 所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
: 事實 - 高度重複實現確定的事情,人很少能和機器比。
: 既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
: ,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
: google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
: 否則跑短跑的咋不去和汽車比誰跑得快呢?
AlphaGo搜索是一方面,但其对局面的大局观是远胜人类的,这个靠傻算毫无用处,同
样算法弄到1998年也做得到
第一版AlphaGo就是看棋谱学棋感的思路,和职业棋手一样,不过人家第一次碰九段就
灭了九段
【在 n******t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 這種事情,很多程度上是東方人沒有比賽,遊戲規則的概念導致的。正常情況下,根本
: 就不該和這種系統來比,因為不公平。
: 所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
: 事實 - 高度重複實現確定的事情,人很少能和機器比。
: 既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
: ,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
: google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
: 否則跑短跑的咋不去和汽車比誰跑得快呢?
f*c
77 楼
话虽然这么说,计算机做数学证明超过人类我估计还得等很多很多年。
在个别领域,如平面几何,计算机在某种程度上已经超过人类了。这个是我国数学家吴
文俊的贡献。我非常肤浅的认识是,吴把平面几何问题翻译成某种代数方程组,然后想
出了一种巧妙的消去法,可以由计算机运行。自然,这个办法做出来的证明人类读起来
是相当费力的。吴有些追随者对此做过改进,对一些问题的证明现在比较可读了。
对于某些特殊的问题,如word problem,即给出一个群的生成元和关系,试判别这个群
是不是平凡的(就是只含单位元的群)。已经有人证明不存在解决此类问题的一般算法
。看看计算机会如何对付此类问题将是非常有意思的。
像Poincare猜想这样的难题,很难想象人工智能会凭空发明出像Ricci Flow这样的东西
。比较现实的是,首先要训练人工智能去读文献。
所以说,我觉得比较现实的目标是用计算机验证某某某的文章是否正确。在顶级杂志上
牛人的文章有本质错误的例子比比皆是,有很多可能大家现在还不知道。IAS的
Veovodsky好像正在搞机器验证证明,但是真正投入实用我估计也得二十多年以后吧。
这个日本的望月新一,2012年夏天宣布证明了abc猜想,可是4年多过去了,有极个别人
号称读懂了,可是大家目前为止还不承认,但也没人找出错误。500多页的手稿愣是悬
在那里;没有结论。要是有个程序,把这玩意扫描进去运行一下,给个结论就好了。不
对拉倒,对的话大家就比较容易下这个狠心去读那500多页。。。
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 人能做的,机器都能做。机器现在不能做的,将来也能做。
: 生物进化在宇宙中的意义到人类已经完结了。人类和别的生物
: 要不了多久就可以退休了。
在个别领域,如平面几何,计算机在某种程度上已经超过人类了。这个是我国数学家吴
文俊的贡献。我非常肤浅的认识是,吴把平面几何问题翻译成某种代数方程组,然后想
出了一种巧妙的消去法,可以由计算机运行。自然,这个办法做出来的证明人类读起来
是相当费力的。吴有些追随者对此做过改进,对一些问题的证明现在比较可读了。
对于某些特殊的问题,如word problem,即给出一个群的生成元和关系,试判别这个群
是不是平凡的(就是只含单位元的群)。已经有人证明不存在解决此类问题的一般算法
。看看计算机会如何对付此类问题将是非常有意思的。
像Poincare猜想这样的难题,很难想象人工智能会凭空发明出像Ricci Flow这样的东西
。比较现实的是,首先要训练人工智能去读文献。
所以说,我觉得比较现实的目标是用计算机验证某某某的文章是否正确。在顶级杂志上
牛人的文章有本质错误的例子比比皆是,有很多可能大家现在还不知道。IAS的
Veovodsky好像正在搞机器验证证明,但是真正投入实用我估计也得二十多年以后吧。
这个日本的望月新一,2012年夏天宣布证明了abc猜想,可是4年多过去了,有极个别人
号称读懂了,可是大家目前为止还不承认,但也没人找出错误。500多页的手稿愣是悬
在那里;没有结论。要是有个程序,把这玩意扫描进去运行一下,给个结论就好了。不
对拉倒,对的话大家就比较容易下这个狠心去读那500多页。。。
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 人能做的,机器都能做。机器现在不能做的,将来也能做。
: 生物进化在宇宙中的意义到人类已经完结了。人类和别的生物
: 要不了多久就可以退休了。
x*u
78 楼
你觉得古今中外,会下围棋的和懂解析数论的哪个多点?
电脑完全可以从头构建整套数论体系,然后输出人类可理解的结果
【在 f*c 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 话虽然这么说,计算机做数学证明超过人类我估计还得等很多很多年。
: 在个别领域,如平面几何,计算机在某种程度上已经超过人类了。这个是我国数学家吴
: 文俊的贡献。我非常肤浅的认识是,吴把平面几何问题翻译成某种代数方程组,然后想
: 出了一种巧妙的消去法,可以由计算机运行。自然,这个办法做出来的证明人类读起来
: 是相当费力的。吴有些追随者对此做过改进,对一些问题的证明现在比较可读了。
: 对于某些特殊的问题,如word problem,即给出一个群的生成元和关系,试判别这个群
: 是不是平凡的(就是只含单位元的群)。已经有人证明不存在解决此类问题的一般算法
: 。看看计算机会如何对付此类问题将是非常有意思的。
: 像Poincare猜想这样的难题,很难想象人工智能会凭空发明出像Ricci Flow这样的东西
: 。比较现实的是,首先要训练人工智能去读文献。
电脑完全可以从头构建整套数论体系,然后输出人类可理解的结果
【在 f*c 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 话虽然这么说,计算机做数学证明超过人类我估计还得等很多很多年。
: 在个别领域,如平面几何,计算机在某种程度上已经超过人类了。这个是我国数学家吴
: 文俊的贡献。我非常肤浅的认识是,吴把平面几何问题翻译成某种代数方程组,然后想
: 出了一种巧妙的消去法,可以由计算机运行。自然,这个办法做出来的证明人类读起来
: 是相当费力的。吴有些追随者对此做过改进,对一些问题的证明现在比较可读了。
: 对于某些特殊的问题,如word problem,即给出一个群的生成元和关系,试判别这个群
: 是不是平凡的(就是只含单位元的群)。已经有人证明不存在解决此类问题的一般算法
: 。看看计算机会如何对付此类问题将是非常有意思的。
: 像Poincare猜想这样的难题,很难想象人工智能会凭空发明出像Ricci Flow这样的东西
: 。比较现实的是,首先要训练人工智能去读文献。
n*t
79 楼
我想指出ai最大的問題,目前為止,不管是alphago,或者是別的ai系統,都沒法做到“
像人”。也就是說不管是deterministic還是stochastically deterministic,都無法實
現人所特有的創造的定義。
舉個現有的例子,現在不管甚麼厲害的ai是無法做到像你的回帖裡面,一上來先扣一頂
帽子的賣萌感和接下來自說自話的磚家感的。這種style,連人自己都無法嚴格描述和定
義其形成機制,AI也沒有辦法。
【在 x****u 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 乱评论
: AlphaGo搜索是一方面,但其对局面的大局观是远胜人类的,这个靠傻算毫无用处,同
: 样算法弄到1998年也做得到
: 第一版AlphaGo就是看棋谱学棋感的思路,和职业棋手一样,不过人家第一次碰九段就
: 灭了九段
像人”。也就是說不管是deterministic還是stochastically deterministic,都無法實
現人所特有的創造的定義。
舉個現有的例子,現在不管甚麼厲害的ai是無法做到像你的回帖裡面,一上來先扣一頂
帽子的賣萌感和接下來自說自話的磚家感的。這種style,連人自己都無法嚴格描述和定
義其形成機制,AI也沒有辦法。
【在 x****u 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 乱评论
: AlphaGo搜索是一方面,但其对局面的大局观是远胜人类的,这个靠傻算毫无用处,同
: 样算法弄到1998年也做得到
: 第一版AlphaGo就是看棋谱学棋感的思路,和职业棋手一样,不过人家第一次碰九段就
: 灭了九段
x*u
80 楼
你孤陋寡闻啊。AI在非逻辑领域完全可以冒充人,可以用来批量生成水军,而且电脑能
有你想不到的创造力。
想试出AI来,就得深入问它逻辑和哲学的问题,不过这类消耗脑细胞的问题真人也不会
回答,你会被直接当sb。
,同
段就
【在 n******t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我想指出ai最大的問題,目前為止,不管是alphago,或者是別的ai系統,都沒法做到“
: 像人”。也就是說不管是deterministic還是stochastically deterministic,都無法實
: 現人所特有的創造的定義。
: 舉個現有的例子,現在不管甚麼厲害的ai是無法做到像你的回帖裡面,一上來先扣一頂
: 帽子的賣萌感和接下來自說自話的磚家感的。這種style,連人自己都無法嚴格描述和定
: 義其形成機制,AI也沒有辦法。
有你想不到的创造力。
想试出AI来,就得深入问它逻辑和哲学的问题,不过这类消耗脑细胞的问题真人也不会
回答,你会被直接当sb。
,同
段就
【在 n******t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我想指出ai最大的問題,目前為止,不管是alphago,或者是別的ai系統,都沒法做到“
: 像人”。也就是說不管是deterministic還是stochastically deterministic,都無法實
: 現人所特有的創造的定義。
: 舉個現有的例子,現在不管甚麼厲害的ai是無法做到像你的回帖裡面,一上來先扣一頂
: 帽子的賣萌感和接下來自說自話的磚家感的。這種style,連人自己都無法嚴格描述和定
: 義其形成機制,AI也沒有辦法。
c*3
86 楼
coding不用”逻辑推理“不行吧,猜谜语不用”联想“不行吧,打哑谜不联系”上下文
“不行吧。
考AI,现在只要考启发式”逻辑推理“(不是预先编程的),”内容联想“(模糊中找
精确),联系内容上下文,推断结果。这些是人的基本生活技能,当然还有举一反三和
很多其它的。
不考这些东西的图灵测试,我感觉是cheating,自己骗自己玩的
【在 g****t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我的意思是懂得哑谜什么的人在过去几年是越来越少的。
: 能问出来机器答不上的问题人群会被逐渐消灭。或者自我改造.
: 我非常肯定。
: 你要是coding天天碰到的问题都是goog,stackoverflow上没人提的,
: 能活多久。。。
: 从历史的角度来看问题的话。说一两个AI解决不了的问题的例子,都能说出来。
: 但能说出来一个AI或者机器差距越来越大的问题吗。
: 或者找出一群人,离机器越来越远吗?我看很难。
:
: 题。
“不行吧。
考AI,现在只要考启发式”逻辑推理“(不是预先编程的),”内容联想“(模糊中找
精确),联系内容上下文,推断结果。这些是人的基本生活技能,当然还有举一反三和
很多其它的。
不考这些东西的图灵测试,我感觉是cheating,自己骗自己玩的
【在 g****t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我的意思是懂得哑谜什么的人在过去几年是越来越少的。
: 能问出来机器答不上的问题人群会被逐渐消灭。或者自我改造.
: 我非常肯定。
: 你要是coding天天碰到的问题都是goog,stackoverflow上没人提的,
: 能活多久。。。
: 从历史的角度来看问题的话。说一两个AI解决不了的问题的例子,都能说出来。
: 但能说出来一个AI或者机器差距越来越大的问题吗。
: 或者找出一群人,离机器越来越远吗?我看很难。
:
: 题。
c*9
95 楼
汽車是两条腿吗? 两个“跑”不是一个概念。
【在 n******t 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 這種事情,很多程度上是東方人沒有比賽,遊戲規則的概念導致的。正常情況下,根本
: 就不該和這種系統來比,因為不公平。
: 所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
: 事實 - 高度重複實現確定的事情,人很少能和機器比。
: 既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
: ,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
: google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
: 否則跑短跑的咋不去和汽車比誰跑得快呢?
【在 n******t 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 這種事情,很多程度上是東方人沒有比賽,遊戲規則的概念導致的。正常情況下,根本
: 就不該和這種系統來比,因為不公平。
: 所謂AlphaGo和人類棋手相比的優勢,仍然是靠傻算算得快,這個道理是很早就知道的
: 事實 - 高度重複實現確定的事情,人很少能和機器比。
: 既然要公平的比較,那google搞一個機器人,從誕生開始起,按照職業棋手入行的規矩
: ,一個人把職業賽事走一邊唄(不許別人幫忙搞定哦),看看能走多遠了。
: google這麼個搞上千臺機器在後面噁心人的廣告手段,在很多別的行業根本就沒人理。
: 否則跑短跑的咋不去和汽車比誰跑得快呢?
c*3
103 楼
所以到最后就是我说的,机器可以把人当成黑盒子,不管人是怎么做的,完全用其它方
法,从头实施一个不同的东西,只要最后结果超过人就可以。
这个方法的问题,就是人里面的各种算法,外面看着貌似简单。但是真的不去反向工程
人是怎么做的,自己从头做一个,就会发现这些算法其实没那么简单。
比如图像识别,人和生物的算法是包括噪声在内,结果基本接近最优(当然不排除有其
它天顶星技术)。还有任何生物的各种运动姿态控制,真的不去反向工程生物的方法,
自己从头做,发现很难达到生物的水平。
这样的算法,慢慢挖,生物里会发现有好多,都是接近最优。每一个,可能都需要花费
大量时间和精力,还是很难接近生物的水准
这上面不能用下棋去评估和人智力的接近程度,因为人脑根本没有下棋的原生的算法。
下棋是人不擅长的,所以作为娱乐。学会下棋和各种千奇百怪的技巧,是人脑灵活性和
适应性的一部分。要比,就应该比这样的适应性。
【在 c*******9 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 你不能精确定义什么是正确,就不能去评判机器到底做的是否正确,机器还觉得人做的
: 不对呢。
: 模糊中找确定机器也能。没精确定义的,机器也能找到最优结果,或者接近最优。
法,从头实施一个不同的东西,只要最后结果超过人就可以。
这个方法的问题,就是人里面的各种算法,外面看着貌似简单。但是真的不去反向工程
人是怎么做的,自己从头做一个,就会发现这些算法其实没那么简单。
比如图像识别,人和生物的算法是包括噪声在内,结果基本接近最优(当然不排除有其
它天顶星技术)。还有任何生物的各种运动姿态控制,真的不去反向工程生物的方法,
自己从头做,发现很难达到生物的水平。
这样的算法,慢慢挖,生物里会发现有好多,都是接近最优。每一个,可能都需要花费
大量时间和精力,还是很难接近生物的水准
这上面不能用下棋去评估和人智力的接近程度,因为人脑根本没有下棋的原生的算法。
下棋是人不擅长的,所以作为娱乐。学会下棋和各种千奇百怪的技巧,是人脑灵活性和
适应性的一部分。要比,就应该比这样的适应性。
【在 c*******9 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 你不能精确定义什么是正确,就不能去评判机器到底做的是否正确,机器还觉得人做的
: 不对呢。
: 模糊中找确定机器也能。没精确定义的,机器也能找到最优结果,或者接近最优。
c*3
107 楼
问题是一个solid证据都没有,我在论坛反这么久进化论,就是看那些学生物的有啥
solid证据。到现在一个都没有发现,基本都是逻辑欺骗,很容易看出来。
最常见的就是用病毒产生抗药性,说这是进化,这是一个典型的逻辑欺骗。因为生物的
多样性,几乎没有一个生物DNA是完全一样的,所以大部分人长相都不一样。所以有抗
药性的病毒早就有了,这是生物多样性导致的,只能证明适者生存。
所谓观察到的进化论证据,基本都是拿生物多样性冒充的。
DNA就和码农代码差不多。真的进化了,产生新的代码模块,内部各种新的模块间逻辑
联系,也需要一并出现。没有出现内部逻辑联系,其实就和自动改代码和设置参数,调
整网页颜色,或者更改桌面模板差不多。Windows 7可以用一个Linux桌面模板,外面看
着完全不一样,内部没区别。
【在 x****u 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 人类进化是假说,生物的进化是实际观测到的现象
solid证据。到现在一个都没有发现,基本都是逻辑欺骗,很容易看出来。
最常见的就是用病毒产生抗药性,说这是进化,这是一个典型的逻辑欺骗。因为生物的
多样性,几乎没有一个生物DNA是完全一样的,所以大部分人长相都不一样。所以有抗
药性的病毒早就有了,这是生物多样性导致的,只能证明适者生存。
所谓观察到的进化论证据,基本都是拿生物多样性冒充的。
DNA就和码农代码差不多。真的进化了,产生新的代码模块,内部各种新的模块间逻辑
联系,也需要一并出现。没有出现内部逻辑联系,其实就和自动改代码和设置参数,调
整网页颜色,或者更改桌面模板差不多。Windows 7可以用一个Linux桌面模板,外面看
着完全不一样,内部没区别。
【在 x****u 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 人类进化是假说,生物的进化是实际观测到的现象
x*u
108 楼
突变加适者生存就是进化论观点,你都承认了还反个屁。
【在 c****3 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 问题是一个solid证据都没有,我在论坛反这么久进化论,就是看那些学生物的有啥
: solid证据。到现在一个都没有发现,基本都是逻辑欺骗,很容易看出来。
: 最常见的就是用病毒产生抗药性,说这是进化,这是一个典型的逻辑欺骗。因为生物的
: 多样性,几乎没有一个生物DNA是完全一样的,所以大部分人长相都不一样。所以有抗
: 药性的病毒早就有了,这是生物多样性导致的,只能证明适者生存。
: 所谓观察到的进化论证据,基本都是拿生物多样性冒充的。
: DNA就和码农代码差不多。真的进化了,产生新的代码模块,内部各种新的模块间逻辑
: 联系,也需要一并出现。没有出现内部逻辑联系,其实就和自动改代码和设置参数,调
: 整网页颜色,或者更改桌面模板差不多。Windows 7可以用一个Linux桌面模板,外面看
: 着完全不一样,内部没区别。
【在 c****3 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 问题是一个solid证据都没有,我在论坛反这么久进化论,就是看那些学生物的有啥
: solid证据。到现在一个都没有发现,基本都是逻辑欺骗,很容易看出来。
: 最常见的就是用病毒产生抗药性,说这是进化,这是一个典型的逻辑欺骗。因为生物的
: 多样性,几乎没有一个生物DNA是完全一样的,所以大部分人长相都不一样。所以有抗
: 药性的病毒早就有了,这是生物多样性导致的,只能证明适者生存。
: 所谓观察到的进化论证据,基本都是拿生物多样性冒充的。
: DNA就和码农代码差不多。真的进化了,产生新的代码模块,内部各种新的模块间逻辑
: 联系,也需要一并出现。没有出现内部逻辑联系,其实就和自动改代码和设置参数,调
: 整网页颜色,或者更改桌面模板差不多。Windows 7可以用一个Linux桌面模板,外面看
: 着完全不一样,内部没区别。
c*3
111 楼
你是上了他们千老的当。我早就仔细观察过,千老的信息,很多都是逻辑有问题,或者
误导,甚至很多都是假的。千老很多logic 101都没有学过,经常放出有大量逻辑漏洞
的信息。
人的相貌不同,是基因复制出错吗?这是生物多样性的一部分,换句话说DNA里面有大
量可调参数,这些不算模块功能代码,参数根据环境或者各种条件变了,就有不同相貌
,特征之类。
所谓病毒抗药性,哪里有啥新功能。抗药性病毒其实就是某些特征和其它病毒不同,这
种早就有了,也不见得是基因出错。
根本不是因为有药才出现的特性,千老故意误导这个次序。这种特性也不是啥新功能,
正好好因此逃过药物作用也是巧合。
所以说产生新功能的证据一个以没有。
【在 x****u 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 你这就没文化了,突变是产生新基因,选择是留下有用的
: 基因复制中出错是客观事实,其中大部分都被淘汰,但极少量会导致新功能出现。一定
: 数量的新功能被选择留下,就有新逻辑,这也是试验观察结果。
: 你这个都承认了,就是承认了进化现象
误导,甚至很多都是假的。千老很多logic 101都没有学过,经常放出有大量逻辑漏洞
的信息。
人的相貌不同,是基因复制出错吗?这是生物多样性的一部分,换句话说DNA里面有大
量可调参数,这些不算模块功能代码,参数根据环境或者各种条件变了,就有不同相貌
,特征之类。
所谓病毒抗药性,哪里有啥新功能。抗药性病毒其实就是某些特征和其它病毒不同,这
种早就有了,也不见得是基因出错。
根本不是因为有药才出现的特性,千老故意误导这个次序。这种特性也不是啥新功能,
正好好因此逃过药物作用也是巧合。
所以说产生新功能的证据一个以没有。
【在 x****u 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 你这就没文化了,突变是产生新基因,选择是留下有用的
: 基因复制中出错是客观事实,其中大部分都被淘汰,但极少量会导致新功能出现。一定
: 数量的新功能被选择留下,就有新逻辑,这也是试验观察结果。
: 你这个都承认了,就是承认了进化现象
b*d
114 楼
展开说说看,怎样用AI来证明哥德巴赫猜想?
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: 我们有生之年应该能看到电脑自动写程序吧。
: 现在engineering的关键是怎么把人类面对的各种稀奇古怪的
: task自动转换成固定的类似下棋的套路。这个并不容易。
: 打个比方,通用计算机take over之前,有各种机器,
: 比如电视机,CD机,电话机,打字机,还有各种专业的
: DSP芯片啥的啥的。现在的人智其实就处于这么一种
: 状态,有图像识别人智,下棋人智,等等。有一个新
: 的任务过来,目前可以达到人类用现有的轮子可以做到
: 超过人类的水平。但是“用轮子”这一步还需要人,
: 虽然这一步已经变得比较容易了。或者说,有了接口
b*d
116 楼
很多数学理论的建立和猜想的证明,都是没有足够数据可以训练的,并且涉及到不同的
无穷。你说的AI搜索只是有限集合里的枚举法,可以说是数学的沧海一粟。AI依此可以
证明类似四色定理单群分类那样的有限类命题,遇到对涉及无限的精确推导目前还看不
到AI有好的办法。再比如说,孪生素数猜想的完全证明在人类这里是可能的,但在目前
AI来说还不可能,除非这猜想能被归结为有限种可逐一验证的情况。
【在 w***g 的大作中提到】![](/moin_static193/solenoid/img/up.png)
: AI证定理不能指哪证哪,因为有的问题不一定能证出来。
: 更可行的做法是在某个特定公里体系内对所有定理的空间
: 或者子空间进行类似广度优先的搜索,搜出来啥是啥。
: AI在搜索中的作用主要是prioritize搜索方向,使得搜索
: 能往fruitful的方向前进。
: 待证明的猜想很多,某个猜想能尝试的方向也很多。
: 最大的问题是大家都不知道哪个猜想能证出来。
: 一个难题被解决,马上立马各种证法就都出来了。
: 求证不是最难。最难的是要压对宝。AI对压宝定方向
: 会有帮助。至于brutal force搜索,机器早超过人类了。
无穷。你说的AI搜索只是有限集合里的枚举法,可以说是数学的沧海一粟。AI依此可以
证明类似四色定理单群分类那样的有限类命题,遇到对涉及无限的精确推导目前还看不
到AI有好的办法。再比如说,孪生素数猜想的完全证明在人类这里是可能的,但在目前
AI来说还不可能,除非这猜想能被归结为有限种可逐一验证的情况。
【在 w***g 的大作中提到】
![](/moin_static193/solenoid/img/up.png)
: AI证定理不能指哪证哪,因为有的问题不一定能证出来。
: 更可行的做法是在某个特定公里体系内对所有定理的空间
: 或者子空间进行类似广度优先的搜索,搜出来啥是啥。
: AI在搜索中的作用主要是prioritize搜索方向,使得搜索
: 能往fruitful的方向前进。
: 待证明的猜想很多,某个猜想能尝试的方向也很多。
: 最大的问题是大家都不知道哪个猜想能证出来。
: 一个难题被解决,马上立马各种证法就都出来了。
: 求证不是最难。最难的是要压对宝。AI对压宝定方向
: 会有帮助。至于brutal force搜索,机器早超过人类了。
相关阅读
请教一个Android的简单HTTP REST编程问题 (转载)angular 的ui.router 配合REST 很强大,感觉今天好虫的偶像来开讲座了。 (转载)XSLT其实就是functional programming学习Haskell的资料rank controls, attention please!想学ios html game development, 请推荐入门的package/toolL家不再用scala了。。if you write doc using MS word in MAC, can you open the doc in pc ?为啥不能用Javascript刷题呢类成员函数调用其它函数error .mdf file unable to attach in Visual Studio 2013 win (转载)Southern California Linux Expo SCALE 13x好像刚刚看到peking2说他做了一个100K tps的node service有什么好的c++ IDE 推荐的吗?C10MC++11 range based for问个问题广大骇老都坐飞机吗,看这个请教client 与server node.js 写的api 如何进行安全验证