标签
本文提出了一种用于Lean 4上下文依赖定理证明的编译器引导自适应证明搜索框架，利用跨模型协同来提高证明成功率并降低计算成本。
MathForm引入了一个利用知识检索和验证引导优化的数学自动形式化框架，产生了FormalVerse数据集和一个8B模型，该模型在性能上优于专业基线模型。
PULSE is a new executable contract language for spatiotemporal knowledge graph engineering, providing a typed runtime with role-based write effects, safety properties verified in Lean 4, and trace parity across large datasets.
OpenAI使用内部模型Astra解决了十个停滞了十多年的数学问题，每个问题花费不到2000美元，并发布了Lean 4形式化证明及一篇论文。这些结果引发了对AI在数学中作用的反思。
本文揭示了图神经网络top-k解释中的一个根本问题：输入图中的自同构导致解释不唯一，因为模型无法区分对称元素。作者提出了一个检测这种任意性的标准，并利用Lean 4中的自动推理对其进行了验证，表明该问题在分子数据集中广泛存在。
一种基于 Google Zanzibar 的 datalog 语言开发的 Lean4 DSL，用于表示和评估知识库，可在 git 下管理，无需重型外部依赖。
一个在 Lean 4 中实现的形式化验证的3D网格交集算法，只需审查93行规范，信任 Lean 检查器而非1000多行AI生成的代码。它展示了一种减少人工审查工作同时确保正确性的新颖方法。
本文介绍了为ARCH HDL（一种面向AI模型生成的硬件描述语言）设计并端到端形式化验证IEEE-754 binary32和bfloat16算术。这些算子通过结合穷举SMT等价性检查和Lean 4证明的混合方法，被证明具有正确的舍入，并输出可综合的SystemVerilog。
本文介绍了Demonstrandum，一个验证优先的多智能体AI数学流水线，能够生成机械可验证的制品，包括通过Lean 4内核验证的反例和猜想证明。
OpenProver 是一个开源系统，利用 Lean 4 进行 LLM 驱动的自动定理证明，采用规划器-工作器-验证器架构，并支持自主和交互两种模式。它实现了数学证明搜索中的可重复评估和人机协同。
本文报告了一个验证流水线的经验，该流水线使用AI证明器（Aristotle和Aleph）结合符号提取工具和形式化密码学库，为Lean 4中的Rust密码学代码生成机器检查的正确性证明，并提供了来自以太坊基金会zkEVM项目的案例研究。
介绍 Leanstral 1.5，一个119B参数（6B活跃）的开放模型，用于Lean 4的形式化证明工程，在miniF2F上达到100%，在PutnamBench和FATE基准测试上达到最先进分数，并发现了开源仓库中先前未知的漏洞。
自动化定理证明正从像 Lean 4 这样的小众工具演变为借助机器学习来帮助解决实际数学问题的系统，例如验证一个对 Erdős 猜想的反例。
Mistral AI 发布了 Leanstral 1.5，这是更新的 Lean 4 形式化证明工程模型，针对自动定理证明和自动形式化进行了优化，总参数为 119B，活跃参数为 6.5B。
本文使用演化博弈论对社区中一个最小化危害的AI代理与一个寻求认可的（RLHF）代理之间的竞争进行建模，分析采纳条件和福利结果。结果表明，尽管自我审计的代理可以占据主导，但这并不足以防止社区危害，且对齐和时间框架至关重要。
Ansatz 是一个 Clojure 库，实现了 Lean 4 的归纳构造演算内核，使 Clojure 程序员能够编写依赖类型的、经过验证的代码，这些代码的证明与 Mathlib 兼容，并能编译为 JVM 字节码。
本文提出了一种基于闭合循环回路的完全架构规范，用于安全的AGI，提供了形式化证明、Lean 4机器验证以及Python代码。该架构与当前前馈方法形成对比，从数学上保证了自我建模、自我保存和安全的目标导向行为。
本文评估了在全局和局部扰动下，Lean 4中证明自动形式化模型的鲁棒性，发现当前基于LLM的模型对扰动敏感，且常常无法忠实地反映局部变化。
本文提出了一种用于在 Lean 4 中形式化数值分析教材的智能体流水线，并引入了一个超越内核接受的质量审计框架，用于评估语义正确性和库复用情况，揭示了常见的不忠实形式化模式。