mistralai/LeanstralSafeVerify

来源：https://github.com/mistralai/LeanstralSafeVerify

SafeVerify

该脚本的目的是检查提交的 Lean 代码和/或证明文件是否符合规范。与直接使用 Lean 编译器或 REPL 进行验证相比，这种方法更安全，因为它能够防范潜在的漏洞利用，包括通过元编程操纵环境、使用额外公理以及利用有缺陷的策略（tactics）。目前，它作为以下项目的证明验证后端：

• Provably-Correct Vibe Coding (http://ProvablyCorrectVibeCoding.com)，一个用于 Lean 的边编程边验证的 Web 应用；
• Code with Proofs: the Arena (https://github.com/GasStationManager/CodeProofTheArena)，一个包含正确性证明的编程问题网站；
• TheoremMarketplace (https://github.com/wadimiusz/lean-contract-interact)，定理悬赏的智能合约。

minif2f-deepseek-check 分支包含一个回溯到 Lean 4.9.0 的版本，可用于验证 DeepSeek Prover V2 对 MiniF2F 的解答（https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main）。类似地，minif2f-kimina-check 分支包含一个使用 Lean 4.15.0 的版本，可用于验证 Kimina-Prover-Preview 和 Kimina-Prover 对 MiniF2F 的解答（https://github.com/MoonshotAI/Kimina-Prover-Preview）。abc-trinity-check 分支包含一个使用 Lean 4.20.0 的版本，可用于验证 Trinity 对 ABC 猜想的 de Bruijin 界的形式化（https://github.com/morph-labs/lean-abc-true-almost-always/）。seed-prover-check 分支包含一个使用 Lean 4.14.0 的版本，可用于验证 Seed Prover 已发布的解答，包括 IMO 2025（https://github.com/ByteDance-Seed/Seed-Prover/tree/main/SeedProver）。SafeVerify 已被 PutnamBench 的官方排行榜（https://trishullab.github.io/PutnamBench/leaderboard.html）用于验证部分已提交的解答。

这是创建安全、无幻觉的编程 AI 的更广泛努力的一部分（https://gasstationmanager.github.io/ai/2024/11/04/a-proposal.html）。

更详细地说：该脚本接收两个 olean 文件，并检查第二个文件是否实现了第一个文件中指定的定理和定义。第一个文件（目标文件）可能包含带有 sorry 的定理/函数签名；第二个文件应填充它们。使用 Environment.replay 来防御对环境的操纵。检查第二个文件中的定理，确保它们仅使用三个标准公理。

大部分代码改编自 lean4checker（https://github.com/leanprover/lean4checker/）。并采纳了 Lean Zulip（https://leanprover.zulipchat.com/）上用户的建议。

脚本执行的检查列表

• 对两个输入文件，通过 Environment.replay 运行文件内容。
  • 这与 lean4checker 执行的检查相同，即用内核重新检查每个声明。如果某个声明不被内核接受（可能由于环境操纵），则会抛出异常。
  • 此操作仅重放文件内容，不包括导入。若要同时重放导入，需要修改脚本以匹配 lean4checker --fresh 的行为。
• 剩余检查在两个文件的重放环境上进行。这确保了检查不受任何环境操纵的影响。
• 对目标文件中的每个声明，确保提交文件中存在同名、同类型（def / theorem）且同类型的声明。
• 对于定义，还要检查其主体是否相同。但目标文件中的定义依赖于 sorry 的情况除外，此时允许提交文件中的定义主体不同。
  • 这旨在同时处理两种情况：完整的定义（不应被修改）以及带有 sorry 的定义存根（需要被填充）。
  • 如果有一个完整的函数 g，但其主体中调用了包含 sorry 的函数 f，那么函数 g 也依赖于 sorry，因此其主体（而非类型）可以被修改。如果不希望 g 被修改，一种方法是让 g 以函数（具有 f 的类型）作为输入，或者使用其他机制来标识哪些定义/定理允许被修改。
• 检查提交文件中的定义和定理，确保它们仅依赖于三个标准公理：propext、Quot.sound、Classical.choice。
  • 使用 CollectAxioms.collect。
  • 可以修改脚本中的 AllowedAxioms 列表来收紧或放宽允许的公理集合。
• 对目标文件或提交文件中的每个定义，如果标记为 partial 或 unsafe，则抛出异常。
  • 此要求可能更特定于验证带有正确性证明的编程任务解答（https://github.com/GasStationManager/CodeProofTheArena）的使用场景。在这些场景中，使用 partial/unsafe 函数可能导致无限循环，但满足类型要求。

SafeVerify 未检查的项（您可能需要通过其他方式检查）：

• 像 implemented_by、extern、noncomputable 等关键字：在 SafeVerify 操作的 olean 文件层面很难捕获，但根据用例，您可以选择在源代码层面扫描并禁用它们。请参见例如 CodeProofTheArena 中的 judge.py（https://github.com/GasStationManager/CodeProofTheArena/blob/main/app/services/judge.py）。

用法

第一步是将 Lean 文件编译为 .olean 文件。例如： lake env lean -o submission.olean submission.lean 然后将 olean 文件传递给工具： lake env lean --run Main.lean target.olean submission.olean

构建可执行文件

lake build 将脚本构建为可执行文件，位于 .lake/build/bin/safe_verify。然后可以通过以下命令运行可执行文件： lake exe safe_verify target.olean submission.olean