微软研究院用 PDD Kit 形式化验证智能体编写的全栈 Web 应用
微软研究院联合 GitHub Next 提出 Proof-Driven Development（PDD）与配套工具 PDD Kit，把用户意图转成 Verus 形式化规格，证明智能体写的代码对每个输入都满足规格，证明覆盖不到的部分改用测试。
推荐理由：微软研究院与 GitHub Next 展示用 Verus 形式化验证智能体生成的登录代码，把审查重心从逐行读代码转向审阅意图规格。
技术方向
部署工程 最新动态
怎么把模型跑得更快更省钱：推理加速、显存与成本、服务部署与基础设施选型。
2 条精选近 30 天 1 条共收录 19 条
更新
部署工程的精选
Microsoft Research精选AI 评分6464
Berkeley AI Research精选AI 评分6060 从 CUDA 到 MLX：K-Search 如何把多年内核经验带到 Apple Silicon
Berkeley Sky Lab 与 IBM Research 把 K-Search 进化式内核搜索框架扩展到 MLX，并加入结构化的 CUDA 到 MLX 翻译层，让已有 CUDA 内核作为知识库迁移到 Apple Silicon。
推荐理由：作者把 CUDA 优化知识整理成结构化上下文交给进化搜索，让 MLX 内核在 Apple Silicon 上接近专家水平，可看跨平台迁移的做法。