5月2日

跨越300多年的接力：受陶哲轩启发，数学家决定用AI形式化费马大定理的证明

数学家Kevin Buzzard宣布启动费马大定理（FLT）的证明形式化项目，使用交互式定理证明器Lean。FLT由17世纪数学家皮耶·德·费马提出，直到1995年由Andrew Wiles证明。Buzzard的动机是将现代代数数论的关键概念形式化，以便计算机能更好地理解并辅助数学研究。项目已获EPSRC资助，计划将FLT简化为1980年代末已知的数学声明，并在Lean社区中众包完成。参与者可通过在线教科书《Mathematics in Lean》学习所需知识，并在Lean Zulip chat上协作。项目进展可在专用网页查看。来源：微信公众号【机器之心】

Transformer要变Kansformer？用了几十年的MLP迎来挑战者KAN

多层感知器（MLP）作为深度学习的基础构件，尽管被广泛使用，但存在可解释性差和参数消耗大等缺陷。最近，一种名为Kolmogorov-Arnold Networks（KAN）的新型网络结构被提出，作为MLP的替代选择。KAN的设计灵感来源于Kolmogorov-Arnold表示定理，通过在网络的边（权重）上放置可学习的激活函数，而非传统MLP在节点上放置固定激活函数的方式。KAN在准确性和可解释性方面显示出对MLP的显著改进，尤其在处理高维函数时。此外，KAN还具有持续学习和避免灾难性遗忘的能力。尽管KAN的训练速度较慢，但研究者认为这是一个可以通过工程优化解决的问题。未来，KAN有望在AI+科学领域发挥重要作用，甚至可能被集成到Transformer等架构中，形成”Kansformer”。来源：微信公众号【机器之心】

Meta 联合纽约大学和华盛顿大学提出MetaCLIP，带你揭开CLIP的高质量数据之谜

Meta联合纽约大学和华盛顿大学提出了MetaCLIP，一种新的数据算法，旨在揭开CLIP高质量数据的秘诀。MetaCLIP通过元数据字符串匹配和平衡数据分布来生成高质量的训练数据，无需依赖已训练的CLIP模型。该算法在CommonCrawl上运行，显著提高了数据质量，同时保持了长尾数据的信号。实验结果显示，MetaCLIP在400M训练数据上达到了70.8%的零样本ImageNet分类精度，证明了其数据质量对模型性能的重要性。来源：微信公众号【机器之心】

Claude iOS版本突然推出！11MB大小，体验丝滑，网友呼吁语音功能快上线

Anthropic公司近日推出了Claude的iOS应用，大小仅为11MB，用户可以在移动设备上无缝同步网络聊天，并使用照片、实时图像分析等功能。尽管应用界面简洁、体验流畅，但目前版本缺少语音功能，且图像读取精度有待提高。此外，Anthropic还推出了团队计划，提供更多聊天次数和高级型号选择。用户需注意，iOS版本需要iOS 17.0或更高版本才能使用。同时，谷歌也更新了Gemini，允许用户使用油管、地图等扩展程序。来源：微信公众号【量子位】

【今日案例】
Kimi 助力发朋友圈(给任务提要求让 AI 生成朋友圈文案)
点击链接查看 Kimi 智能助手的对话