跳到正文
今天10月23日周五4 条
  1. AIHOT · AI 动态聚合80

    Anthropic 用 Claude 为 123 个开源库完成汇编级形式化无崩溃证明

    Anthropic 与 Theorem 合作,用 Claude 将 OSS-Fuzz 模糊测试转化为规格,对 123 个开源库的 239 个入口点证明任意 64 MB 以下输入不会崩溃,生成约 1.8 亿行 Rocq 证明。

    推荐理由:读者可据此了解 LLM 规模化形式化验证的实际流程、证明复用机制与可信组件边界。

  2. AIHOT · AI 动态聚合34

    Microsoft Research 与合作者证明 31 年历史的 KLS 猜想

    Microsoft Research 的 Xinzhi Zhang 与 Zhao Song 证明了 1995 年提出的 KLS 猜想,确立对数凹分布的最优平面切割与任意形状切割之差以普适常数为界、不随维度增长。证明源自人类引导的多智能体迭代剪枝过程,约百条研究路径中筛出关键判据,另有独立团队同日发布完整证明,并已有 Lean 4 形式化验证。

10月22日周四
10月21日周三