智源社区 05月15日 20:44
陶哲轩携AI再战数学!o4-mini秒怂弃赛,Claude 20分钟通关
index_new5.html
../../../zaker_core/zaker_tpl_static/wap/tpl_guoji1.html

 

陶哲轩通过实验,探讨了AI工具在形式化数学证明中的应用。他测试了Claude和o4-mini在将代数蕴含转化为Lean代码上的表现,并深入分析了自动化工具在不同尺度上的效率。实验结果显示,过度依赖自动化工具可能导致对证明整体结构的理解不足,最优的自动化水平需要在人工干预和工具辅助之间取得平衡,以实现更灵活、更具启发性的数学形式化。

💡 实验目标:陶哲轩旨在测试AI工具(Claude和o4-mini)将人类可读的数学证明转化为Lean代码的能力,并考察其在证明助手中编译的效果。

🤖 Claude的表现:Claude在单行代码生成方面表现出色,但未能正确处理自然数起始问题和对称性问题,需要人工干预修复错误,最终在20分钟内完成了形式化。

🤔 o4-mini的谨慎:o4-mini在识别问题上较为谨慎,但选择了放弃,未能完成形式化证明。两者都遇到了类似对称性问题,表明LLM在处理数学逻辑细微差别时存在局限。

⚖️ 效率与理解的平衡:陶哲轩强调,过度依赖自动化工具可能牺牲对证明结构的整体理解,最优的自动化水平应介于0%和100%之间,在减少重复性工作的同时,保留人工干预,以加深对任务结构的理解。

编辑:桃子 

3天后,陶哲轩YouTube视频二更来了。

上一次,他使用GitHub Copilot(基于GPT-4),成功在33分钟内完成一页非形式化证明。

这次,他尝试了一种更短、更概念化的证明版本,并测试Claude、o4-mini能否基于之前的非形式和形式证明,生成类似的形式化代码。

实验的核心是,在Lean中形式化同一个代数蕴含的证明。

此外,他还发文深入剖析了,自动化工具不同尺度上的效率表现,以及自动化与人工干预之间的微妙平衡。


Claude 20分完成,o4-mini弃题


最新实验中,陶哲轩围绕一个代数蕴含展开(algebraic implication):证明方程1689蕴含方程2。

录制前,他已进行了一次测试。

这里直接在Claude/o4-mini中粘贴prompt,然后附上非形式证明、形式证明、方程三个附件。

接下来,一起看看这两个模型具体表现如何?

Claude

实验中,Claude整体表现出色,能够快速将非形式证明的单行,转化为看似合理的Lean代码。

它生成了与之前形式化证明结构相似的代码,并成功定义了关键的幂函数。

然而,陶哲轩创建一个新文件,在Claude编译过程中,却发现错误——它假设从自然数1开始,而Lean中的自然数从0开始。

另外,Claude未能正确处理方程的对称性,比如x=(y·x)·z,导致了证明逻辑出现偏差。

尽管单行代码生成高效,但缺乏对整体结构的理解,使得错误诊断和修复变得困难。

通过人工干预,陶哲轩修复了这些问题,最终在20分钟内完成形式化。

o4-mini

相比之下,o4-mini表现得更为谨慎。

与Claude类似,o4-mini一上来也创建了一个幂函数,却胜过前者。

它正确识别了幂函数定义中的问题,magmas中没有单位元1,因此不能简单假设0=>x设置为等于1。

然而,o4-mini在关键时刻却选择了「放弃」,仅生成了部分证明代码,并在修复步骤中输出「抱歉」。

最终,o4-mini未能完成形式化证明。

陶哲轩表示,它的谨慎策略虽避免了严重错误,但也限制了其在复杂任务中的实用性。

有趣的是,o4-mini和Claude同样遇到了类似对称性问题,表明LLM在处理数学逻辑的细微差别时,存在共同的局限。

总之,整个实验目标看似简单,即让AI工具将人类可读的证明转化为Lean代码,并在证明助手中成功编译。

然而,陶哲轩的实验揭示了自动化的复杂性,尤其是在效率和正确性之间的平衡。


100%过度自动化,毁掉数学未来?


在长达一周的自动形式化实验中,陶哲轩得出了一个教训——

即使纯粹专注于效率,仅接受在证明助手中实际编译并产生预期结果的形式化,衡量效率的尺度现在也产生了显著差异。

在形式化数学证明过程中,效率可以从以下四个不同尺度衡量。

1. 单形式化:加快证明中任意一行的形式化

2. 单一引理形式化:加快形式化证明中的任一引理

3. 单一证明形式化:加快形式化定理的任一证明

4. 「整个教科书」形式化:加快形式化整个教科书的成果

每个尺度看似都在指向同一个目标:更快地完成形式化。然而,实际操作中,这些尺度的优化策略可能互相冲突。

陶哲轩以自己最近的实验为例,尝试用一些自动化工具,加速形式化过程。

我意识到,许多当前的自动化工具可以在其中一个尺度上加速形式化,但出乎意料的是,过度依赖此类工具可能会削弱在其他尺度上形式化的能力。

比如,依赖类型匹配工具canonical在「单行形式化」(尺度1)的任务中,表现出色。

它能快速解析,并生成正确的代码,在此过程中,陶哲轩几乎无需手动干预。

然而,当过于依赖canonical,盲目接受它对某一步的解析,并迅速进入下一步时,他发现自己逐渐失去了对证明整体结构的把握。

这导致了,在「引理形式化」(尺度2)上,诊断和修复错误变得更加困难,因为到了此刻,陶哲轩对证明步骤之间的联系缺乏深入的理解。

有趣的是,修复这些错误的过程,却让陶哲轩本人受益匪浅。

通过手动检查和调整,他逐渐理解了引理之间的作用,这反过来提升了其解决「单一证明形式化」(尺度3)任务的能力。

这种「意外收获」让他意识到,完全依赖自动化工具,可能会让自己错过对证明结构的深刻洞察,而这些这些洞察在更大尺度上至关重要。

陶哲轩认为结论是,「最优的自动化水平并不是100%,而是介于0%和100%之间的某个值」。

从每个尺度上来说,自动化工具应该被用来减少重复性的繁琐工作,但同时必须保留足够的人为干预,以审查和修复局部问题,从加深人类对所有尺度任务结构的理解。

更广义地看,如果我们100%依赖自动化工具解决所有任务,可能会失去对任务空间的熟悉度。

在面对中等,甚至高难度任务时,自动化工具可靠性下降,我们却可能因缺乏经验而束手无策。

值得警醒的是,过度聚焦于单一尺度的效率优化,可能会违背数学形式化的长远目标。

其终极目标,不仅是生成在证明助手中编译的代码,更是要创造一个灵活、可用、不断演变且富有启发性的形式化数学语料库。

参考资料:
https://mathstodon.xyz/@tao/114498906474280949
https://mathstodon.xyz/@tao/114501119350851281


内容中包含的图片若涉及版权问题,请及时与我们联系删除

Fish AI Reader

Fish AI Reader

AI辅助创作,多种专业模板,深度分析,高质量内容生成。从观点提取到深度思考,FishAI为您提供全方位的创作支持。新版本引入自定义参数,让您的创作更加个性化和精准。

FishAI

FishAI

鱼阅,AI 时代的下一个智能信息助手,助你摆脱信息焦虑

联系邮箱 441953276@qq.com

相关标签

陶哲轩 AI 数学证明 形式化 自动化
相关文章