HackerNews中文版

简而言之：我正在开发一个名为 OpenATP [1] 的 Python 包，它为编码代理提供了一个通用的接口，用于在 Lean 中进行自动定理证明。在最新版本中，我增加了对 Leanstral 1.5 [2,3]、Grok 和 Kimi Code [4] 的支持。令我惊讶的是，Grok 的准确性与 Claude Code 和 Codex 相当，但速度更快，成本却只有一小部分。有关更多详细信息，请参阅本文其余部分和 OpenATP 文档 [5]。自动定理证明器接收形式化陈述（在 Lean 等证明助手中使用），并尝试合成证明。不出所料，大型语言模型 (LLM) 已成为这项任务的主流方法。许多人专门为定理证明微调了 LLM，例如 Mistral 的 Leanstral 1.5 模型。然而，最近的一些论文表明，在编码环境中使用的通用前沿模型与这些专用模型相比具有竞争力，有时甚至表现更优 [6,7]。在我自己的研究中，我使用 Claude Code 和 Codex 作为自动定理证明器取得了很大成功。随着过去几个月新模型和编码环境的发布，我一直很好奇它们在准确性、时间和成本方面的比较。在尝试运行基准测试时，我遇到了两个主要问题： * 我需要通过订阅计划计费才能负担得起。 * 编译 Lean 需要大量内存，我需要一种廉价的方法来远程并行运行多个隔离的代理。我创建了一个名为 OpenATP [1] 的开源 Python 包来解决这两个问题。OpenATP 会自动将代理的 CLI 凭据转发到 Docker 容器中，以便通过订阅计划计费，并提供 Modal 后端以远程并行运行多个代理（Modal 提供每月 30 美元的免费计算额度）。有关所有支持的证明器/编码环境以及如何为每个设置凭据的详细信息，请参阅 OpenATP 文档 [5]。 OpenATP 的最新版本增加了对 Leanstral 1.5、Grok 和 Kimi Code 的支持。我对 FATE-H 和 FATE-X 数据集 [8] 的一个子集进行了一些小型基准测试，以进行比较。Kimi Code 的订阅速率限制过于严格，无法将其包含在基准测试中。在 FATE-H 上，Claude Code 和 Codex 的速度最快，每项证明约 10 分钟。它们的成本也显著更高。Aristotle [9] 是免费的，并且在两倍的时间内实现了完美的准确性。Leanstral 1.5 也是免费的，其时间和准确性与 Aristotle 相似（一次未命中是由于 60 分钟超时）。DeepSeek 非常便宜，但也是最慢的。它的速度大约是 Claude 的三倍，并且遇到了 3 次超时。 Grok 登场了！Grok 的准确性与 Claude Code 和 Codex 相当，但成本却只有一小部分，并且是实际运行时间最快的。在更具挑战性的 FATE-X 数据集上，这种差异更加明显。Grok 的速度比 Claude Code 和 Codex 快约 50%，成本便宜约 3 倍。在这些更具挑战性的问题上，最便宜的证明器开始真正遇到困难。DeepSeek 的速度比 Grok 慢 4 倍，并且遇到了 4 次超时。 FATE-H --------------------------------- 证明器准确性时间成本超时 --------------------------------- claude 10/10 9:50 $2.05 0 codex 9/10 10:00 $2.68 0 grok 10/10 8:46 $0.94 0 deepseek 7/10 28:21 $0.15 3 leanstral 9/10 23:00 免费 1 aristotle 10/10 19:39 免费 0 --------------------------------- FATE-X --------------------------------- 证明器准确性时间成本超时 --------------------------------- claude 8/9 15:43 $3.60 0 codex 9/9 14:27 $3.70 0 grok 9/9 10:42 $1.31 0 deepseek 3/9 41:48 $0.21 4 --------------------------------- [1] https://github.com/henryrobbins/open-atp [2] https://news.ycombinator.com/item?id=48780801 [3] https://mistral.ai/news/leanstral-1-5/ [4] https://news.ycombinator.com/item?id=48935342 [5] https://open-atp.henryrobbins.com [6] https://arxiv.org/abs/2601.14027 [7] https://arxiv.org/abs/2602.24273 [8] https://github.com/frenzymath/FATE [9] https://aristotle.harmonic.fun

