ChatGPT 人工智能 GPT4 伦理 生成式 医疗 监管 安全 机器学习 深度学习 神经网络 计算机视觉 强化学习 模型 算法 应用 开发 研究 工具 平台 框架 数据集 训练 部署 安全 合规 培训 投资 LLM,llm AI,ai,Ai 大模型 大语言模型 制图 生图 绘图 文生图 文生视频 生成式AI AGI 世界模型 sora chatGPT,chatgpt,ChatGpt claude openai Llama deepseek midjourney 红熊猫模型 Red panda,panda Stable Diffusion,StableDiffusion,stable DALL- E 3 DALL E DALL Flux,flux 扩散模型 混元大模型 文心一言 通义千问 可灵 Pika PixelDance 豆包 月之暗面 零一万物 阶跃星辰 搜索增强 MiniMax Talkie Agent prompt fastai LangChain TTS 微调 提示词 知识库 智能体
# 热门搜索 #
搜索
陶哲轩用AI证明方程理论,19天进度99.99%!论文即将上线
3387点击    2024-10-14 16:42

AI已完全融入数学家的工作流中。陶哲轩刚刚宣布,最新方程理论项目已完成99.9963%,众包之力外加AI辅助取得了重大成绩。他认为,剩余大约700个让人类头疼的难题,AI或许更有潜力。


AI,已成为菲尔兹奖得主最得心应手的工具。


大约三周前,陶哲轩提出了一个协作项目——


结合专业和业余数学家、自动定理证明器、AI工具,以及证明辅助语言Lean,来描述与4694条幺半群(magmas)方程定理定理相关的蕴含图。



这些定理最多可以使用,四次幺半群运算来表达。


也就是说,需要确定4694条定理之间可能存在4694 * (4694 - 1) = 22028942蕴含的关系真伪。


地址:https://github.com/teorth/equational_theories/blob/main/data/equations.txt


这一项目在9月25日发布当天便启动了,如今,已经紧锣密鼓进行了19天。



刚刚,陶哲轩公布了项目的最新进展:


从已解决原始蕴含关系角度来看,截至目前,项目进度已完成99.9963%。


在需要解决的22028942个蕴含关系中,8178279个被证明为真,13854531个被证明为假,只有826个仍未解决。



而且,项目每一天的进展,他都记录到了个人日志中。



一起看看,陶哲轩如何通过「众包方式」,探索数学新领域。


方程理论项目,进度99.99%


在集合中,有249个蕴含关系推测为假,并且很快就证明了是假的。


出于编译效率的考量,他们并没有在Lean中记录每一个证明,只在其中证明了一个较小的592790个蕴含关系集合,然后通过传递性推导出更广泛的蕴含关系集合。



例如,利用如果方程X蕴含方程Y,方程Y蕴含方程Z,那么方程X蕴含方程Z的事实。


他们还很快利用蕴含图对偶对称性,对其进一步简化。


经过项目志愿者的不懈努力,陶哲轩称现在有了很多出色的可视化工具(尚未完成的),来检查蕴含图的各个部分。


比如,如下这张图描述了方程1491:x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有结果。



陶哲轩将其称之为「Obelix law」。它还有一个伙伴Asterix law,即方程65:x = y ◇ (x ◇ (y ◇ x ))。


如下是,他们正在研究的所有方程定理的表格,以及它们蕴含/被蕴含定理数量。


地址:https://teorth.github.io/equational_theories/implications/


这些界面也在某种程度上与Lean集成。


比如,我们可以点击查看Obelix law蕴含方程359,陶哲轩将其作为题目,让大家进行挑战。他暗示,在Lean中仅用4行就可以完成证明。



在过去的几周里,他还了解到这些定理中,有许多之前已经出现在文献中。


由此,这里编制了这些方程的「导览」。


地址:https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations


例如,除了众所周知的交换律(方程43)、结合律(方程4512)之外,一些方程(方程14、方程29、方程381、方程3722、方程3744)曾出现在一些Putnam数学竞赛中;


方程168定义了一个引人入胜的结构,被称为「中心幺半群」(central groupoid)。特别是,由Evans和Knuth研究过,并且是Knuth-Bendix完成算法的关键灵感来源;




而方程1571则对指数为二的阿贝尔群(abelian groups)进行了分类。



根据Birkhoff完备性定理,如果一个方程定理蕴含另一个,那么它可以通过有限次重写操作来证明。


不过,所需的重写次数可能相当长。


上面提到的1491蕴含359的证明已经相当具有挑战性,需要四到五次重写。


另外,方程1689蕴含方程2的证明,更是极其冗长。尽管如此,标准的自动定理证明器,如Vampire,完全有能力证明绝大多数这些蕴含关系。



更微妙的是反蕴含关系,在这种情况下必须证明定理X不蕴含定理Y。原则上,只需要展示一个遵循X但不遵循Y的幺半群即可。


在很大一部分情况下,他们可以简单地搜索小型有限幺半群——比如两个、三个或四个元素的幺半群——来获得这种反蕴含关系。


但这些并不足够,事实上,他们只知道有些反蕴含关系,只能通过构造无限幺半群来证明。


比如,现在已知的Asterix law不蕴含Obelix law,但所有反例必然是无限的。


有趣的是,已知的构造方法与集合论中著名的forcing技术有一些相似之处,即不断向(部分)幺半群添加「通用」元素,以forcing存在具有某些特定属性的反例。


