特朗普政府削减科研经费诉讼 - 美国16个州在纽约曼哈顿联邦法院提起诉讼 包括纽约州 加利福尼亚州 伊利诺伊州和新泽西州等 [1] - 诉讼旨在阻止特朗普政府大幅削减用于增加STEM领域多样性的科学研究及相关项目的联邦资金 [1] - 这些州的总检察长认为特朗普政府无权限制研究资金或取消国会授权的美国国家科学基金会多元化项目 [1]

量子位 | 公众号 QbitAI 破解挂谷猜想 的中国女数学家 王虹 ，又有新动向。 这一次，这位出身北大数学系的90后，将 加入法国高等研究所（IHES），担任常任教授 。 什么概念？目前，法国高等研究所只有7位常任教授，5位来自数学领域，另外2位是物理学 家。 鱼羊 发自 凹非寺 这5位数学家每一位都在数学界声名赫赫，包括分别在1998年和2022年获得数学最高奖—— 菲尔兹奖的Maxim Kontsevich和Hugo Duminil-Copin，2018年菲尔兹奖获得者Peter Scholze的合作者Dustin Clausen等等。 再算上历任IHES数学常任教授，13人中共有8人是菲尔兹奖获得者。 官方公布的消息显示： 王虹将于2025年9月1日正式入职。这是IHES和纽约大学的联合任职，她在担任IHES数学常 任教授的同时，也将担任纽约大学柯朗数学科学研究所数学教授。 菲尔兹奖获得者Hugo Duminil-Copin第一时间欢迎了他的新同事： 欢迎王虹加入成为我们的教职员工！ 她在纽约大学关于这一成果的讲座，现场被挤得水泄不通： △ 图源：纽约大学 我希望她能在IHES享受我一直珍视的：宁静 ...

大模型数学推理能力发展 - 5月DeepSeek Prover V2发布 陶哲轩AI数学直播举行 谷歌AlphaEvolve推出 显示大模型解数学题能力成为衡量AI智能天花板的关键指标[1] - FormalMATH基准测试近期发布 旨在系统评估AI数学推理能力 自动定理证明表现与技术路径成为行业焦点[2] 行业技术研讨活动 - 5月29日20:00举办大语言模型形式化证明前沿探索直播 由2077AI开源基金会与多个项目团队联合发起[2] - 参与嘉宾包括DeepSeek Prover第一作者辛华剑 FormalMath项目郁昼亮 Kinima技术负责人王海明等7位学术与工业界专家[3] 行业生态互动 - 量子位策划AI主题征集活动 涵盖365行AI落地方案与一千零一个AI应用案例 鼓励分享AI产品新动向[4] - 量子位每日AI交流群开放加入 提供科技前沿进展每日更新服务[5]

核心观点 - 大模型在数学推理能力与指令遵循能力之间存在显著权衡关系，即模型越擅长复杂推理，越容易忽略用户指令要求 [1][6] - 研究团队通过MathIF基准系统验证了23个主流大模型，发现参数规模与指令服从性无正相关，部分小模型反而表现更佳 [6][7] - 推理导向训练（如SFT/RL）会提升解题能力但降低指令敏感性，且推理链越长模型越容易偏离指令要求 [9][10][13] MathIF基准设计 - 专门针对数学推理任务设计，通过程序自动验证模型对格式、语言、长度、关键词等指令的遵循程度 [3] - 包含单一/双重/三重指令组合测试，涵盖GSM8K简单题到AIME竞赛题不同难度层级 [3] - 采用硬准确率（HAcc）和软准确率（SAcc）量化评估，前者要求全部指令满足，后者计算平均满足比例 [4] - 指令类型覆盖长度限制（如500字内）、语言要求（仅中文）、格式规范（禁用逗号）、前后缀标记等5大类 [5] 实验结果 - 表现最佳的Qwen3-14B模型仅能遵守50.71%的指令（HAcc），67.06%的平均指令满足率（SAcc） [7] - 32B参数以上大模型中，Owen3-32B的HAcc达43.81%，但70B参数的DeepSeek-R1-Distill-Llama-70B+反降至41.43% [7] - 1.5B小模型Qwen2.5-Math-1.5B-Instruct在无约束时解题准确率44.05%，加入指令约束后反而提升至44.29% [7] 原因分析 - 推理导向训练使模型优先关注解题准确性，监督微调（SFT）导致Qwen2.5-7B的HAcc从15.95%降至7.86% [10][11] - 推理链长度与指令遵循负相关，人为延长思考过程会使HAcc下降超20个百分点 [13][15] - 限制RL训练中最大响应长度（1k tokens内）可提升指令遵循能力，但会牺牲部分推理性能 [17][18] 优化方法 - 在模型输出答案前重复指令要求，可使HAcc提升约5个百分点，但会降低解题准确率 [19][20] - 在RL训练中引入格式奖励机制，Qwen2.5-1.5B的SAcc从20.44%提升至28.49% [11]

