- 文献阅读：Solving olympiad geometry without human demonstrations
- 1. 文章简介
- 2. 方法介绍
- 1. Overview
- 2. Symbolic deduce
- 3. Language Model
- 4. 联合使用
- 3. 实验考察 & 结论
- 1. 基础实验考察
- 2. 结果分析
- 3. 样例展示
- 4. 总结 & 思考
- 文献链接：https://www.nature.com/articles/s41586-023-06747-5
- GitHub链接：https://github.com/google-deepmind/alphageometry
1. 文章简介
这篇文章是Google Deepmind在今年1月发表在Nature正刊上的一篇工作，讲道理，ML的文章能发到Nature的正刊上面也是牛得飞起了，所以虽然和工作关系不大，也是忍不住跑过来观摩了一下这个工作。
这篇文章的核心就是提出了一个AlphaGeometry的模型框架，用于挑战奥林匹克竞赛的几何部分，并且获得了堪比高中奥赛金牌的乘积，从方法命名也可以看出，基本对标的就是AlphaGo，AlphaFold等一系列模型了。
不过虽然同为Alpha命名系列，这篇文章中给出的AlphaGeometry模型较之其他几个至少感觉在形式上感觉并不像另外那些那么优雅，因为这并不是一个端到端的模型，而是一个基于搜索的模型生成结果，感觉像是RAG那样像是一个拼凑的系统而不是一个纯粹的技术突破。
但无论如何，这个结果也确实够这篇工作上Nature，我等普通小民负责喊666就行了LOL
2. 方法介绍
下面，我们来具体看一下文中的AlphaGeometry方法到底是怎么做的。
1. Overview
给出文中关于AlphaGeometry的整体方法示意图如下：
上图是AlphaGeometry在一个简单问题和一个复杂问题当中的demo，其中AlphaGeometry的部分主要由上图中的b,c两部分展示，其主要包括一个符号推理系统和一个语言模型，后者用于辅助线的构造等发散性的部分，而前者则进行符号推理等确定性的内容。
下面，我们分别来看一下这两部分的内容。
2. Symbolic deduce
首先，我们来看一下文中的符号推理引擎的部分。
这部分又可以主要分为DD和AR两个部分：
- DD: deductive database
- AR: algebraic reasoning
这两部分的内容主要是来源于以下一些外部文献：
- A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering
- Ye, Z., Chou, S. C. & Gao, X. S. in Proc. Automated Deduction in Geometry: 7th International Workshop, ADG 2008 (eds Sturm, T. & Zengler, C.) 189–195 (Springer, 2011).
文中并没有对其进行过度的展开，只是给出了几个example如下：
3. Language Model
然后，文中关于Language Model的部分，则基本和普通的language model没啥太大的差别，唯一的问题在于说数据的表示和准备。
首先，关于数据的表示，这里主要就是使用latex的符号语言表达。
然后，关于数据的准备，则是使用上一部分当中给出的DD和AR的方式进行的，文中给出这部分内容的过程示意图如下：
文中得到的训练数据的推理长度分布，或者说单条数据的长度分布则如下所示：
而关于模型的训练部分倒是感觉没啥，基本就是一个Language Model而已。
4. 联合使用
具体到使用方面，其实就如上述Fig.1当中所展示的那样，整体过程就是：
- 先使用DD+AR进行符号推导，直至无法推出新的结论
- 使用LM生成辅助线，然后重复符号推理过程
当然，上述过程可能会陷入重复推理以及过于繁复的问题，因此文中还需要对中间过程进行一些剪操作。
3. 实验考察 & 结论
然后，我们来看一下文中对于AlphaGeometry的一些实验考察和分析。
1. 基础实验考察
首先，文中给出的最主要的实验结果就是在奥赛题目上面对AlphaGeometry进行了效果考察，得到结果如下：
可以看到，AlphaGeometry一共答出了25道IMO试题，操过了银牌选手，几乎逼近了金牌选手的水平。
其更为详细的结果可以查看下表获得：
2. 结果分析
然后，文中考察了一下上述IMO竞赛题当中题目的难度（选手的平均得分）和AlphaGeometry做题所使用的推导步数的关系如下：
可以看到：
- 对于较难的问题，AlphaGeometry往往也需要很多的步数来完成题目，但是对于简单的题目，AlphaGeometry使用的步数和题目的难易关系没有可靠的关联关系。
3. 样例展示
最后，文中给出了一个具体的AlphaGeometry的题解如下：
可以看到，AlphaGeometry不但搞定了这道题目，且方法较之人类选手还更好。
4. 总结 & 思考
综上，文中提出了AlphaGeometry，能够在数学奥林匹克的几何问题上达到几乎金牌选手的水平，考虑到LLM在数学问题上的各种拉胯属性（毕竟数学还是推理系统不是模式匹配问题），AlphaGeometry简直强到不行了。
不过具体方法和实现方面，文中的方法倒是没觉得有什么特别大的突破，而且确实和工作差的有点远，所以细节就不打算去追了，有空的时候拿开源代码玩玩看好了。
