我认为LLM不断复杂地添加各种trick的路线可能不是最快速提升科技的方向，伟大的思路应当是简洁明了的，况且AI学了一大堆没用的知识也没什么意义，虽然可能提高一部分生产力，但我认为真正能引领社会大幅度进步需要靠数学和理论物理突破，或者说我认为AGI之路可能是让AI对数学和物理的理解很深刻以后，再反过来理解这个世界。比如有了很多数学大定理后再创造、理解物理大定律，然后再让他理解新华字典。

最终可能还是要采用多模型、多层架构的思路，也就是LLM提供可能的idea方向，形式化推理用于严谨推导，给出定理。根据公理使用的严谨程度、推理的逻辑深度等，对模型进行划分。

这可能与我之前认为“要让人工智能理解世界”的想法冲突了，我现在认为我以前的想法可能是错的，因为越往后发展，理论物理可能越难给数学提供idea了，更多的是数学引领物理前进，然后再是工程上的巨大进步。

这里讲一讲很久以前萌芽的一些想法，我可能不是第一个想到的，也很有可能不是第一个提出的。这是个类似Alpha Zero的想法，我基本没有看过形式化人工智能的有关前沿论文，只是直觉告诉我这么做可能可以：训练不依靠任何人类数据。

什么定理是“好的定理”？什么定义是“好的定义”？能够解决更多问题的定义、定理就是更好的。事实上可能有很多强大的定理的我们人类没有能力证明，但是却不是很深的逻辑，而是足够抽象：比如牛顿-莱布尼茨公式的逻辑链极深（如果从一阶逻辑开始出，完整地证明)，要定义面积、极限等等东西，但是相对来说更好理解；而伽罗瓦基本定理的逻辑应该是相对于微积分基本定理来说更短的，但是更抽象，对人类来说理解起来很困难，但是这两个定理都是极其重要的。

我的想法是直接从一阶逻辑出发：仅使用必须的那几个逻辑词，随机构造定义和命题和定理。已有的逻辑词和定义、定理构成整个备选词空间。

不过我不清楚用什么神经网络合适，可能可以用transformer，我不是这方面的专家，不过我认为很有可能可行。神经网络具体的连接、节点如何构造，以及用到的学习算法，需要进一步深入思考。其中关键的步骤可能是要强化问题与解决问题所需的逻辑链的连接权重，或者可能要让问题与解决问题的逻辑链中的关键部分在高维向量空间中存在一些映射等方法以让模型学习到证明的思路。

我们可以把已有的“好定理”，“好定义”当作已有的一盘棋局，Alpha Zero给定下一步棋的概率是策略，对应数学证明里面需要用到的“下一组词”（现在想来大概不能直接用下一个词，下一组词是已有词加上已有词的排列组合），还需要专门的模块输出“下一组词”。

具体而言，Alpha Zero是训练一个网络从棋局输出策略，策略是每个动作的概率，也就是每一步棋的概率分布，还输出当前状态的胜率。对应到自动数学定理证明器就是从当前已有的词向量空间（包括逻辑词、已有定义、已有定理）输出当前状态的可能用到的下一组逻辑词、定义、定理的概率，以及当前逻辑链条的“可行性评估”。

评估网络用类似Alpha Zero的方法，用蒙特卡洛树搜索，从当前已有的好逻辑词、好定义、好定理下随机生成大量随机问题。随机生成一些备选定理、定义组合小组，每个小组类似围棋中的“下一步棋”，然后随机进行逻辑推导，以给定推导步数或者时间内的证明成功数量进行“可行性评估”，最后使用类似Alpha Zero的方法进行强化学习。这样的方法可以不断扩充重要定义定理的词库，就好像围棋中下出了一步又一步的妙棋。