AI与人类数学能力对比 - AI模型o4-mini-medium在FrontierMath基准测试中以6:2的比分击败了8支人类数学专家团队中的6支 [1] - o4-mini-medium在竞赛中得分22%，高于人类团队平均分19%，但低于所有团队综合得分35% [7] - Epoch AI预测AI很可能在年底前明确超越人类数学能力 [27] FrontierMath基准测试设计 - 测试包含300道题，难度从本科生水平到菲尔兹奖级别 [3] - 竞赛选取23道题(7道基础题+16道进阶题)，涵盖拓扑学、代数几何等四个子类 [16] - 评分机制：进阶题每题2分，基础题1分，每个领域至少答对一题额外加1分 [16] - 题目难度分为3级，竞赛中普通题为1-2级，高级题均为3级 [24] 人类参赛者表现分析 - 40名参赛者(数学博士或竞赛获奖者)组成8个团队，每组4-5人 [11] - 人类团队解题正确率在13%-26%之间，平均19% [19] - 若考虑任何一支团队答对即算人类答对，人类正确率可提升至35% [21] - 参赛者在最喜欢的测试题上平均花费40分钟 [28] 测试结果解读 - 调整难度权重后，人类平均得分约30%，"多次尝试"方法下可达52% [24] - AI解题时间(5-20分钟/题)显著短于人类 [27] - 人类在长期扩展行为上优于AI，表现能持续提升 [29] - 当前测试可能低估人类能力，更多时间可能提升表现 [27] 测试局限性 - 参赛者不能完全代表前沿数学水平 [10] - 竞赛题目仅为FrontierMath的不具代表性子集 [8] - 人类基准定义模糊，估计值在30%-50%之间 [8][20] - 竞赛形式限制了人类表现，如时间压力等因素 [27]

GitHub Copilot在数学定理证明中的应用 - 核心观点：GitHub Copilot在数学定理证明中主要起辅助作用，能快速生成代码框架和常见模式，但复杂数学细节和创造性解决方案仍需人工干预[5][6][7] - 陶哲轩演示了如何正确引导Copilot完成函数极限问题的求和、求差和求积定理证明[3][11][13][25][33] 具体证明过程 求和定理证明 - Copilot自动补全了ε-δ定义，但需手动调整绝对值符号表达[12] - 生成基本证明框架，但δ的正性验证和不等式处理不严谨，需人工修正绝对值符号、三角不等式应用和最终表达式[17][18][20] - 后期提示使用Lean内置的`add_sub_add_comm`引理简化步骤[23][24] 求差定理证明 - 沿用求和定理的框架，但虚构不存在的`sub_sub_anc`方法[27][28] - 处理代数表达式时不稳定，需手动完成恒等式证明[31][32] 求积定理证明 - 提出ε分配策略（ε/(2|M|+1)和ε/(2|L|+1)），但实现时出现正性验证和绝对值不等式错误[34][37][43] - 错误使用`add_lt_add`方法，需人工调整假设条件[37][39] - 建议复杂问题先用纸笔推导再形式化验证[41][42] Copilot的功能特点 - 优势：快速生成代码框架、提示库函数使用，对初学者友好[6][24] - 局限性：复杂数学细节可靠性低，易虚构方法或忽略适用条件[7][28][37][40]

