★ 3
DRAGO：确定性诊断修复 LLM 生成形式化规格，回归率降至 1.3%
论文提出 DRAGO 修复框架，用确定性、形式化系统专属诊断替代无依据的 LLM 批评，仅在诊断错误权重严格下降时保留改写。在 SMT-LIB2、MiniZinc、PDDL 五个基准上，回归率从 11.8% 降至 1.3%，答案准确率较零样本形式化提升 12.9 个百分点。论文还发现 Planet…
arXiv cs.AI13 天前
#形式化方法
共 6 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 3
Kern 发布 AI 生成代码零信任验证网关
Kern 是一个位于 AI 编码代理与代码仓库之间的 L0–L5 验证网关，用 SMT 求解器与形式化证明替代「测试通过」的布尔结果。它采用 Belnap B₄ 四值逻辑，只有机器可验证的声明才能通过，防止 AI 代理用无断言测试蒙混过关。
Hacker News – AI16 天前
★ 2
FRACTAL：自相似多智能体编排架构，给出通信与深度界
论文提出 FRACTAL 自相似多智能体架构，用于递归目标分解，五组件组织模式在分解树每层重复。形式化贡献包括：两阶段协议下节点内通信成本线性于集成规模与轮数、生成与评估两阶段编排判据、超多数收敛保证与深度界、贝叶斯层间升级机制。论文未报告定量性能结果。
arXiv cs.AI13 天前
★ 2
面向规范引导决策的信念道义逻辑
研究者提出一种简单的信念道义逻辑，用于自主系统在规范冲突与信息不完整下做决策。该逻辑扩展了Chellas最小道义逻辑的可归约片段，结合多智能体KD45，定义「信念规范合规优化问题」。论文给出主客观优化一致的条件，并证明最优决策可在多项式时间内归约为加权部分MaxSAT。
arXiv cs.AI31 天前
★ 2
OpenShell 用形式化方法控制 AI 智能体的经验
OpenShell 分享了将形式化方法应用于 AI 智能体控制所获得的经验教训。形式化方法通过数学化规约与验证来约束智能体行为，有望提升其可靠性与可预测性。该实践为智能体安全与可控性研究提供了工程层面的参考。
Hacker News47 天前
★ 1
Barista：用LLM智能体合成类型状态规范
Barista是一项学术研究，利用LLM智能体自动合成类型状态规范（typestate specifications），用于程序验证。该方法旨在降低形式化规范编写的人工成本。
Hacker News – LLM17 天前