HackerNews中文版

简而言之：我正在开发一个名为 OpenATP 的 Python 包 [1]，它为 Lean 中的自动定理证明提供了一个通用接口。在最新版本中，我添加了对 Leanstral 1.5 [2,3]、Grok 和 Kimi Code [4] 的支持。我惊讶地发现，Grok 的准确性与 Claude Code 和 Codex 竞争，同时在时间和成本上都更具优势。有关更多详细信息，请参见本文的其余部分和 OpenATP 文档 [5]。自动定理证明器接受形式化的声明（如 Lean 中的证明助手），并尝试合成证明。毫无疑问，大型语言模型（LLMs）已成为这一任务的主流方法。许多人专门为定理证明微调了 LLM，例如 Mistral 的 Leanstral 1.5 模型。然而，最近的一些论文表明，通用的前沿模型在编码环境中与这些专用模型竞争，有时甚至超越它们 [6,7]。在我自己的研究中，我成功地使用 Claude Code 和 Codex 作为自动定理证明器。随着最近几个月新模型和环境的发布，我对它们在准确性和时间/成本方面的比较产生了好奇。我在进行基准测试时遇到了两个主要问题： - 我需要根据订阅计划进行计费，以使其变得可负担。 - 编译 Lean 需要大量内存，我需要一种便宜的方法来远程并行运行多个独立的代理。我创建了一个名为 OpenATP 的开源 Python 包 [1] 来解决这两个问题。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 --------------------------------- 证明器准确率时间成本 t/o --------------------------------- 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 --------------------------------- 证明器准确率时间成本 t/o --------------------------------- 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 是一个出乎意料的优秀自动定理证明器。