不过,这里的构造肯定比集合论构造简单得多。


他们还从「线性」幺半群x ◇ y = ax + by构造中取得了有益的进展。这些构造存在于交换环和非交换环中。


与「汇聚」(confluent)方程定理相关的自由幺半群,以及更普遍的具有完整重写系统的定理。


因此,未解决的蕴含关系数量继续稳步减少。


遵循标准GitHub实践,论文很快上线


经过相当繁忙的后端设置和「灭火」(putting out fires)工作后,项目现在运行得相当顺利。


项目在Lean Zulip频道上协调,所有贡献都通过GitHub上的拉取请求(pull request)过程进行,并通过基于问题的GitHub项目进行跟踪。


另外两位维护者Pietro Monticone、Shreyas Srinivas为其提供了宝贵的监督。


与之前的PFR形式化项目相比,这次项目的工作流程遵循了标准的GitHub实践,大致如下:



如果在Zulip讨论过程中,明确需要完成某些特定任务以推进项目(比如,在Lean中形式化讨论线程中已经推导出的蕴含关系证明),就会创建一个「问题」(通常由陶哲轩自己或其他维护者创建),其他贡献者可以「认领」这个问题,单独工作(使用主GitHub仓库的本地副本)。


然后提交「拉取请求」将他们的贡献合并回主仓库。这个请求随后可以由维护者和其他贡献者审查,如果获得批准,就会关闭相关问题。


更广泛地说,他们正努力记录这个设置中的所有过程和经验教训。


这将成为即将发表的关于这个项目的论文的一部分,现正处于初步规划阶段,可能会包括数十位作者。


陶哲轩表示,自己对项目取得的进展非常满意,而且许多最初的期望已经实现。


在科学方面,他们发现了一些新的技术和构造,用来证明一个给定的方程理论不蕴含另一个;他们还发现了一些具有有趣特征的奇特代数结构,如Asterix和Obelix对,是通过系统性搜索方式被发现的。


参与者方面,非常多样化,从各个职业阶段的数学家、计算机科学家,到感兴趣的学生和业余爱好者。


此外,Lean平台在整合人工生成和机器生成的贡献方面表现良好。


机器生成在数量上是迄今为止最大的贡献来源,但许多自动生成往往是基于人类最初在特殊情况下发现的,然后由项目的不同成员进行推广和形式化。


在讨论线程中,他们还进行了许多非正式的数学论证,但这些论证往往会迅速在Lean中形式化,消除了关于正确性的争议就。


进而,研究人员可以转而专注于如何最好地部署各种经过验证的技术,来解决剩余的蕴含关系。


AI并未做出重大贡献


原本,陶哲轩期待看到现代AI工具,能够在项目中做出重大贡献。


但实际上,它们以一种辅助、次要的方式被使用。


比如,通过GitHub Copilot等工具来加速编写Lean证明、LaTeX文档框架、其他软件代码。


此外,他们的几个可视化工具,也主要是使用Claude等大模型共同编写的。



然而,对于解决蕴含关系这一核心任务,更「传统」的自动定理证明器表现更好。


不过,目前剩余的大约700个蕴含关系,大多数不适合使用传统工具来处理。


有几个蕴含关系(特别是涉及Asterix和Obelix那些),已经让人类专家困惑多日。


陶哲轩认为,在解决剩余的、更困难的蕴含关系时,现代AI可能会发挥更重要的作用。


文章来自于“新智元”,作者“桃子 好困”。


关键词: AI , AI数学 , AI科研 , 人工智能
AITNT资源拓展
根据文章内容,系统为您匹配了更有价值的资源信息。内容由AI生成,仅供参考
1
AI工作流

【开源免费】n8n是一个可以自定义工作流的AI项目,它提供了200个工作节点来帮助用户实现工作流的编排。

项目地址:https://github.com/n8n-io/n8n

在线使用:https://n8n.io/(付费)


【开源免费】DB-GPT是一个AI原生数据应用开发框架,它提供开发多模型管理(SMMF)、Text2SQL效果优化、RAG框架以及优化、Multi-Agents框架协作、AWEL(智能体工作流编排)等多种技术能力,让围绕数据库构建大模型应用更简单、更方便。

项目地址:https://github.com/eosphoros-ai/DB-GPT?tab=readme-ov-file



【开源免费】VectorVein是一个不需要任何编程基础,任何人都能用的AI工作流编辑工具。你可以将复杂的工作分解成多个步骤,并通过VectorVein固定并让AI依次完成。VectorVein是字节coze的平替产品。

项目地址:https://github.com/AndersonBY/vector-vein?tab=readme-ov-file

在线使用:https://vectorvein.ai/(付费)

2
AI数据分析

【开源免费】DeepBI是一款AI原生的数据分析平台。DeepBI充分利用大语言模型的能力来探索、查询、可视化和共享来自任何数据源的数据。用户可以使用DeepBI洞察数据并做出数据驱动的决策。

项目地址:https://github.com/DeepInsight-AI/DeepBI?tab=readme-ov-file

本地安装:https://www.deepbi.com/

【开源免费airda(Air Data Agent)是面向数据分析的AI智能体,能够理解数据开发和数据分析需求、根据用户需要让数据可视化。

项目地址:https://github.com/hitsz-ids/airda