查看原文

TL;DR: I'm working on a Python package called OpenATP [1] that provides a common interface to coding agents for automated theorem proving in Lean. In the latest release, I added support for Leanstral 1.5 [2,3], Grok, and Kimi Code [4]. I was surprised to find that Grok has accuracy competitive with Claude Code and Codex at faster wall-clock times and a fraction of the cost. See the rest of this post and the OpenATP docs [5] for more details.Automated theorem provers take formal statements (in a proof assistant like Lean) and attempt to synthesize a proof. Unsurprisingly, LLMs have become the dominant approach to this task. Many have fine-tuned LLMs specifically for theorem proving, like Mistral's Leanstral 1.5 model. However, a number of recent papers have shown that general-purpose frontier models in a coding harness are competitive with, and sometimes outperform, these specialized models [6,7].In my own research, I've had a lot of success using Claude Code and Codex as automated theorem provers. As new models and harnesses have been released in the last few months, I've been curious how they would compare, both in accuracy and in time/cost. I ran into two main issues trying to run benchmarks:- I needed to bill against subscription plans to make it affordable.- Compiling Lean is RAM intensive and I needed a cheap way to run multiple isolated agents in parallel remotely.I created an open-source Python package called OpenATP [1] to solve both of these problems. OpenATP automatically forwards agent CLI credentials into a Docker container to bill against subscription plans and it offers a Modal backend to run multiple agents in parallel remotely (Modal offers $30/month in free compute). See the OpenATP docs [5] for all of the supported provers / harnesses and how to set up credentials for each.The most recent release of OpenATP added support for Leanstral 1.5, Grok, and Kimi Code. I ran some small benchmarks on a subset of the FATE-H and FATE-X datasets [8] to compare them. The Kimi Code subscription rate limits were too restrictive to include it in the benchmark.On FATE-H, Claude Code and Codex are the fastest at ~10 minutes per proof. They are also significantly more expensive. Aristotle [9] is free and achieves perfect accuracy in 2x the time. Leanstral 1.5 is also free and has similar time and accuracy to Aristotle (the one miss was due to 60 min timeout). DeepSeek is incredibly cheap, but is also the slowest. It's roughly 3x slower than Claude and hits 3 timeouts.In comes Grok! Grok achieves accuracy comparable to Claude Code and Codex, but at a fraction of the cost and the fastest wall-clock time. The difference on FATE-X, a more challenging dataset, is even more pronounced. Grok is ~50% faster and ~3x cheaper than Claude Code and Codex. On these more challenging problems, the cheapest provers really begin to struggle. DeepSeek was 4x slower than Grok and hit 4 timeouts.FATE-H---------------------------------prover acc. time cost t/o---------------------------------claude 10/10 9:50 $2.05 0codex 9/10 10:00 $2.68 0grok 10/10 8:46 $0.94 0deepseek 7/10 28:21 $0.15 3leanstral 9/10 23:00 free 1aristotle 10/10 19:39 free 0---------------------------------FATE-X---------------------------------prover acc. time cost t/o---------------------------------claude 8/9 15:43 $3.60 0codex 9/9 14:27 $3.70 0grok 9/9 10:42 $1.31 0deepseek 3/9 41:48 $0.21 4---------------------------------[1] https://github.com/henryrobbins/open-atp[2] https://news.ycombinator.com/item?id=48780801[3] https://mistral.ai/news/leanstral-1-5/[4] https://news.ycombinator.com/item?id=48935342[5] https://open-atp.henryrobbins.com[6] https://arxiv.org/abs/2601.14027[7] https://arxiv.org/abs/2602.24273[8] https://github.com/frenzymath/FATE[9] https://aristotle.harmonic.fun

Grok 是一个出人意料的优秀自动定理证明器。