晚上好，我是蓝色蒜头。
2024 年 2 月 2 号，短播客第 79 期
今天这一期有一些门槛
涉及的到的计算机领域概念可能会比较多
确实有一定的了解难度
没有足够的时间做成一篇更浅的科普
只能尽可能不讲太复杂
就在上个月 17 号，谷歌在 Nature 发布了一篇论文
介绍了最新的一个模型 Alpha Geometry
可以简单翻译为阿尔法几何
什么都叫阿尔法，是他们从阿尔法狗就开始的习惯了
毕竟公司现在也叫 alphabet
这篇论文的中心思想
是讲如何利用人工智能技术去证明平面几何证明题
也就是欧几里得几何的那些证明题
大家应该都非常熟悉，是我们每个人高考的时候都做过的那些题目
当然，如果按照数学竞赛的标准，平面几何证明题会很难
而用计算机去证明各种不管是简单的还是难的平面几何题
就是一个计算机和数学交叉的领域下比较重要的研究
现在以各种角度讲这篇论文的文章或视频有不少
蒜头在这里给一些我的个人理解体会角度
首先说一下背景，其实几何定理的机器证明
国际先驱是我国的吴文俊院士
早在上个世纪 70 年代，可以说我国大陆地区刚出现仅有的计算机技术研究可能性时
吴文俊就开始做几何定理证明算法的研究
并且在 1978 年提出系统性的吴方法
很多人经常普遍认为我国不重视没有经济利益，不能快速转化为实用技术的研究课题
这种说法是错的，实际上早在 2000 年的第一次中国国家科学技术奖
就给了两个人，一个是吴文俊，一个是袁隆平
袁隆平老先生大家可能很了解，吴文俊可能就没有太多人知道
至少第一次的这个奖项上，这两位是等同的
这两位前辈现在都已离开我们
这里对他们表示致敬与缅怀
后来的所有几何定理的机器证明思路，也就是计算机算法思路
都是在吴文俊的思路框架基础上构建的，包括谷歌的这篇论文也不例外
简单概括一下 吴文俊方法的大致思路
首先，把所有的平面几何问题，尝试以一套符号系统进行表达
去描述平面上的点线连接关系
这样，把几何证明题的命题，和要证明的结论都转化为符号式的描述
或者也可以叫代数式的描述
然后，根据这套符号系统描述建立的表达式
进行表达式的转化运算
大家应该都熟悉如何解方程或者解代数问题
代数问题里就会利用各种手段把表达式进行化简
用各种消元法处理原来的表达式
还记得高中数学内容的朋友都不会难理解
吴方法的手段类似，虽然他的表达式系统不能单纯理解为常见的多项式方程
但是在消元化简的逻辑上是相似的
所以，先将平面几何问题转化为符号表达式
再对这个符号表达式进行消元化简
再根据化简后的表达式变形成符合要证明的结论的表达式
这样就相当于完成了证明
而计算机算法要做的
就是去进行符号表达式的化简和变形
我们把化简前后，变形前后的表达式
都看成同一个对象的不同状态
算法其实就是在对象的状态转换树上做遍历搜索
逐步来缩小解空间，最终达成证明
或者也可能由于解空间过大，状态过多，而无法在短时间内完成证明
上面这段计算 机术语比较多
我也不知道怎么更简化，还请见谅
吴方法 1978 年提出，到今天为止，还是非常优秀的算法实践
后来被做过若干次的优化改进，但是大框架变化不大
后来的一个重要改进是演绎数据库 Deductive Database 简称 DD
简单来说，就是基于现有的命题条件，根据人为设计好的一些规则
来对现有数据进行不断的演绎变化，来形成新的数据
和吴方法结合，其实就是扩充了表达式变形的可能性
可以更好的去优化算法的搜索过程
从另一个角度来说，吴方法和演绎数据库都是符号主义的人工智能领域的重要理论
人工智能长期以来分为符号主义和连接主义
具体解释起来很繁琐，这里简单概括其区别
符号主义尝试把一切知识转化为符号表示，然后以各种推理规则来得出结论
连接主义会基于统计学来归纳提取信息模式，建立其某种潜在的相关性，基于这种相关性去得出结论
现在这一轮人工智能的崛起，大规模神经网络的各种成果
就是基于连接主义，神经网络就是用特定的方法，形成许多模拟神经节点联系的多层关联，每层关联包括一些统计学意义上的模式信息，最终形成一个可以处理许多问题的包含巨量节点的模型
常说的深度学习，这里的深度就是指的节点和层次特别多，从而量变导致质变
到现在，大模型在一些场合的成果，已经有了非常好的
所有人都非常容易理解到的效果
例如绘画模型，以及大语言模型
以上是一些铺垫
接下来说谷歌的这篇论文里做了什么事情
前面说的吴方法，以及根据吴方法改进的算法，思路非常优秀
但是面对一些比较复杂的问题，可能在较短的可接受的时间内找不到解
如果我们从人类证明几何题的思维角度来说
它有一个比较大的局限是，不会在证明过程中添加辅助线
添加辅助线比较难，因为加辅助线的方式很多，几乎可以说是无穷无尽
没有一套标准化的策略来给几何证明题的命题条件添加辅助线
很多证明题，加了合适的辅助线
证明会变得很简洁
是一种非常好的化简方法
而吴方法中间没有找到采用这种辅助线化简的可行方法
谷歌团队因此有了一个想法
如果我们这里用深度学习的方法，把很多添加辅助线的证明过程作为训练数据
来训练出一个模型，然后把证明题的命题输入这个模型
让模型帮助我们添加辅助线，然后再用原来的方法处理
是否可以做到更好的证明呢
他们尝试了把现有的可以收集到的证明过程，做了规范化表达之后
作为训练数据来进行模型训练
用这样得到的模型去完成添加辅助线的任务
由于数据数量有限
团队首先采用了基于 GPT4 为基础，进行微调训练的做法
实际效果不理想，因为 GPT 模型里可能包括很多非几何方面的内容
以及一些比较常见的通用教学内容，不能做到很好的数据质量
所以只能单独去专门训练这样一个模型
但麻烦的问题在于，如果要训练这样的专用模型，就需要大量的规范化表示的几何证明过程
每个过程包括命题，结论和证明步骤
用现有的比较容易找到的数据
由于数据有限，构建不了比较大的模型
这种问题不像人脸识别，车辆识别，每天都会产生海量的拍照数据
几乎每个专门的领域，都会面临类似的数据不足
因此谷歌团队在这篇论文里
采用了一个不同的思路来构建训练数据
大概概括如下
首先编写随机算法，生成数亿个随机的组合平面几何图形
然后，用前面说的演绎数据库 DD 的方法
以一些人为策略，对这些随机图形组合进行各种推导
通过这些推导，生成很多结论
这样对于每个结论，都可以通过推导演绎过程，对应回那些随机的组合图形
这样就有了人为产生的「命题、结论、证明步骤」信息
接下来是重要的一点
去分析 每个过程，在每个这样随机生成的证明过程里
去对比命题和结论，如果出现了某个几何要素，例如一个线段，一个圆，和结论没有关系
但是却参与了证明过程，那么就认为这个要素是辅助线
这样，就得到了大量的利用了辅助线去完成证明的过程
当然以上过程都可以通过计算机程序来完成
进一步再利用程序进行去重复的处理
最后得到了一亿个证明过程
其中有 9% 的证明过程包含了辅助线
接下来对模型进行训练
用全部一亿个过程对模型进行预训练
然后再用 9% 的包含辅助线的过程对模型进行微调训练
在实际的证明过程里
如果出现传统方法无法做到的证明
就调用这个训练好的模型，尝试添加辅助线
针对添加了辅助线的图形，再次尝试进行证明
直到完成证明或者计算超时
他们使用了四个 nvidia V100 作为运行环境来进行并行计算
成本折合人民币二十几万
超时时间则设为一个半小时
而训练过程用到的设备成本则更大
大概有 10 万个 CPU 核心
通过最终实现的完整算法 + 模型取得了比较好的效果
以 2000 到 2022 的 30 个国际奥林匹克竞赛几何问题来测试
之前的最好传统方法可以解出十几个问题
而 Alpha Geometry 可以解出 25 个问题
至少在平面几何证明这一点上，算是达到了人类的奥林匹克竞赛选手水准
以上说的非常简化
实际的论文细节要比这个多得多，每一步的具体数学表达和编程处理手段也很复杂
需要花时间去看
但了解了上述过程，基本上也就了解了这个论文的主干
蒜头在第 70 期播客里就提到过
早在 2021 年，我在一些严肃项目上
和人争论过是否要在特定智能系统里引入传统的符号式推理机
更直白的说，是否要在现有的基于连接主义的大模型构建的解决方案里
引入符号主义的一些运算能力，来整合成整个智能系统
其实这几年我个人的观点一直都是，应该引入
之前我的想法是，把推理机这样的组成部分，作为多智能体的一部分
以一个智能体或者一个可调用函数的形式加入到整个的集成体系里
谷歌在这篇论文里的 Alpha Geometry 就更进一步
直接利用符号式的方法，去生成训练数据，从而完成专门模型的训练
对我目前的思路算是一个非常好的补充
也值得进一步尝试
不过，模型训练的成本比较高
作为外挂智能体的方式，成本则相对低
但无论如何，也是印证了我的观点
就是仅靠现在的大模型，其实能解决的具体领域问题比较有限
最主要的瓶颈就是领域性的数据其实并没有那么多，覆盖不了这个领域的完备的知识
去年有一种 GPT 的使用方法，被很多媒体吹捧过一段时间
就是有人开发了一套集成方案，利用向量数据库 + 大语言模型
实现把一些现有资料拆分后，存入向量数据库，再利用大语言模型 + 向量检索
来实现一个针对输入资料的对话机器人
比如说，我输入一本某教程，就可以形成一个根据该教程进行答疑的机器人
输入三国演义，就可以形成一个回答三国演义中问题的机器人
这种做法有一定的效果，但是不可能像媒体说的那么好
游戏媒体 IGN 在去年也用类似方法做了所谓的游戏攻略机器人，效果非常一般
我个人也用一些小说和游戏数据资料做了尝试
结论也是效果一般
其实这些实践我在去年比较早的播客里
大概是 21 到 24 期
以及年底的零散若干期，都分别讲过
其最大的问题就是，仅仅输入一本书或者少量资料
还并不足以形成实质的知识
举一个简单的例子
老张是小张的父亲
小张是小小张的父亲
仅仅输入 这两句话
其实用上述方法无法直接得出老张是小小张的爷爷
这个结论
因为上述内容中并不包含爷爷这个词以及关系描述
所谓向量数据库只是用各种方式进行信息分解和匹配
而「父亲的父亲是爷爷」这个是一个额外知识
很多书如果缺失了这些额外知识，基础知识
仅凭这本书无法满足一个专门智能系统的构建
所以，还是需要做两项工作，第一，在大模型中补充更多常识
但更重要的是第二，补充更多的由推理演绎形成的知识
比如上面的例子，父亲的父亲是爷爷就可以作为一个推理规则
得出老张是小小张的爷爷这样一个原文并不包括的结论
换言之，根据已有信息
加上推理演绎规则，可以得出很多的新结论
就像 Alpha Geometry 的训练过程里
通过对原始图形的演绎，产生了新的证明结论，对训练数据的完备性有了很好的补充
目前围绕知识表示和推理演绎的计算机实践
包括知识图谱，推理机，本体等相关概念
目前并不应该舍弃，而是要尝试进一步的去和大模型整合
符号主义还是要和连接主义共同使用
来满足当下的一些具体场景
当然这只是一个思维方式的 开头
具体如何整合，是在训练过程里整合还是通过外挂智能体整合
还是有之后的其他方式，需要各方面的实践
而且，平面几何问题是特定的非常规范的问题
可以借助吴方法的设计做很规范的表达
但其他一些领域的问题，可能就没有办法做严谨到代数程度的符号式表达
因此，谷歌的这个论文中的方法，对于各种领域的探索有启示
但并不能直接运用，甚至连非平面几何的其他数学问题求解，目前也不能直接运用
这个论文是个很重要的思维启示，以及中间的许多建模方法可以参考
但是要把他说成多么大的爆炸突破
以及谷歌在 AI 领域再度领先之类
都言过其实，属于媒体的议题设置，大家一定要警惕，一定要理性思考
至少这两天我就已经看到过大肆渲染 AI 做奥赛题，超越人类
之类的无聊标题，正文不对论文本身和计算科学做任何探讨
只是渲染奥赛题多难，一般人不喜欢数学所以差距多大，AI 多厉害，人多渺小之类
我觉得极其没有意思
为什么蒜头总是隔几期播客就要喷媒体议题设置
是我不想只讲电子游戏吗
是我不想只讲计算机科学吗
这些垃圾信息泛滥，把公众话题都搞烂了
让我怎么好好讲，只能经常的骂一骂
这一期的字数比预期的多
概念也比较晦涩，不太适合讲更长了
之后的播客我会把一些小点掰碎放在更日常的讨论里
或者找到一些更直白易懂的说法
今天就聊到这里，离春节还有最后几个工作日
我正在考虑春节的播客更新计划
但至少明天休息
祝大家进步，春节前过得顺利，再见！