北京
8月2日消息，OpenAI周六公开十项数学与理论计算机科学成果，同时放出249页论文、62页推理说明和一套Lean 4形式化证明。不过生成这些结果的下一代模型Astra仍是内部版本，没有随之开放。
据OpenAI介绍，Astra生成数学论证后，人类与模型共同将其整理成论文，再由模型编写Lean证明。OpenAI把寻找十项解法消耗的token按Sol API价格折算，估计成本约为2000美元。
这种发布方式在AI行业里不太寻常的：外界暂时无法测试Astra，却可以先检查它交出的数学结果。
周五The Information曾援引三名知情人士称，Astra当时仍是暂定名称。OpenAI向华盛顿的政策制定者和监管人员演示过它处理长时任务和多智能体协作的能力，但没有给出产品发布时间和最终型号。
十项成果，分属不同的证明任务
这份名单横跨高维几何、编码理论、群论、算术电路、量子复杂性、格密码和极值组合数学等多个分支。
具体来看，高维球堆积和编码理论得到新的上界；Astra构造了非sofic群，并为Connes刚性猜想给出反例；Ehrhart体积猜想得到锐界；多色Ramsey数和极值图论的研究则解决了三个由保罗·厄多斯提出、长期未解的问题。
有些工作把已知边界向前推进，有些构造过去不知道是否存在的对象，还有些推翻或完成具体猜想。它们被放在同一次发布里，后续复核和引用则会分别发生在各自领域。
Lean 给外部复核加了一条可运行路径
OpenAI在GitHub公布了十项结果的Lean文件、统一构建命令和Comparator配置。官方形式化清单显示，主要证明的sorry_count为0，只使用propext、Classical.choice和Quot.sound三类公理。Comparator目录里的sorry是留给外部核验者的题面空缺，不在正式证明文件中。
配置相应版本的Lean、mathlib和Comparator后，研究者可以在本地重跑证明，检查解答是否证明同一形式化命题、是否引入清单之外的公理、以及推导能否被Lean内核接受。同行审稿通常需要数月乃至数年，形式化文件提供了一条可以定位到具体行的复核路径。
不过Lean内核只检查推导本身。猜想到形式化命题的翻译是否走样、方法是否新颖、结果在学科内的分量，仍需要人来判断。
62页推理说明是事后整理稿。文件注明，模型读过原始思维链与最终论文后，重新叙述成功思路、失败路线和转折点。这意味着，读者看到的是重构后的路线图，不是模型当时的原始思考。
2000 美元只是 token 成本
寻找解法约2000美元这个数字，只计算token，并按Sol API价格折算。模型训练、选题、数学家参与、基础设施和项目中的其他成本没有列入。官方仓库另注明，把这些证明写成Lean形式化文件，前后花了一周时间。
与这次发布同期，《华尔街日报》报道，新晋菲尔兹奖得主雅各布·齐默曼（Jacob Tsimerman）将从多伦多大学休假，加入OpenAI从事AI安全研究。他准备把数学中的形式语言和验证方法用于理解、评估模型行为。
两周前，Anthropic研究员莱文特·阿尔珀格（Levent Alpöge）公布了Jacobian猜想在三维及更高维度的反例，并把寻找反例的功劳归给Fable 5。提示词、搜索过程以及人和模型各自完成了多少工作，至今没有公开。
阿尔珀格的博士导师正是齐默曼。
OpenAI这次用Lean检查模型给出的数学证明。齐默曼加入后，想把形式化方法继续用到模型行为上。对OpenAI而言，“验证”正在同时进入模型的产出和模型本身。（易句）
（本文由AI翻译，网易编辑负责校对）
本文来源：网易智能
责任编辑：
王凤枝_NT2541