虎嗅注： "大模型江湖，落地为王。"这句话的含金量还在提升。随着DeepSeek V3/R1在春节期间一夜爆火， 基于超大规模MoE（Mixture of Experts）架构的大模型正在从训练开发转向推理应用的落地。 对于MoE推理部署来说，效率一直是一个痛点。谁能将部署计算效率提升至最高，才能真正获得大 模型商业成功。但受限于庞大的模型容量与计算需求，传统部署方案通常依赖于多张数据中心级 GPU（如H20）。你我都知道，英伟达不仅贵，而且不断受到地缘政治摩擦的影响，不断降低自己的 性能来满足监管需求。 而在最近，华为全面揭秘超大规模MoE模型推理部署技术，不仅实现了国产的进一步突破，更全面 超越了基于英伟达Hopper架构的推理部署性能。 他们是怎么做到的？ 数学补物理，极致提升计算效率 "数学补物理"，这种通过数学理论、工具、算法和建模等方式，来弥补硬件和工艺的局限性，实现最 大化发挥芯片和系统能力效果。华为轮值董事长孟晚舟曾在2025年新年致辞中提到： "华为十多个实验室与伙伴们的工程师组成"大杂烩"团队，面对天成AI集群系统和单芯片性能的严峻 工程挑战，他们创造性应用数学补物理、非摩尔补摩尔、系统补 ...

华为昇腾技术突破 - 华为昇腾在超大规模MoE模型推理性能上全面超越英伟达Hopper架构，实现"英伟达含量为0"的突破 [1] - 通过"以数学补物理"策略，利用数学理论、算法和建模弥补硬件局限，最大化发挥芯片和系统能力 [1] - 具体产品性能： - CloudMatrix 384超节点在50ms时延下单卡Decode吞吐达1920 Tokens/s [1][18] - Atlas 800I A2推理服务器在100ms时延下单卡吞吐达808 Tokens/s [1][21] 技术开源与披露 - 公司将全面开源昇腾超大规模MoE模型推理部署技术，包括技术报告和核心代码 [2] - 技术披露周活动将展示最新进展，相关资源可通过指定链接获取 [40][41] 行业趋势与挑战 - 大模型发展重心从训练转向推理应用落地，企业竞争焦点转向推理效率 [5][6] - 超大规模MoE模型（如6710亿参数的DeepSeek V3）带来三大挑战： - 内存压力：单个专家2.5G，64GB内存硬件难以承载 [7] - 通信开销：跨芯片数据传输耗时超过计算时间 [8] - 架构创新负担：如MLA机制导致中间变量激增 [9] 技术解决方案 硬件部署优化 - 采用PD分离部署解耦Prefill和Decode时延约束 [10] - CloudMatrix 384超节点采用144卡EP并行部署，128卡专用于路由专家 [17] - Atlas 800I A2采用多节点互联，2机16卡Prefill+4机32卡Decode [20] 框架与模型优化 - 基于vLLM框架适配DP/EP并行策略，优化调度分桶和分层传输 [12] - 采用A8W8C16量化策略（INT8+BF16），差异化部署不同机型 [13] - API Server横向扩展方案提升高并发场景QPS，动态负载均衡技术解决显存占用问题 [22] 通信优化 - FlashComm方案降低25%通信量并提升10%推理性能 [25] - 层内并行转换方案消除节点内卡间求和操作 [26] - 计算通信并发机制最大化硬件利用率，MLA层计算性能提升10% [27] 算子优化 - AMLA算法将乘性计算转为加性等价形式，减少数据搬运 [31] - L1/L2缓存精细化管理提升命中率，K-buffer流水排布掩盖计算耗时 [31] - 通算融合算子实现Token粒度流水排布，降低卡间同步开销 [31] 性能实测数据 - Prefill阶段：16K序列端到端耗时631ms，卡均吞吐1622 Tokens/s [34][36] - Decode阶段： - 2K输入+2K输出场景下吞吐达808 Tokens/s（90%接受率） [32] - 1K输入+2K输出场景下吞吐达876 Tokens/s（90%接受率） [32] - SiliconLLM框架部署DeepSeek-R1实现单卡1920 Tokens/s，等效H100性能 [38][39]

