主题
形式化验证
用经机器检查的数学证明，表明神经网络、程序或 AI 生成的代码在适用范围内的所有输入上都满足精确的规约。
只要信任证明检查器（如证明助手或验证器），任何拿到证明的人都能确认某项性质对适用范围内的所有输入成立，无需依赖写出证明的人或 AI。在 AI 领域，这类证据有三种形式。关于神经网络的证明，可以说明某个输入区域内的鲁棒性等性质。机器检查的证明可以说明 AI 生成的代码满足其规约。在“可保证安全的 AI”构想中，验证器相对于安全规约和世界模型出具数学证明证书，世界模型描述系统如何影响其所处的环境。数学证明只能确立系统符合其规约，因此规约中的错误或遗漏会原样带入保证之中。对当前的 AI 智能体来说，整个代码仓库规模的验证也仍然困难。
报道
Anthropic 称 Claude 写出费马大定理的完整 Lean 证明
Anthropic 于 2026 年 9 月 4 日表示，Claude 智能体用 11 天写出了费马大定理的完整 Lean 证明，代码约 1300 万行。证明已经公开，配套文档列出了它通过的各项检查，以及重复这些检查所需的计算资源。
来源日期 本站刊发 verifiable.pro 快讯，自动采编。
VNN-COMP 2026 结果出炉：α,β-CROWN 居首，首次参赛的 Vibecheck 位列第二
国际神经网络验证竞赛于 7 月 24 日公布 2026 年结果，α,β-CROWN 在两个赛道均排名第一。据石溪大学介绍，排名第二的 Vibecheck 用了大约两个月开发完成，代码由 Anthropic 的 Claude 生成。
来源日期 本站刊发 verifiable.pro 快讯，自动采编。
Math, Inc. 称旗下 AI 系统 Gauss 完成 Viazovska 球堆积证明的 Lean 形式化
Math, Inc. 于 2026 年 3 月表示，旗下 AI 系统 Gauss 已完成 Maryna Viazovska 8 维和 24 维球堆积证明的 Lean 形式化，这些证明曾为她赢得菲尔兹奖。8 维部分的工作有人类撰写的蓝图作指引，24 维情形则没有，因此后者的形式化命题最需要独立审查。
来源日期 本站刊发 verifiable.pro 快讯，自动采编。
Towards Verified Artificial Intelligence
简介
一篇纲领性论文，从形式化方法（用数学手段描述和验证系统的技术）的角度界定“经验证的人工智能”（Verified AI）。论文提出五项挑战和相应的五条原则。
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
简介
将“可保证安全的 AI”定义为一类方法，这类方法结合世界模型、安全规约和验证器。世界模型以数学方式描述 AI 系统如何影响外部世界。验证器提供可审计的数学证明证书，表明相对于该世界模型，AI 系统满足安全规约。
Provably safe systems: the only path to controllable AGI
简介
立场论文，主张在构建通用人工智能时，应确保能用数学证明它满足人类设定的要求。作者提出借助先进 AI 完成形式化验证和机制可解释性分析；后者研究模型的内部机制。
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
简介
基于单纯形法的 SMT 技术，面向采用 ReLU 激活的神经网络。它要么证明网络满足给定性质，要么找出反例。该技术在机载防撞系统原型（ACAS Xu）的网络上做了评估。
alpha-beta-CROWN
简介
基于线性界传播和分支定界的 GPU 加速神经网络验证器。其 README 称，它赢得了 2021 年至 2026 年历届 VNN-COMP（年度神经网络验证竞赛）。
The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results
简介
关于 2025 年度神经网络验证竞赛的报告。该竞赛每年举办，在统一的 ONNX 和 VNN-LIB 基准上比较各类验证器。本届有 8 支队伍参赛。
Lean
简介
开源编程语言和证明助手；证明助手是逐步检查证明的软件。Lean 用于编写经过形式化验证的代码和机器检查的数学证明，也是 AI 生成证明的常用目标语言。
Dafny
简介
支持验证的编程语言，其静态验证器在代码运行前依据规约检查代码。Dafny 程序可编译为 C#、Java、JavaScript、Go 和 Python 等语言。
Verus
简介
用于验证 Rust 代码的工具：开发者编写规约和证明，由自动求解器检查代码在所有可能的执行中都满足规约。
DafnyBench: A Benchmark for Formal Software Verification
简介
包含 750 多个 Dafny 程序的基准，测试语言模型能否生成 Dafny 验证器所需的验证提示（hints）。发布时，最佳模型与提示组合的成功率为 68%。
A benchmark for vericoding: formally verified program synthesis
简介
包含 12504 条 Dafny、Verus/Rust 和 Lean 形式化规约的基准，用于评测生成形式化验证代码的能力。现成模型在三种语言上的成功率分别为 82%、44% 和 27%。
Vero: Can AI Agents Build Formally Verified Software Repositories?
简介
包含 43 个多模块 Lean 4 任务的仓库级基准，要求智能体同时写出实现和证明。智能体也可以证明某条规约无法满足。最强的智能体完整解决了 27 个任务。
Safeguarded AI
简介
英国高级研究与发明局（ARIA）的项目，投入 5900 万英镑。项目正在构建一套开源工具，供 AI 智能体生成经过形式化验证的成果，目前主要应用于网络安全领域。
Olympiad-level formal mathematical reasoning with reinforcement learning
简介
介绍 AlphaProof：一个受 AlphaZero 启发的智能体，通过强化学习学会在 Lean 中寻找形式化证明。它在数百万道自动转写为 Lean 的题目上训练。在 2024 年国际数学奥林匹克竞赛中，它解出了 5 道非几何题中的 3 道。它与 AlphaGeometry 2 合计达到相当于银牌的分数。
Aristotle: IMO-level Automated Theorem Proving
简介
Harmonic 的自动定理证明系统，为 2025 年国际数学奥林匹克竞赛 6 道题中的 5 道给出了形式化解答。它借助蒙特卡洛图搜索选择 Lean 策略（构造证明的命令）。其非形式推理系统负责起草并形式化引理，另有独立的求解器处理几何题。
DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
简介
开源的 Lean 4 定理证明模型。第一阶段训练所用的冷启动数据来自一条流水线，由 DeepSeek-V3 把问题分解为子目标。随后进入强化学习阶段。6710 亿参数版本在 MiniF2F-test 上的通过率为 88.9%，并解出 PutnamBench 658 道题中的 47 道。
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
简介
Lean 定理证明模型，利用 Lean 反馈、已证明的引理和自我总结迭代完善整个证明。它配合几何推理引擎 Seed-Geometry 使用。作者报告，它完整证明了 2025 年国际数学奥林匹克竞赛 6 道题中的 5 道，其中 1 道在提交截止后完成。作者还报告，它证明了 78.1% 的已形式化历届 IMO 题目。
Certified Adversarial Robustness via Randomized Smoothing
简介
证明了经高斯噪声平滑的分类器在 ℓ2 范数下的紧致鲁棒性保证；这类分类器对输入加噪后的多份副本做多数投票来预测。例如，在 ImageNet 上，对 ℓ2 范数小于 0.5 的扰动，它认证了 49% 的 top-1 准确率。由于该保证通过蒙特卡洛采样计算，它只以高概率成立。
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
简介
Marabou 2.0 的系统描述论文。Marabou 是一款开源神经网络验证器，用于检验网络性质。它借助基于 SMT 的过程求解线性和非线性约束。新版本可为无解的查询生成证明证书。它还支持更多激活函数，并可通过更完善的 Python API 提交查询。
Automated Reasoning checks is now available in Amazon Bedrock Guardrails
简介
AWS 宣布 Amazon Bedrock Guardrails 中的自动推理检查（Automated Reasoning checks）正式可用。这项防护措施用形式化验证技术，对照自动推理策略检查生成式 AI 的输出。策略中的规则从客户自己的文档中提取。
The Rocq Prover
简介
交互式定理证明器和依赖类型编程语言，前身为 Coq 证明助手。它用于编写形式化规约，以及程序符合规约的机器检查证明。它还能从规约中提取 OCaml 或 Haskell 可执行代码。
Isabelle
简介
通用证明助手，主要以基于高阶逻辑的 Isabelle/HOL 形式使用。它可检查关于数学以及硬件、软件和协议正确性的形式化证明。借助 Sledgehammer，它能调用外部自动证明器。它还配有形式化证明档案库（Archive of Formal Proofs），收录经 Isabelle 检查的证明。
Theorem Proving in Lean 4
简介
一本教材，讲解如何在 Lean 4 中编写定义和机器检查的证明，Lean 社区也为本书作出了贡献。内容涵盖依赖类型论、命题与证明、策略（tactic）、归纳类型、结构体和类型类。