日志

三“英”战吕布

热度 19已有 344 次阅读2026-2-14 19:17

最近用AI做定理证明太投入，一不小心把Gemini的额度用完了。趁着等待Gemini重置额度的时间，我把正在证的一个证明分别在多个AI上面试了一下。办法很简单，初始是完全相同的问题，然后哪个AI有了反馈后，就跟哪个AI交流。上个日志坛友们推荐了豆包和GLM5。所以候选工具是4个，分别是DeepSeek V3（百万上下文），KIMI 2.5，GLM 5和豆包。调研后发现豆包就没有上传项目文件的功能，直接出局。这样就形成了三英战吕布的格局。

由于类似的问题之前用Gemini解决过，所以主要是看DS，KIMI和GLM是否能尽快给出正确的证明。我要证的是一个复杂递归函数的函数步进的等效性。由于这个递归函数特别复杂，那些高度自动化的单步证明策略是一定会超时的。所以在一开始，我就告诉这些AI不能用单步证明策略，只能用逐步拆解的手工证明方法。DS和KIMI都听明白了，但是GLM的第一次回答还是选择了单步证明策略，在我纠正后，它后面也开始输出逐步拆解的证明方案。

在最初的几轮，这些AI都试图对一个特别复杂的单一待证目标进行各种变形和优化，但是无一例外证不出来，不是超时就是证错。GLM在两轮之后就消耗完了我套餐的所有token，率先出局。

第三轮KIMI最先想出来把单一待证目标拆解成多个小目标，然后分别证明的方案。但是它在消解掉多数子目标后，对于还剩下的两个子目标一直没消解掉，直至我的套餐额度用完。DS在我把KIMI的方案喂给它后，明确提示对单一目标进行拆解成多个目标。它用了七轮，最后给出了一个合格的证明方案。

补充：今天上午用Gemini证明一个类似复杂度的步进归纳问题，发现Gemini又开始打转。我仔细看了Gemini之前解决的那个问题，复杂度比较低，可以用传统方式解决，所以Gemini的创造力不像我之前评估的那么高。最后我是把DS证明的那个问题的解决方案喂给Gemini，Gemini经过一轮就搞定了新的证明。考虑到是KIMI第一个想到了把单一目标拆解成多个小目标的方案，在此给KIMI点个赞。