Google DeepMind 推出 AlphaProof Code，用 AI 智能体形式化验证 Signal 协议代码
Google DeepMind 发布 AlphaProof Code，一个多 LLM 智能体形式化验证框架，并用它数学证明了 Signal 协议实际代码的关键安全属性。
推荐理由：DeepMind 用多 LLM 智能体框架对 Signal 协议实际代码做形式化验证，四周完成过去需数年的工作，并开源验证产物。
内容类型
论文研究 最新动态
值得读的 AI 论文与研究成果：架构创新、训练方法、能力测量与理论进展。
5 条精选近 30 天 3 条共收录 21 条
更新
论文研究的精选
Google DeepMind精选AI 评分8585
Microsoft Research精选AI 评分7474 微软研究院等证明 31 年未解的 KLS 猜想
微软研究院研究员 Xinzhi Zhang 与合著者 Zhao Song 证明了 1995 年提出的 KLS 猜想，给出与维度无关的固定界，解决了高维几何与概率论的核心开放问题。证明过程采用人类引导的智能体搜索，探索了 100 多条候选路径，由研究者筛选和调整方向；同期另有独立团队给出完整证明，并出现 Lean 4 形式化验证。作者称此前用多个前沿模型做无引导的端到端尝试未能成功。
推荐理由：微软研究员与合著者借助人类引导的智能体搜索证明 KLS 猜想，展示了人机协作做数学研究的具体流程。
Microsoft Research精选AI 评分6060 微软研究院推出 Magnetar：基于证明的通用计算 zkVM
微软研究院发布零知识虚拟机 Magnetar，可直接证明用 Rust、Go 或 C 编写的程序执行过程，在 15 个基准程序上平均比现有最快 zkVM 快 10 至 39 倍。它基于 RISC-V 架构，在笔记本上每秒可证明 720 万至 870 万条处理器指令，证明验证约需 12 毫秒。其安全性仅依赖 SHA-256、SHA-3 等标准哈希函数，不需要椭圆曲线、格假设或可信设置。
推荐理由：微软研究院梳理十余年零知识证明研究脉络，说明 Magnetar 如何同时解决效率、通用性与后量子安全三个难题。
GitHub Blog · AI & ML精选AI 评分6262 GitHub 发布 AI 代码审查开放基准 ReviewBench
GitHub 发布 AI 代码审查开放基准 ReviewBench，基于 1.039 亿个 GitHub PR 的分布构建 219 个公开 PR 语料，覆盖 19 种语言。
推荐理由：GitHub 公开了基准的构建方法、评分规则和人工一致性数据，读者可据此判断 AI 代码审查评测的可信度。
Berkeley AI Research精选AI 评分6262 从 CUDA 到 MLX：K-Search 如何把内核优化经验迁移到 Apple Silicon
Berkeley Sky Lab 与 IBM Research 在 K-Search 演化式内核搜索框架上新增 MLX 后端和结构化 CUDA-to-MLX 翻译层，让已有 CUDA 内核作为知识库迁移到 Apple Silicon。
推荐理由：作者把 CUDA 优化经验整理成结构化上下文交给 K-Search，读者可看到跨平台内核迁移中上下文质量比模型写代码能力更关键。