标签
一篇研究论文，介绍了一种故障触发级联方法，用于将机器学习安全地集成到Lean 4的grind策略中，实现了效率提升并解决了之前无法解决的证明，且没有回归问题。
本文介绍了FVSpec，这是一个用于AI辅助形式验证的基准测试，它通过多智能体LLM管道将真实世界的基于属性测试从Python转换为Lean 4规范，旨在推动真实世界软件形式验证的进展。
Aleph Prover 已在 Lean 4 中形式化了 OpenAI 对保罗·埃尔德什平面单位问题的反证，并将其作为开源发布以供独立验证，展示了人工智能在加速数学研究中的作用，同时提供了可验证的证明数据。
本文在Clever基准的程序验证任务中，采用智能体证明框架评估Claude Code，在规范生成和端到端验证方面取得了超过98%的成功率，揭示出现有基准可能不足以评估现代智能体证明器的能力。
OProver是一个统一的框架，用于Lean 4中的代理式形式定理证明，通过使用经过验证的证明和编译器反馈进行训练，迭代地改进证明生成，在多个基准测试中取得了最先进的结果。
TorchLean 是一款全新发布的 Lean 4 框架，可实现神经网络软件的形式化验证，具备类型化张量、可验证自动微分、PyTorch 互操作性及 GPU 执行等特性。此次发布进一步扩展了对扩散模型、GPT 风格 Transformer 和状态空间模型等现代架构的支持，将实际的机器学习工作流与数学证明检查紧密连接。
本文介绍了 Discover and Prove (DAP)，一个用于 Lean 4 自动定理证明的开源智能体框架，针对"困难模式"问题进行优化——即在构造形式化证明前必须独立发现答案。该工作发布了新的困难模式基准变体，达到最先进的结果，同时揭示了 LLM 答案准确率（>80%）与形式化证明器成功率（<10%）之间的巨大差距。