AI DAILY / 2026-08-02
今天的主线是模型能力开始留下可复查的外部痕迹：OpenAI 称内部版 Astra 在数学与理论计算机科学中给出十项结果，并公开 Lean 证明；Grok Imagine Video 1.5 把原生 1080p、文生视频和引用能力放进同一产品线。开发侧，OpenAI 正把大仓库 Git 优化提交回上游，Codex 与 ChatGPT Work 的周末使用限制也被重置。
OpenAI 称其下一代主要模型 Astra 的一个内部版本，在数学和理论计算机科学的长期问题上给出十项新结果，并已把相关 Lean 形式化证明公开到 GitHub。 公司列举的范围包括高维球堆积、编码理论、群论、算术电路复杂度、量子并行重复、最近向量问题和极值图论等方向；公开仓库的说明确认其中保存的是数学与理论计算机科学证明对应的 Lean certificates。 这批结果仍需数学界按各自领域标准审阅。OpenAI 的说明把模型生成论证、人工整理和 Lean 形式化作为不同环节；因此，公开仓库可供复查的是形式化证明材料，而非对全部研究过程的独立复现。 证明库：https://github.com/openai/ten-proofs
SpaceXAI 为 Grok Imagine Video 1.5 增加文生视频、图像/语音引用与原生 1080p 输出能力。 官方开发文档显示，文生视频和图生视频可使用 1080p；引用生成则可由一张或多张参考图引导视频，但该模式最高为 720p。视频生成采用异步任务方式，处理时间会随分辨率和编辑方式变化。 语音引用目前只面向美国的受信任合作伙伴，文档要求通过销售渠道申请；因此，不同引用能力的可用范围并不相同。原生 1080p 是文本和图像驱动生成的规格，不应与 reference-to-video 的输出上限混用。 文档：https://docs.x.ai/developers/model-capabilities/video/generation
OpenAI 公开了面向大型仓库的 Git 补丁状态页：2 个补丁主题已进入上游 Git 的 master，5 个在 seen 分支审查，另有 23 个仍在其维护的主题分支中。 已合入的主题包括避免路径受限的 git stash 不必要展开 sparse index，以及为 path-walk 使用 bitmap 与 delta islands。页面将这些工作定位为对大型仓库 Git 使用的性能和正确性改进。 处于 seen 或本地开发阶段的补丁尚未成为 Git 的稳定上游行为。OpenAI 在页面中提供对应的上游提交、邮件列表和分支链接，后续是否合入仍取决于 Git 社区审查流程。
Codex 负责人 Tibo 在 X 上表示，已重置 Codex 和 ChatGPT Work 的使用限制，面向周末的高强度任务使用。 该信息来自负责人的公开帖文，未附新的订阅价格、长期额度或产品规则说明；本次调整应理解为一次限额重置，而不是永久配额政策变更。
一名开发者在 LocalLLaMA 社区介绍 LM Bench：该项目收集食品安全、激光物理、无线网络、英语文学、心理学等窄领域小型基准，并允许用户组合模型与系统提示词后进行人工评测和比较。 项目作者将其定位为补充通用排行榜的入口，重点是让领域任务自行定义题目和判定方式。 这是一项社区项目，当前能力和样本规模以发布者描述为准，尚不构成独立的通用模型榜单。对本地模型使用者而言，价值在于把实际业务问题与模型、提示词配置放到同一组对照中，而不是直接替代公开大基准。 ---