公司与模型
微软的 Copilot 系列产品、Azure AI 云服务，以及与 OpenAI 的合作动向。
6 条精选近 30 天 5 条共收录 46 条
微软研究院发布 PDD Kit，把开发者意图转成 Verus 形式化规范，对每个输入验证智能体所写代码，证明覆盖不到处以测试兜底。团队在 GitHub Next 的 Chopin 中用它验证了约 5,000 行 Rust 全栈应用 Pet Store 的登录逻辑，开发者只审查意图产物而未逐行阅读生成代码，pdd-ship 还会把 Verus 检查加入 CI。
推荐理由：原文展示把代码审查重心从逐行阅读转向意图规范的方法，以形式化验证和边界测试守住智能体的实现约定。
Microsoft 宣布将 GitHub 工程团队打造的 Copilot harness 通过 Microsoft Foundry 开放，开发者与企业客户可用全托管方式构建能推理、调用工具并完成复杂长任务的智能体。
推荐理由：原文解释了多模型编排层为何难以自建与维护，开发者可据此评估改用托管 harness 来聚焦上层应用的取舍。
Microsoft Research 研究员 Xinzhi Zhang 与 Zhao Song 证明了 1995 年提出的 KLS 猜想，表明对数凸分布中最优平面切割与任意形状切割的差距不超过与维数无关的通用常数。
推荐理由：原文讲清了证明如何通过递归精化消除维度依赖，同日出现的独立证明和随后的 Lean 4 形式化让结果不依赖单一推理链。
Microsoft Research 发布零知识虚拟机 Magnetar，可直接证明 Rust、Go 或 C 程序的执行，在 15 个基准程序上比现有最快 zkVM 平均快 10 到 39 倍。
推荐理由：原文给出零知识证明在速度、通用性和安全性三方面的实测数据，读者可以据此了解可验证计算走向实用的程度。
Microsoft 宣布从 2027 年起将 Azure Maia 家族扩展至多吉瓦级部署，并使 Maia 成为 Microsoft 产品与服务的主要推理系统。
推荐理由：原文给出 Maia 300 每兆瓦 token 效率和机架吞吐的具体数字，读者可据此比较微软自研芯片与 GPU 方案的定位。
微软宣布Microsoft 365与LinkedIn执行副总裁Ryan Roslansky将离开公司，年底前以顾问身份向Satya Nadella汇报并协助过渡。
推荐理由：原文同步公布核心汇报线调整，可据此了解LinkedIn与Microsoft 365业务在这次人事变动后的组织归属。