STEM版，合并数学，物理，化学，科学，工程，机械。不包括生物、医学相关，和计算机相关内容。
版主： verdelite， TheMatrix
-
Caravel楼主
- 论坛元老
Caravel 的博客
- 帖子互动： 676
- 帖子： 26925
- 注册时间： 2022年 7月 24日 17:21
帖子
由 Caravel楼主 »
你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了
-
（ヅ）
- 论坛支柱
- 帖子互动： 549
- 帖子： 11819
- 注册时间： 2022年 8月 21日 14:20
帖子
由 （ヅ） »
Caravel 写了： 2022年 12月 23日 21:03
你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了
最近研究机器(非AI)证明，挑战还是挺大的
用DL模型的话，怎么给定理证明建模梯度呢？
-
Caravel楼主
- 论坛元老
Caravel 的博客
- 帖子互动： 676
- 帖子： 26925
- 注册时间： 2022年 7月 24日 17:21
帖子
由 Caravel楼主 »
（ヅ） 写了： 2022年 12月 23日 21:18
最近研究机器(非AI)证明，挑战还是挺大的
用DL模型的话，怎么给定理证明建模梯度呢？
按照NLP的路数来，证明里面的逻辑性比自然语言强，应该更容易一点。比如数学的基础就是集合轮，这个东西可以用公理化的方法一路攻击上来
-
（ヅ）
- 论坛支柱
- 帖子互动： 549
- 帖子： 11819
- 注册时间： 2022年 8月 21日 14:20
帖子
由 （ヅ） »
Caravel 写了： 2022年 12月 23日 21:26
按照NLP的路数来，证明里面的逻辑性比自然语言强，应该更容易一点。比如数学的基础就是集合轮，这个东西可以用公理化的方法一路攻击上来
我最近看的机器证明是用SAT和SMT，这些机器对付propositional logic还是很厉害的。问题在于真实的定理，绝大多数是1st order logic.这些工具不太有效
-
tfusion
- 论坛支柱
- 帖子互动： 729
- 帖子： 9537
- 注册时间： 2022年 7月 25日 15:42
帖子
由 tfusion »
Caravel 写了： 2022年 12月 23日 21:03
你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了
证明数学题可以，发现新定理没戏。
-
verdelite
- 论坛元老
- 帖子互动： 1038
- 帖子： 24235
- 注册时间： 2022年 7月 21日 23:33
帖子
由 verdelite »
tfusion 写了： 2022年 12月 23日 21:35
证明数学题可以，发现新定理没戏。
你搞个猜想，让它证，不就行了。
-
tfusion
- 论坛支柱
- 帖子互动： 729
- 帖子： 9537
- 注册时间： 2022年 7月 25日 15:42
帖子
由 tfusion »
verdelite 写了： 2022年 12月 23日 21:36
你搞个猜想，让它证，不就行了。
证不出来。
比如你给个非欧几何的定理，只告诉AI 欧式几何的公理，它证到死都证不出来。
其实哥德尔早已给机器定理证明判了死刑。以上就是一个例子。
-
verdelite
- 论坛元老
- 帖子互动： 1038
- 帖子： 24235
- 注册时间： 2022年 7月 21日 23:33
帖子
由 verdelite »
tfusion 写了： 2022年 12月 23日 21:39
证不出来。
比如你给个非欧几何的定理，只告诉AI 欧式几何的公理，它证到死都证不出来。
其实哥德尔早已给机器定理证明判了死刑。以上就是一个例子。
chatGPT不从欧氏几何公理出发吧。假定它学了网上所有的知识。。。
训练一个数学博士型的chatGPT，其做数学题可能会比全能型的历害很多。
-
Caravel楼主
- 论坛元老
Caravel 的博客
- 帖子互动： 676
- 帖子： 26925
- 注册时间： 2022年 7月 24日 17:21
帖子
由 Caravel楼主 »
verdelite 写了： 2022年 12月 23日 21:42
chatGPT不从欧氏几何公理出发吧。假定它学了网上所有的知识。。。
训练一个数学博士型的chatGPT，其做数学题可能会比全能型的历害很多。
AI可以propose新公理，跳出哥德尔的陷阱
-
tfusion
- 论坛支柱
- 帖子互动： 729
- 帖子： 9537
- 注册时间： 2022年 7月 25日 15:42
帖子
由 tfusion »
Caravel 写了： 2022年 12月 23日 23:17
AI可以propose新公理，跳出哥德尔的陷阱
基于冯诺依曼结构的计算机只知道你告诉它的东西。它想不出你不告诉它的东西。所以它没法propose公理。
-
Caravel楼主
- 论坛元老
Caravel 的博客
- 帖子互动： 676
- 帖子： 26925
- 注册时间： 2022年 7月 24日 17:21
帖子
由 Caravel楼主 »
tfusion 写了： 2022年 12月 23日 23:27
基于冯诺依曼结构的计算机只知道你告诉它的东西。它想不出你不告诉它的东西。所以它没法propose公理。
冯诺依曼结构只是一种计算机结构，没有限制计算机的能力，你要说图灵机还能唬唬人，但是依然不成立
-
tfusion
- 论坛支柱
- 帖子互动： 729
- 帖子： 9537
- 注册时间： 2022年 7月 25日 15:42
帖子
由 tfusion »
Caravel 写了： 2022年 12月 23日 23:35
冯诺依曼结构只是一种计算机结构，没有限制计算机的能力，你要说图灵机还能唬唬人，但是依然不成立
就是图灵鸡。只知道你告诉它的。没法propse新公理
你们这些CS半路出家的人就是对计算机有基本认知问题
-
Caravel楼主
- 论坛元老
Caravel 的博客
- 帖子互动： 676
- 帖子： 26925
- 注册时间： 2022年 7月 24日 17:21
帖子
由 Caravel楼主 »
tfusion 写了： 2022年 12月 23日 23:38
就是图灵鸡。只知道你告诉它的。没法propse新公理
你们这些CS半路出家的人就是对计算机有基本认知问题
你连图灵机说不出来也好意思自称科班？
-
tfusion
- 论坛支柱
- 帖子互动： 729
- 帖子： 9537
- 注册时间： 2022年 7月 25日 15:42
帖子
由 tfusion »
Caravel 写了： 2022年 12月 24日 00:02
你连图灵机说不出来也好意思自称科班？
尼玛这有啥说不出的？我着眼于具体计算机体系结构所以说冯诺依曼结构的
-
verdelite
- 论坛元老
- 帖子互动： 1038
- 帖子： 24235
- 注册时间： 2022年 7月 21日 23:33
帖子
由 verdelite »
tfusion 写了： 2022年 12月 24日 00:05
尼玛这有啥说不出的？我着眼于具体计算机体系结构所以说冯诺依曼结构的
本版专门批评过这种行为：轻易否定一个Idea。当初弃婴就是代表。我自己也有过惨痛教训。
那些学到的基本原理都有成立条件。条件不同可能结论也会不同。
-
FoxMe（令狐）
- 论坛精英
- 帖子互动： 155
- 帖子： 5566
- 注册时间： 2022年 7月 26日 16:46
帖子
由 FoxMe（令狐） »
Caravel 写了： 2022年 12月 23日 21:03
你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了
我也有同感。
-
marclee
- 论坛支柱
- 帖子互动： 557
- 帖子： 9903
- 注册时间： 2022年 7月 22日 01:40
帖子
由 marclee »
计算机（AI）是有可能做出证明题的。很快就会有人用AI来挑战数学猜想，而且会很有成果，最起码会帮助找到思路。
例如像一堂张这样绞尽脑汁找灵感的过程，AI会大派用场，对A I来说就如打败人类围棋高手，就暴力的办法，它就是费点电而已。
这个有多少人断言围棋AI不可能赢，但是AI赢了大部分人才打脸，才明白这样也行！
现在AI做数学缺的是做数学团队做AI而已。
这个领域马上会有人搞，谁先搞谁先出成绩，各个领域的诺奖以后要看借助AI的智力是否还发给诺奖。
-
catoh（亲氧化猫）
- 正式会员
- 帖子互动： 0
- 帖子： 27
- 注册时间： 2022年 10月 10日 19:56
帖子
由 catoh（亲氧化猫） »
哥德尔定理说的是，你不能证明存在一个，或者做出一个定理证明AI，它的证明都是对的。
哥德尔不排除你可以做出定理证明AI，但是你必须一个一个读AI的证明来验证每一个定理的正确性
也就是说，这个AI就像一个数学家。所以楼主说的事情是很有可能发生的！
-
marclee
- 论坛支柱
- 帖子互动： 557
- 帖子： 9903
- 注册时间： 2022年 7月 22日 01:40
帖子
由 marclee »
catoh 写了： 2022年 12月 24日 10:18
哥德尔定理说的是，你不能证明存在一个，或者做出一个定理证明AI，它的证明都是对的。
哥德尔不排除你可以做出定理证明AI，但是你必须一个一个读AI的证明来验证每一个定理的正确性
也就是说，这个AI就像一个数学家。所以楼主说的事情是很有可能发生的！
它暴力起来，一般数学家不是对手，无论是知识面广度深度再加上速度遍历所有可能（所谓的灵感也就是人类没能力全搞一遍各种可能性而已，AI只要搞的可能性多，数量级的多，人类就只有膜拜的份），那它就是数学家。一般数学家望尘莫及。
就如人类所谓的围棋高手对AI一样。
上次由 marclee 在 2022年 12月 24日 12:07 修改。
