形式化验证 LLM-DailyDigest 2026-08-30 2026-08-30 约 100 字 预计阅读 1 分钟 形式化验证 本主题由提交工具自动创建，可在此补充洞察与资料。 相关消息（按子主题自动聚合） 世界模型 1 通用决策大模型 Decitron：开放世界推演与求解闭环 09-03 元智能体编排 1 Eureka：面向科学发现的任务条件元代理编排 08-20 分层验证 1 给验证器打分：LLM 推理验证自治等级 L0–L5 08-20 协同规划 1 集体反事实规划：表征约束下的协调、同意与验证 08-19 可信执行 5 基于 Petri 网监督控制的智能体认证执行框架 10-23 Proof-Carrying Contracts：智能体不可违背的可证明契约 10-22 VeriLoop E2以外部证据门控实现可验证状态演化 10-18 VeriLoop E2以循证递归实现可验证状态提交，黎曼零点比例下界达67.35% 10-09 面向可信智能体执行的策略代数 08-18 可信推理 3 人机协商即交互式证明：无需透明性的可验证条件 09-22 LogicTrack：用形式逻辑求解器审计大模型推理轨迹 09-21 验证器引导的可解释推理框架：QLoRA、符号路由与群组相对 RLVR 09-07 可验证推理 1 SymbolLKG：以逻辑知识图与符号求解器实现可验证推理 08-29 多智能体协作风险 1 自主科研智能体群体中的涌现作弊与举报行为 09-07 多智能体系统 2 随机环境中的多智能体协调社会法则 09-17 Stellar Colosseum：面向数学与理论计算机科学长程研究的多智能体框架 09-15 形式化证明 36 数十个 AI Agent 24 天形式化有限单群分类定理 10-29 OpenAI与Anthropic模型被曝独立证伪指数时间假设 10-29 OpenAI多智能体生成纳维－斯托克斯证明，人类启动解读与核查 10-29 智能体算法设计：在 Lean 中提出、形式化并证明进化算法运行时界 10-27 微软研究员借助 AI 证明 KLS 猜想 10-22 OpenAI纳维-斯托克斯证明路线遭重新解读 10-18 LeanGraphSearch：面向形式化定理证明的图搜索 10-18 面向 GPU 高效证明候选评估的 Lean 反馈学习 10-18 九章云极以可验证数学推理问鼎陶哲轩数学蒸馏挑战赛 10-18 NanoProof：开放高效的 Lean 4 自动定理证明器 10-10 LEVER：基于 AND/OR 图的自适应成本感知证明搜索 10-09 Claude被曝以Lean证明渗流理论连续相变猜想 10-08 CoCo-Prover：智能体编排驱动的低成本程序定理证明 10-08 让方法库自荐：面向形式化证明的适用性感知方法选择 10-08 10个Claude协作形式化证明汤姆逊问题N=7 10-01 FYAN：面向文档级形式化的语义审计人机协作框架 10-01 ProofLoom：以证明义务驱动的随机优化理论自动形式化 09-30 多智能体提出C-HD最短路径算法并完成Lean验证 09-29 AI辅助Lean完整形式化验证庞加莱猜想证明 09-29 多智能体提出并验证 C-HD 最短路径算法 09-28 报道称万名 AI 智能体用形式化证明攻克 Navier–Stokes 难题 09-25 Lean Pool：AI 维护的形式化数学档案库 09-24 GPT-6 Astra证明刘维尔–哥德巴赫猜想并经Lean 4验证 09-21 传OpenAI积压数百项AI生成数学证明 09-18 FormalFlow：MIP* = RE 核心定理的长程自动形式化 09-18 Aaronson称AI公司或暂未公开多项数学突破 09-16 OpenAI被曝逼近霍奇猜想，并与Anthropic竞逐BSD猜想 09-11 OpenAI称在第二道千禧年难题上取得实质性进展 09-11 Claude借助多智能体Harness完成费马大定理形式化证明 09-07 Claude 推进黎曼猜想零点界，获数学家重证与 Lean 验证 09-07 Claude多智能体形式化验证费马大定理 09-07 GPT-5.6提出大素数空隙新构造并通过Lean验证 09-07 AxQM：有限维量子力学形式化证明合成基准 09-07 Claude 以 Lean 完成费马大定理端到端形式化验证 09-07 AxiomProver用Lean 4完成“246定理”形式化验证 08-23 AI 辅助攻克森多夫猜想，陶哲轩推导出更强结果 08-16 形式化证明修复 1 CAPRI：面向 Isabelle 的契约感知证明修复 08-16 形式化评测 1 FormalTCS：端到端前沿理论计算机科研评测 08-21 形式化验证 17 OpenAI 邀外部专家与 Lean 核查 AI 科学证明 10-29 ORSMT：基于SMT的LLM优化建模语义验证与修复 10-22 Racer：用符号等价性检查发现 GPU 内核缺陷 10-21 FAOP：AI 智能体工作流的范式与代数体系 10-18 SpecGuard：在编码智能体作弊前证明任务规格冲突 10-08 VeriCodeBench：自生成规约的可验证代码生成评测 10-01 从验证失败中提炼编码智能体的可复用指导 10-01 面向 LLM 辅助 Verus 验证的低假设可复用技能 09-30 RAISE：基于符号评估强化大模型访问控制策略合成 09-29 认证 AI 提议的时序规范修订：受保护核心仍不够 09-29 EquivSVA：跨等价 RTL 实现的形式化验证行为断言数据集 09-23 LLM-Falsifier：用大语言模型寻找信息物理系统反例 09-18 利用 LLM 发现数学形式化建模中的常见错误 09-16 CONTINUITY：可组合 LLM 智能体控制的安全上下文契约 09-07 Specula 自动形式化验证：67 个开源系统发现 382 个深层 Bug 08-27 AI 证明泛滥后，可信验证成为最昂贵的智能 08-19 Vero：智能体能否构建形式化验证的软件仓库 08-16 指标演化 1 EvalCEGAR：从盲点中自动演化评估指标 08-20 推理评测 1 GPT-6 Astra补全FrontierMath Tier 4最后一道未解题 09-11 数学推理 5 数学家呼吁抵制 OpenAI 批量发布 AI 生成证明 10-09 未发布 Claude 推进黎曼猜想相关下界并支持形式化验证 10-08 OpenAI内部模型被曝24天攻克百余道数学难题 09-22 GPT-6 Astra攻破FrontierMath Tier 4最后未解题 09-13 OpenAI以千禧年难题测试万级Agent数学研究系统 09-11 断言生成 1 NeuroAssertion：覆盖驱动的 RTL 断言生成与神经符号精炼 08-20 本体推理 1 Baobab：将 OWL 2 DL 编译为可微电路的神经符号学习 08-19 模型评测 1 SIV：基于定理证明器的 NL→FOL 翻译评测指标 09-29 模型验证 1 以模型检验为预言机自动测试 LLM 事后解释器 09-01 符号规划 1 PDDLCoder：智能体式 PDDL 生成辅助符号规划 08-18 答案验证 1 迁移式验证：精确信息前沿与调用成本 10-09 缺失前提识别 1 GUARD：论证性实质推理的自动形式化 09-16 脚手架演化 1 面向 Rocq 与 Lean 的智能体证明器接口演化 10-01 自动化科学研究 8 PSI用AI辅助突破5项量子信息开放问题 10-29 ClawsGO Science用Lean验证化学平衡猜想的细致平衡情形 10-29 OpenAI 宣布 AI 模型取得三项科学理论突破 10-27 AI 智能体发现低延迟共识协议 A-greement 10-22 Claude Mythos 5 闭环优化量子电路，八项任务刷新最优设计 10-18 OpenAI 公开 722 篇 AI 生成数学手稿 10-08 GPT-6 Astra辅助构造Grad核聚变猜想反例 10-08 陶哲轩警告黑箱AI解题或“污染”数学研究 09-07 自动形式化 1 自然语言到一阶逻辑的 LLM 自动形式化综述 10-09 自我改进 1 回望式分层规划：通过事后提炼思路训练推理模型 10-09 评测审计 2 ALIAS：评估 LLM 生成 TLA+ 规范的性能与记忆效应 10-22 RTL 修复基准究竟测量了什么？ 10-21 语义编译 1 受限语义规划与确定性编译提升企业 Text-to-SQL 可靠性 08-18 辩论评判 1 事后辩论裁判理论 08-20 过程奖励模型 1 SPRING：SMT 求解器引导的逻辑推理过程奖励 09-30 递归自我改进 1 自我改进问题：自动更新门控的可计算性边界 10-18 长期记忆 1 PerMIT：以机器验证完整性定理保护智能体持久记忆 10-22 验证器开发 1 AI 权威执行：从应用到芯片的机器验证 08-24