核心观点 - 大语言模型（LLM）与形式化数学结合正推动数学领域的范式变革，解决传统人工验证的瓶颈问题 [1][4] - 形式化数学通过严格逻辑和计算机辅助验证提升数学证明的可靠性和效率 [4][7] - 从Theorem Prover向Proof Engineering Agent转型是形式化数学的未来趋势 [11][17] - APE-Bench作为自动化证明工程基准，支持形式化数学的长期动态演进 [12][16] - LLM与形式化方法的结合将催生Certified AI，提升知识生产的可信度和效率 [17] 形式化数学的背景与挑战 - 现代数学证明规模庞大（如300页的开普勒猜想证明），传统人工验证效率低且易出错 [6] - 形式化数学通过公理系统和逻辑语言表达数学内容，借助计算机工具实现自动化验证 [8] - LLM的"幻觉"问题在数学领域尤为突出，需结合形式化方法确保生成内容的逻辑严密性 [6] 形式化定理证明的应用 - 典型案例包括Flyspeck项目（验证开普勒猜想）、液体张量实验（验证凝聚态数学引理）、PFR猜想众包验证 [13] - 形式化方法适用于数学理论证明和软件工程验证，确保逻辑一致性 [9] LLM驱动的最新进展 - AlphaProof在国际数学奥林匹克题目证明中达到银牌水平，DeepSeek-Prover V2在miniF2F基准成功率近90% [10] - LEGO-Prover项目利用LLM构建可复用的数学知识库，推动形式化数学向库级理论构建转型 [10] - 前沿研究探索LLM主动提出数学猜想和发现抽象结构的潜力 [10] Proof Engineering Agent转型 - 当前形式化工具面临人工成本高、协作效率低等问题（如Flyspeck项目耗费数十人年） [11] - 下一代工具需具备自我规划、修复和知识积累能力，支持大规模跨模块协作 [11] APE-Bench的设计与实施 - 分为三个阶段：单文件局部修改（APE-Bench I）、跨文件一致性维护（APE-Bench II）、完全自主Agent模式（APE-Bench III） [19] - 基于真实数学库（如Mathlib4）的历史修改记录，模拟实际Proof Engineering场景 [12] 未来影响与展望 - 数学领域：提升验证效率，推动理论创新和概念探索 [17] - 工业领域：应用于高安全系统（如操作系统内核、智能合约），提升安全性与可靠性 [17] - Certified AI将结合形式化验证与动态学习，成为可信的知识生产伙伴 [17]

白交 一水 发自 凹非寺 量子位 | 公众号 QbitAI 快来围观，陶哲轩当视频博主了。 第一个产出就很炸裂： 人类需要写满一页纸的证明，结果借助AI 33分钟就搞定了？！ 整个过程看起来一气呵成，还是全程 "盲证" 不用过脑子那种。 对于这一操作，网友们惊呆：这具有足够的历史意义。 在没有明显引导、宣传之下，他的订阅数一天时间已经有900+，观看数超两千，目前仍然在高速增长中。 大家赶在爆火之前留言： 今天我们相聚在这里，就是为了见证伟大数学频道的诞生。 具体来看看是如何做到？ 33分钟盲证定理 陶哲轩这次选取了泛代数中的一个命题，即 证明Magma方程E1689蕴含E2 。 方程具体是什么不重要，我们只需要了解，即使是方程理论项目的合作者Bruno Le Floch，也足足人工花了一页纸才完成证明。 而用上AI后，整个证明过程仅用时 33分钟 ： 具体而言，陶哲轩尝试完全基于Bruno Le Floch的草稿，逐行进行形式化。 他将草稿拆分为微小逻辑单元，交由 GitHub Copilot生成代码骨架，再以Lean的canonical策略匹配填补细节 ，过程中也涉及部分手动补 全。 最终，整个形式化证明 ...