标签
本文介绍了一个框架，使LLMs能够发现和证明有趣的数学定理，通过优化基于证明难度的指标，从而产生更多新颖且有用的数学知识，并减少与现有库的重叠。
本文介绍了一种在Lean中利用LLMs自动生成具有完备性形式化证明的泛化规划的方法，并在基准领域上进行了评估，展示了在自动规划验证方面的显著进步。
这条推文讨论了使用形式验证方法如 TLA+ 和 Lean 来确保关键任务 AI 基础架构软件的正确性和可扩展性，并提到了 Intent Lab 和 Boris Cherny 在 Claude Agent SDK 方面的工作。
作者使用 Claude 的 Opus 5.5 模型通过 Lean 对 Claude Agent SDK 进行了形式化验证，生成了 16 个 PR 来修复 bug 和竞态条件，并建议结合 Lean 和 TLA+ 以增强 bug 查找能力。
Trail of Bits使用AI代理为Miden零知识虚拟机开发定制的安全审计工具和形式化模型，揭示了关键漏洞并生成机器验证的正确性证明。
本文介绍了SWE-Proof，这是一个针对现实世界软件问题的经过形式验证的代码补丁基准，表明形式验证能提高LLM生成代码的错误检测能力，并将规范综合识别为一个关键开放问题。
@poteto 对 Bend 表示热情，Bend 是一种支持形式验证的语言，能够加速软件开发并解决代码审查问题，@VictorTaelin 同意其在构建无错误复杂软件方面的潜力。
本文探讨了OpenAI针对Navier-Stokes问题的Lean证明的验证，强调了确保形式证明与预期数学问题一致的重要性，以及数学家进一步审查的必要性。
本文批判了专为AI编码时代设计的编程语言Bend 2，指出其陷入了'氛围编程'的陷阱，并将其与SPARK等形式化验证方法进行了不利的比较。
MAGS引入了一种多智能体框架，利用Dafny进行形式化验证，从LLM编程智能体生成具有安全保证的可执行程序，在CUDA内核和机器人任务等多个领域实现了100%的验证代码生成成功率。
本文评估LLMs解释网络协议规范并将其映射为形式化有限状态机的能力，通过为各种协议设计的任务和查询来评估其推理能力。
Verus 是一个开源的自动化程序验证器，专为 Rust 设计，通过数学证明帮助确保代码正确性，并被亚马逊用于像 Nitro Isolation Engine 这样的项目。
StochBench 引入了一个包含 450 个研究生水平随机过程问题的领域特定基准测试，使用 Lean 4 实现，并通过一个 AI 代理评估，证明率达到 34.9%，以推进应用数学中的形式化定理证明。
从2025年到2026年事件的时间线，详细描述了合作与竞争的努力，以解决Navier-Stokes方程，最终以OpenAI宣布使用AI模型解决该问题而告终。
这篇博客文章详细描述了作者在Rocq中形式化《Dummit和Foote的Abstract Algebra》教材时发现的一个错误：关于单射函数和左逆的一个命题对空集不成立。
RePro将面向Lean的神经自动化定理证明器集成到基准重写中，以确保问题有效性和答案正确性，从而可靠评估LLMs在数学问题求解中的表现。
本文介绍了SA-Pass，一种用于评估自动形式化中语义对齐的方法，并提出了ShadowBench，一个包含178个问题的Lean 4基准测试，展示了与专家判断的高度一致性。
作者正在开发一个用于AI生成声明的确定性验证引擎，专注于形式化验证方法，并寻求研究人员和合作伙伴进行合作。
ProofEvolve是一个神经符号框架，通过使用神经模型进化形式化验证的证明结构来增强自动定理证明，通过保留来自未完成尝试的验证知识，在Lean基准测试中实现高求解率。