标签
GitHub Next 与微软研究院推出 Chopin 和 Proof-Driven Development Kit（PDD Kit），可将开发计划转化为形式化规范，并证明 AI 生成的代码对所有输入均符合规范，使团队无需逐行审查即可将 AI 生成的代码安全上线，目前已进入研究预览阶段。
本文正式提出了规范驱动的智能体开发（SDAD），旨在利用AI重构软件开发生命周期，强调精确规范和多智能体验证，以实现规范化的智能体速度。
SCP-NL2TL 是一篇提出选择性翻译框架的论文，该框架利用保形风险控制来决定自然语言到时序逻辑的翻译何时可以信任，从而提高安全关键型自主系统的可靠性。
HyPOLE提出了一种在部分可观测性下进行多智能体强化学习的框架，它通过HyperLTL时序逻辑进行超属性引导学习，并与集中训练分散执行（CTDE）集成，在SMAC、MessySMAC和WildFire基准测试上展示了优于基线的结果。
讨论AI生成代码中形式规范的必要性，并介绍PICK，一种利用人类判断帮助程序员为LLM生成的正则表达式指定所需属性的工具。