OpenAI数学突破、Anthropic IPO与推理模型教程

OpenAI连发三项基础科学成果，数学猜想证明引争议

OpenAI近日公布了数学、计算机和物理三个领域的科研成果，分别涉及调和分析、计算复杂性和量子场论。公司坦言这些手稿"更像是原始研究数据"，需要外部专家把关才能转化为科学理解。

数学成果针对1991年提出的局部平滑猜想，该猜想与波的聚焦有关，认为最极端的聚焦只能短暂存在。OpenAI称其模型给出了所有维度下的证明，并据此解决了开皮亚猜想和Stein限制猜想，证明基于一个新的辅助偏微分方程。AI输出于10月18日产生，次日便在Lean中完成形式化。

计算机成果更为激进：OpenAI称其系统证明了指数时间假设（ETH）不成立。ETH是关于布尔公式可满足性计算复杂度的长期猜想，被广泛相信成立，数百篇论文借它推导难度结论。该证明于10月16日找到，次日完成形式化验证。OpenAI强调，要得到更快的算法还需大量后续研究，这项工作将由三位算法与复杂性专家牵头把关，其中两位是ETH的原始提出者。

物理成果涉及量子场论的严格数学基础。OpenAI称模型给出了某些相互作用量子场论的存在性证明，包括量子色动力学以及标准模型的一种统一完成，作为子问题还包括纯杨-米尔斯理论的存在性证明——这属于克雷数学研究所的千禧年大奖问题。由诺贝尔奖得主领衔的专家组将负责把关，且决定暂不公开AI产物，先自行撰写说明。

三项成果采用了三种不同的发布策略：数学成果直接公开AI输出，计算机成果公开并组建专家组，物理成果则由专家组决定材料是否发布。合作遵循透明、不谋求学术荣誉、认可贡献和独立参与者自愿且无报酬等原则。

需要指出，这则结论目前仍在专家审查和社区检验之中。OpenAI承诺公开全部原始数据便于社区独立验证，并同意出资举办一场会议。自然语言证明和Lean证明已发布在公开的GitHub仓库。

指数时间假设（ETH） 是计算复杂性理论中关于布尔公式可满足性问题（SAT）的核心猜想，由 Impagliazzo 和 Paturi 于 1999 年系统提出。它断言：不存在能在 $O(2^{\delta n})$ 时间内（对某个固定 $\delta < 1$）求解一般 $n$ 变量 SAT 的算法，即最坏情况下 SAT 无法显著快于暴力枚举。ETH 比 P ≠ NP 更强，是「细粒度复杂性」的基石，大量论文以其为条件推导各类问题的精确下界（如编辑距离、正交向量等）。若 ETH 被推翻，意味着存在指数级加速算法，将连锁推翻数百项条件性结论，因此 OpenAI 的这一声明若成立，冲击面极广。

Lean 是微软研究院主导开发的交互式定理证明器与函数式编程语言，基于依赖类型论（Calculus of Constructions 的变体）。用户在 Lean 中编写的证明由内核逐条检查，只要通过即保证逻辑正确（前提是公理可信）。近年 Lean 与 mathlib 社区推动了「形式化数学」运动，陶哲轩等人积极倡导。文章说「次日完成形式化」意义重大：自然语言证明可能有漏洞，但 Lean 验证提供机器可核验的正确性证书，不过它只保证推理链条无误，不保证陈述本身正是人们想证的猜想——这也是争议焦点之一。

Anthropic提交上市申请，亏损收窄但治理结构存忧

据TechCrunch报道，Anthropic正式提交了上市申请，计划以NT为股票代码上市。文件披露了其财务与业务细节。

2026年上半年营收163亿美元，去年同期为12亿美元。运营亏损6.93亿美元，低于去年同期的21亿美元。合计亏损807亿美元，主要来自可转债相关的非现金调整。公司称未来可能无法实现或保持盈利，募资规模和发行价尚未披露。

企业业务规模方面，截至9月底年消费10万美元以上的客户超过11900家，年消费100万美元以上的超过1900家，年消费1000万美元以上的约250家。第三季度末净收入留存率约为900%。年消费10万美元以上的客户中，超一半同时使用平台和第一方应用，去年底该比例约为30%。

