LLM辅助CHC求解框架HornCraft
热点事件持续更新
LLM辅助CHC求解框架HornCraft
1 篇报道1 个报道来源58 分钟前更新
先了解这件事
AI 综述
2026年10月20日，arXiv Artificial Intelligence 刊出论文，提出 LLM 辅助的约束 Horn 子句（CHC）求解框架 HornCraft。该框架将 LLM 生成的 DPU（推导力欠近似）与不变量过近似相结合，用于 CHC 求解。报道称，在 Spacer 运行 30 分钟仍未解决的 260 个 CHC-COMP 基准上，HornCraft 对 228 个实例给出经认证的判定结果，其中 42 个被认证为不安全；而禁用 DPU 构建与复用时，被认证为不安全的实例为 22 个。报道未提及该框架的适用范围、发布时间以外的限制或收费信息。
AI 根据报道生成 · 38 分钟前更新
最新进展10月20日 12:00
HornCraft：LLM 辅助的双近似 CHC 求解框架报道时间线
沿着报道，了解事件的不同侧面。
10月20日
- arXiv Artificial IntelligenceHornCraft：LLM 辅助的双近似 CHC 求解框架
HornCraft 将 LLM 生成的 DPU（推导力欠近似）与不变量过近似结合，用于约束 Horn 子句求解。在 Spacer 运行 30 分钟仍未解决的 260 个 CHC-COMP 基准上，HornCraft 对 228 个实例给出经认证的判定结果，其中 42 个被认证为不安全，而禁用 DPU 构建与复用时该数字为 22。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。