日志
点评一下最近用到的AI工具
热度 12
Gemini 3.0 Pro：是最为全面和稳健的，是我在定理证明时用到的主要工具。但是这个工具太有自己的主见了，经常把问题复杂化，而且会陷在某个特定细节中出不来。当然，可能其它工具也有类似的问题，只是我用的比较少，没有发现。
Kimi 2.5：这个工具的能力挺强的，对某些引理的证明可以直接输出完全正确的证明。但是有的时候会犯一些非常微妙的语义错误。它曾给出一个引理，我用了一天时间证完后，才发现这个引理的方向是反的。
DeepSeek V3：这个工具的逻辑推理能力是最强的。曾有一个引理，我问了所有AI，只有DeepSeek给出了内容正确且不超时的证明。为什么说是内容正确呢，因为DeepSeek的原始表述存在语法结构错误，最后在Gemini的帮助下，才完成证明。但是我现在用的网页版还是128K的上下文，无法支持工程级别的定理证明项目，希望能尽早用到百万级别上下文的新版本。
GLM 4.7: 逻辑推理能力一般。最严重的问题是不提供持久性会话，不适合工程级别的项目。
Qwen 3-Max: 复杂的逻辑推理能力欠缺，回答问题是答非所问，也可能是我的提示词用的不好吧。
全部作者的其他最新日志
发表评论 评论 (6 个评论)
- 回复 唐家山
- 目前我是以Gemini为主，间或用Kimi和DeepSeek。等GLM5网页版出来后，我再试试吧。对我来说，工具候选不会太多，最多三家，否则就会影响工程效率。
xiejin77: 可以试试GLM5了。另外国内有一个专门的评测，徐亮搞的superclue
- 回复 smileREGENT
- Gemini 3.0 Pro：目前个人体验觉得最常用最可靠的工具
Kimi：据说长文本阅读能力不错，大型的文本阅读总结会试着用它
DeepSeek V3：中文写作能力私以为最好的，还会拿来和gemini给的结果互相检查印证，gemini思考时间过长的备用牛马
claude:编代码时候用,推荐antigravity的类vs code IDE工具，里面可以白嫖claude的token
- 回复 唐家山
- 我开始只是试试水，用的是DeepSeek，发现还真能用。后来工程的规模上去之后，DeepSeek就不够用了。然后改用Gemini作为主力工具。Kimi也是近期才开始用的。ChatGPT和Claude据说推理很厉害，但是在国内用还是相对麻烦。豆包我还真没用过，之前也没听说豆包的逻辑推理能力强。等以后吧，我可以试试GLM5和豆包。
伯威: 国外LLM样本太少，没有豆包？