Anthropic依靠AWS、谷歌云和微软进行联合销售，直接与客户签约并向云厂商支付费用。但文件承认这些云伙伴越来越把它视为竞争对手，这可能让它更难获得所需算力——亚马逊、谷歌和微软可能优先满足自身需求。文件还提示了大客户集中的风险。

治理结构同样是关注焦点：七位联合创始人组成Founder LLC掌握50.1%投票权，公司称这是为了保护其AI安全使命。2023年设立的长期利益信托有权任命多数董事。报道称这意味着投票权与创始人的经济所有权不成比例，公众股东的实际控制力将很有限。

SpaceX获巨额GPU融资，AI业务收入超总营收一半

SpaceX披露了一笔约400亿美元的融资承诺，资金用于AI芯片和数据中心设备。TechCrunch称这是最大的GPU融资承诺。

阿波罗管理的实体买下芯片和服务器再租给SpaceX，租期约5年到5年又四分之一，从每批设备交付时开始，交易预计年底前交割，租约自2027年上半年开始。阿波罗称这将帮助交付英伟达的下一代Vera Rubin芯片。

第三季度SpaceX的AI业务收入76亿美元，超过总收入146亿美元的一半。该业务包括Grok聊天机器人、Cursor编程工具和云算力。资本开支近200亿美元，去年同期为69亿美元。首席财务官称第四季度预计支出350亿到400亿美元，并称AI基础设施投资的回收期不到一年。马斯克在X上称200多家新型云厂商将面临淘汰和整合。

开源模型工具调用准确率不足，约束解码成解法

云服务商Ubicloud在一篇工程文章中发现，开源大模型的实际工具调用表现远低于基准成绩。他们用vLLM 0.28版部署Kimi K2.6，结果只有92%的调用格式正确，也就是每25次调用有两次失败。调用失败会让上下文被错误信息污染并增加成本，这在多轮智能体场景中尤其明显。

解决办法是约束解码：从生成环节保证格式正确。vLLM在0.31版本把它做成服务器端开关，引擎在每个模型阶段屏蔽非法词元，只允许合规输出。文章称这让准确率从"尽力而为"变成"运行时保证"，预先计算掩码后额外开销可以忽略。

不过vLLM后来把默认行为改成了不开启，这让Ubicloud的准确率又降到了91%。原因是vLLM要兼容大量模型，部分模型开启后会出错，例如语法转换漏洞以及与推测解码的冲突。Ubicloud专注服务Kimi和DeepSeek^广告，于是主动开启，在测试中工具调用准确率从92%提升到100%。

约束解码（constrained decoding） 是一类在生成阶段强制输出满足给定形式语法（如 JSON Schema、正则表达式、上下文无关文法）的技术。典型做法是：每个解码步先用预计算的词元掩码屏蔽掉会导致非法前缀的词元，只在合法集合内采样。常见实现包括 Outlines、Guidance、XGrammar 以及 vLLM 的 guided decoding。其代价是可能扭曲模型的概率分布、降低语义质量，并可能与推测解码、并行采样等优化冲突；掩码需针对词表预先计算并缓存，故文章称额外开销可忽略。

8个视频11小时，从零构建推理模型教程

某知名博主发布了从零构建推理模型的视频课程，共8个视频、超过11小时，内容涵盖评估、推理时扩展、强化学习和蒸馏，全部用Python和PyTorch实现。课程从一个预训练的小型千问3模型出发，并配套一本同名新书。

博主认为，推理模型是在常规大模型上加了强化学习后训练，训练用的是可验证奖励，也可配合推理时扩展技术。他把推理模型比作引擎，智能体外壳则提供工具和上下文管理。他说当前多数大模型本身就是推理模型或带有推理模式。

硬件门槛方面，早期的文本生成和评估示例用CPU就能运行，后期训练实验则最好使用GPU。对想深入理解推理模型内部机制的开发者，这套课程提供了从理论到代码的完整路径。