标签
MathAdv 是一个用于数学形式定理证明的诊断基准，覆盖13个领域，并提供辅助任务以评估知识、推理和鲁棒性。该研究揭示了形式化瓶颈以及模型间的性能差异。
Proofcraft公司已完成seL4微内核在AArch64架构上的形式化安全证明（包括机密性），并宣布为RISC-V架构验证了MCS seL4，同时在LICS'26会议上提交了一篇理论论文。
FormalTCS是一个用于评估大型语言模型在端到端理论计算机科学研究上的基准，揭示了显著局限性，尤其是在自动形式化方面。
文章讨论了人工智能如何加速发现，但在人类验证方面创造了瓶颈，尤其是在关键软件中，并倡导使用形式化方法来确保代码的正确性。
本文介绍了RDFdL，一个将RDF与微分动态逻辑集成的框架，以实现对信息物理系统中静态知识和动态行为的推理。
这篇综述论文回顾了38项关于安全LLM代理的研究，强调了关键挑战，如规范翻译瓶颈、运行时监控等执行方法的不完全安全保障，以及阻碍安全任务完成的验证者税。
这篇文章反映了前沿大语言模型和Lean自动化如何大幅减少了编程语言研究中形式化证明所需的工作量，导致会议投稿数量翻倍并改变了出版规范。
本文重新审视了一篇1979年批评形式验证的论文，认为近期软件工程中基于人工智能的发展正在重新激发兴趣并挑战历史性的反对意见。
本文介绍了Keeta共识协议的建模与验证，重点在于使用形式化方法验证其在分布式系统中的正确性。
TLA+是一个模型检查工具，它通过探索所有状态交错来查找分布式系统中的缺陷；通过形式化验证，它帮助在Depot Registry的垃圾回收器中识别了一个遗漏的缺陷，从而提升了安全性。
这篇文章回顾了在Rocq中使用程序逻辑验证连续分布精确采样器的过程，详细阐述了形式验证中充分性定理面临的挑战与创新。
本文描述了通过改进YARPGen随机程序生成器用于差异测试，以在Alive2形式化验证工具中寻找遗漏警报漏洞的方法。
本文检验了多智能体系统组合可靠性界限所依据的独立性假设，发现同模型智能体以高比率共同失效，且常见的证书不健全。它提出了一种通过协同执行矩上的线性规划得到的有限样本、无依赖性的证书，并在18,000次任务上进行了验证。
陶哲轩的ICM 2026讲座《数学在AI时代》已上传至YouTube，探讨了AI、形式化验证和协作平台如何改变数学实践，同时也指出了它们目前的局限性。
This paper argues that semantic safety constraints are off-support objects not invariant under the learning problem, explaining phenomena like reward hacking and sandbox escape. It derives consequences for prior design, containment, and formal verification, using a July 2026 OpenAI–Hugging Face incident as a motivating case.
Specula是一个代理系统，能够自动从代码推导TLA+规范，运行模型检查以发现并发错误，并通过集成测试复现这些错误。它在48个开源分布式和并发系统中发现了249个错误，展示了形式化验证的显著扩展。
本文使用SAT求解证明塔斯基高中代数问题的最小反模型大小为12，提供了分类并在Lean中验证了该结果。
本文提出了DNSSE，一种混合框架，结合了基于LLM的调度预测、符号约束求解和覆盖引导的随机变异，用于验证分布式并行AI程序。它在现实基准上检测到的并发缺陷数量是基线的2.9倍，并将分支覆盖率从68.6%提高到91.6%。
与 Lean 和 Z3 的创造者 Leonardo de Moura 的访谈节目，讨论 Lean 的工作原理、LLM 在形式化验证中的作用，以及 AI 辅助证明如何改变软件开发和数学。