★ 4
研究团队用 Claude 对 100 多个开源库完成汇编级形式化验证
研究团队与 Theorem 合作，使用 Claude 在 RISC-V 汇编层面为 100 多个真实开源软件库生成形式化安全证明，属首次大规模将 AI 用于生产级软件的形式化验证。过程中 Claude 还发现了历经数万亿次测试仍未暴露的缺陷，有望让形式化验证进入常规开发流程。
Hacker News10 天前
#形式化验证
共 40 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 4
验证器驱动的智能体 RL 实现可证明正确代码
论文构建智能体环境与奖励，读取程序验证器的诊断而非仅判定结果，按已履行证明义务的加权比例评分，并加入完整性审计防止策略作弊。在 Qwen3 系列模型上，DafnyBench 留出验证率从 66.1% 升至 93.5%，SWE-Proof 从 56.3% 升至 100%，仓库补丁问题解决率从 59.…
arXiv cs.LG17 天前
★ 4
OpenAI公开数学研究目录
OpenAI发布由内部模型生成的数学手稿与证明工件目录，包含722篇手稿、372个结果族，覆盖多个数学学科。这些结果由未公开的内部模型平均花费3小时ChatGPT Pro思考算力得出，部分结果尚未完成Lean形式化验证。
Lobsters – Machine Learning26 天前
★ 4
SWE-Proof：用机器可验证证明评测代码生成
作者提出 Benchproofer 流水线，将带有已知正确补丁的编码任务转化为形式化验证任务，并据此构建 SWE-Proof，包含 500 个经形式化验证而非测试验证的真实 issue。评测发现测试通过的补丁中有四分之一到一半存在反例，而正确形式化规范可将 Opus 4.8 的解决率从 85% 提…
arXiv cs.LG41 天前
★ 4
MAGS多智能体框架为生成代码提供形式化安全保证
论文提出多智能体框架MAGS，针对LLM编码智能体生成代码难以人工审查的安全风险，以Dafny作为可验证中间表示，冻结人工审计的API与安全需求，将生成代码翻译为Dafny并利用验证器反馈修复违规，再编译回可执行程序。在100个CUDA内核、100个终端脚本和20个机械臂任务共220个样例上，实现…
arXiv cs.AI44 天前
★ 4
Magenta：打通数学推理与Lean形式化验证的闭环
论文提出Magenta，一个免训练的智能体流水线，仅给定自然语言问题即可产出答案、将其表达为Lean 4命题并构造机器可验证的证明。系统包含命题裁判以验证形式化是否保留原问题，以及错误归因裁判将失败尝试路由到数学重新推导或局部Lean修复。Magenta在AIME 2025、AIME 2026和H…
arXiv cs.AI50 天前
★ 3
PaperFormalizer 推出 Lean 论文形式化作者在环流水线
研究团队发布 PaperFormalizer，一个基于 Lean 的智能体流水线，从 LaTeX 源码出发将论文转写为陈述依赖图，审计忠实性与歧义，再在 Mathlib 上形式化并证明。流水线在陈述存在多种解读时暂停询问作者，输出带注释的修订版论文、变更报告与 Lean 代码，可运行于 Claud…
arXiv cs.AI6 天前
★ 3
PerMIT：为 LLM 智能体持久记忆提供可验证完整性
论文提出 PerMIT 记忆架构，在「仅信任用户输入与闸门确认值」的前提下提供可证明的完整性保证，两条定理已在 Lean 4 中机器验证。在 Trojan Hippo 上零攻击成功；在 τ²-bench 上最多 90 个智能体共建共享知识库，无记忆注入被提升，且新智能体在留出任务上表现提升。
arXiv cs.AI10 天前
★ 3
研究用形式语义检验 LLM 智能体规划能力，在线成功率仅 40%
论文以隐藏 PDDL 模型为形式语义基准，在五个领域、四个模型、六种提示策略与三种智能体架构下检验 LLM 智能体的规划声明。最佳配置离线解决 78% 可解任务，在线仅 40%；不可解任务识别率低于 10%，更重的提示策略消耗 5 至 22 倍 token 却无明显收益。
arXiv cs.AI12 天前
★ 3
arXiv 发布 Lean4AgenticRL 框架与 LAR-9B/27B 智能体模型
Lean4AgenticRL 是首个将多级过程奖励建立在统一 Lean4 形式化体系上的开放式智能体强化学习框架，结合问题专属工作流与工作流阶段归一化 GRPO 算法。基于该框架训练的 LAR-9B/27B 中，LAR-27B 在 TerminalBench-2.1 上达到 77.3%，平均超越基…
arXiv cs.LG13 天前
★ 3
VEPA：可验证演化的LLM智能体形式化护栏
论文提出VEPA框架，将智能体护栏表示为可执行符号规则的形式化策略，部署时由LLM根据反馈提出策略补丁，经确定性验证器校验后由证据感知授权层激活。在ASSEBench-Safety、ASSEBench-Security和ATBench上持续超越基线，并在混合流、损坏反馈等条件下保持优势。
arXiv cs.AI20 天前
★ 3
SpecGuard：用Lean 4形式化验证提前识破智能体作弊任务
论文提出SpecGuard，可在编码智能体执行前检测任务意图与测试之间的冲突，并用Lean 4形式化生成机器可验证证书。在冲突的SWE-bench任务上检测率达72.8%，形式化认证率51.1%，漏检率比模型判断低近五倍。
arXiv cs.AI24 天前
★ 3
Choir：分布式多智能体形式化开放协议
当前用 Lean 等证明助手形式化教科书与定理的工作多为集中式，由单一团队承担全部算力成本。Choir 提出开放协议，将项目拆解为可由独立贡献者完成的任务，各自运行自己的智能体与 LLM 订阅，通过 GitHub 仓库协调，合并前经确定性门禁校验。协议支持 Lean 4、Isabelle 与 Ro…
arXiv cs.AI33 天前
★ 3
NeuralCert：神经网络辅助数学构造的精确认证框架
该论文提出 NeuralCert 框架，将高维变分试探函数以紧凑可分离表示学习，经谱诊断与剪枝后通过多模评估实现精确认证，使数值证明完全显式且可独立验证。在三个极值问题上，神经优化分别实现了发现更优构造、揭示经验不变量以导向证明、以及暴露优化障碍三种贡献。该框架可在普通个人电脑上运行，指向计算发现…
arXiv cs.LG34 天前
★ 3
LogicTrack：用形式逻辑求解器审计推理链
论文提出LogicTrack神经符号框架，将LLM的每一步推理自动形式化为符号表示，并用自动定理证明器验证，解决模型通过逻辑缺陷链得出正确答案的问题。框架引入基于求解器的回溯奖励（SBR）指导推理时树搜索，并可生成SFT数据让模型内化逐步审计能力。在8个推理基准、7个LLM上验证了推理链可验证性与…
arXiv cs.AI41 天前
★ 3
ContrAgent：用契约对 LLM 智能体做符号时序监督
论文针对 LLM 智能体工具调用中的幻觉、分布不稳与对抗操纵风险，指出现有防护要么事后用随机 LLM 评判轨迹，要么逐次拦截动作，缺乏统一确定性产物。作者提出 ContrAgent，用 LTLf 假设-保证契约将行为编译为确定性有限自动机，同时支持在线门控与离线评估。在四个基准上匹配最先进基线，且…
arXiv cs.AI45 天前
★ 3
FaithSieve：细粒度数学证明评估框架
FaithSieve利用Lean辅助验证自然语言数学证明，通过分解证明步骤和语义对齐评分，实现精确的错误定位。在奥林匹克和大学级数据集上，其准确率显著优于直接判断基线，展示了形式化证据在评估中的价值。
arXiv cs.AI65 天前
★ 2
开源工具 SpecGuardian 用形式化规范测试 AI 生成代码
开发者 mrasu 在 GitHub 发布 SpecGuardian，可将 FizzBee 形式化规范的状态转移结果转化为 Go 测试，用于校验 AI 生成的实现是否符合规范。示例展示了如何通过注入 I/O 故障发现缓存与数据库写入顺序错误。
Hacker News – AI13 小时前
★ 2
Bend 2 探讨形式化验证能否成为 AI 编程未来
视频讨论 Bend 2 与形式化验证在 AI 编程中的作用，探讨用数学证明保证生成代码正确性的路径。支持者认为形式化方法可弥补大模型生成代码的可靠性缺陷。该方向仍处探索阶段。
Hacker News – AI2 天前
★ 2
Lean 创造者 Leo de Moura 谈 AI 与形式化验证的未来
Lean 创造者 Leo de Moura 在访谈中讨论 AI 与形式化验证的结合前景，探讨大模型在数学证明与程序验证中的角色。该话题在 Hacker News 引发小范围关注。
Hacker News3 天前
★ 2
论文给出独立与负相关噪声下赢家偏差的紧界
论文研究从 M 个含噪无偏评分中取最大值导致的赢家偏差，确定了独立非同分布与两两非负相关噪声两类情形下的紧常数，并在 448 个模型与分类器选择流程上验证。所有定理均在 Lean 4 中形式化验证，并给出交叉验证估计偏差的紧界。
arXiv cs.LG6 天前
★ 2
Bend 语言开源：用证明阻止 AI 写错代码
GitHub 项目 Bend 发布一门面向后 AGI 时代的新编程语言，通过 LAWS.bend 声明规则并要求编译器生成数学证明，从而机械验证 AI 生成的代码是否符合意图。项目宣称编译速度接近 C、可全量运行在 GPU 上，并能在一秒内完成其他证明助手需数分钟的校验。
Hacker News – AI7 天前
★ 2
UPA 开源：面向人与 AI 的显式组织模型
开发者发布开源项目 UPA，将业务规则、工作流、系统、证据与假设表示为机器可读结构，供人与 AI 智能体共同检视，并用 Z3 对模型属性做形式化验证。项目定位为「机器可读的组织大脑」实验。
Hacker News – AI9 天前
★ 2
新方法用 Lean 4 编译器报错修复定理证明，解出率提升 32%
论文提出有界在线步骤级修复模块：每步采样 K 个策略，失败时把 Lean 4 编译器错误信息喂给预训练修复模型就地修正，而非丢弃重采样。在 LeanDojo 1990 条定理子集上最多取得 32% 相对提升、多解出 82 条定理，收益主要来自浅层策略执行错误。该方法在 Lean Workbook …
arXiv cs.AI11 天前
★ 2
博客：用 TLA+ 规范引导 AI 生成代码
一篇技术博客提出「蓝图而非提示词」的思路，主张先用 TLA+ 形式化规范描述系统行为，再让 AI 依据规范编写代码。该方法旨在提升 AI 生成代码的正确性与可验证性。
Hacker News – AI12 天前
★ 2
高斯加权脊波变换给出无限维神经网络构造性通用逼近
论文将脊波变换扩展到可分无限维希尔伯特空间上的连续映射，用高斯权重替代无穷维中不存在的勒贝格测度，得到 Plancherel 恒等式与重构公式。由此对包括 ReLU 在内的多项式增长激活函数给出紧集上的一致逼近，并附 Lean 4 机器验证证明。
arXiv cs.LG12 天前
★ 2
Cortex：编码智能体的定点治理理论技术报告
论文研究 Cortex 这一编码智能体监督层，负责执行前治理、需求追踪与迭代验证修复，并在有限格上形式化需求闭合，证明穷举迭代可达到最小不动点。报告同时定义 Gauntlet 轨迹相似度与构建门控评分等评估方法，但作者指出观测集不均与溯源不完整限制了因果结论。
arXiv cs.AI12 天前
★ 2
研究：正确性反馈削弱 Verus 规格完整性审计证据
arXiv 论文在 12 个 Verus/Rust 任务、四个模型家族上发现，正确性反馈会抑制规格完整性审计本应发现的证据：无反馈独立发现的认证见证产出率 59.0%，远高于 IntentShield 纠正反馈循环的 27.1%。保留这些见证可带来更强的规格修复效果，Phase-Revised 合…
arXiv cs.AI16 天前
★ 2
AdaCore 展示 AI 生成代码的形式化验证与可信开发
AdaCore 发布博客介绍 GNAT Foundry 与形式化证明结合，用于验证 AI 生成代码的可信度。目标是让 AI 辅助开发的代码具备确定性信任与形式化保证。
Hacker News – AI18 天前
★ 2
Vosti：确定性大模型推理的规约、实现与验证
一篇arXiv论文提出Vosti，用于规约、实现并验证确定性的大语言模型推理过程。该工作关注推理结果的可复现性与形式化验证，对可靠部署LLM有潜在意义。
Hacker News – LLM24 天前