Leanstral 1.5是一款免费开源的6B参数模型，在形式验证领域取得重大突破，在miniF2F、PutnamBench等基准测试中表现优异，并发现57个开源仓库中的5个未知漏洞，现已通过Hugging Face和免费API开放使用。

好的，这是根据您的要求，对原文进行中文重述和精简后的版本：

标题：Leanstral 1.5：为所有人提供丰富的证明能力

核心摘要： Leanstral 1.5 是一个免费、采用 Apache-2.0 许可的模型，拥有 119B 总参数和 6B 活跃参数。它在形式化验证领域实现了重大性能提升，在 miniF2F 基准测试中达到饱和，解决了 PutnamBench 中 672 个问题中的 587 个，并在 FATE-H（87%）和 FATE-X（34%）上取得了最先进的结果。该模型通过中期训练、监督微调和基于 CISPO 的强化学习进行训练，在智能体证明工程和真实世界代码验证方面表现出色，在测试的 57 个代码仓库中发现了 5 个先前未知的错误。Leanstral 1.5 现已完全开源，可通过 Hugging Face 和免费 API 获取，用于 Lean 4 中的实际证明工程。

训练过程： Leanstral 1.5 的训练分为三个阶段：中期训练、监督微调和基于 CISPO 的强化学习。它利用了两个强化学习环境： 1. 多轮环境：模型根据给定的定理陈述，通过提交证明、接收 Lean 编译器反馈并反复优化，直到证明通过或预算耗尽。 2. 代码智能体环境：模型像开发者一样操作原始文件系统，可以编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标、错误和类型信息。这使其能够处理长期任务，如完成仓库中的部分证明、构建辅助引理，并在多次上下文压缩中持续工作。

评估结果： * miniF2F：在验证集和测试集上均达到 100% 的饱和状态。 * PutnamBench：解决了 672 个问题中的 587 个，每个问题的成本约为 4 美元，远低于其他模型（如 Seed-Prover 1.5 的 300 美元以上）。 * FATE-H/X：分别解决了 87 和 34 个问题，达到了新的最先进水平。 * FLTEval：在基于真实世界复杂性的基准测试中，pass@1 从 21.9 提升至 28.9，pass@8 从 31.9 提升至 43.2，超越了成本高得多的 Opus 4.6 模型。 * 测试时扩展：随着每个尝试的 token 预算从 25k 增加到 4M，模型性能持续且单调地提升，证明了其强大的推理能力。

代码验证案例研究： 1. AVL 树时间复杂度证明：Leanstral 1.5 成功证明了一个真实 AVL 树实现的时间复杂度保证（O(log n)）。该证明过程使用了超过 270 万个 token，经历了 22 次上下文压缩，通过结构归纳和详尽的情况分析，最终完成了插入和删除操作的时间复杂度验证。 2. 发现隐藏错误：通过一个自动化流程，Leanstral 在 57 个测试仓库中发现了 47 个被违反的属性，其中 11 个指向了真正的错误，5 个是之前未在 GitHub 上报告过的。例如，它在 datrs/varinteger 库的 zigzag 解码符号函数中发现了一个因整数溢出导致的错误，这种边缘情况通常会被测试和模糊测试所遗漏。

如何开始： Leanstral 1.5 采用 Apache-2.0 许可，权重可在 Hugging Face 上获取，并可通过免费 API 端点 leanstral-1-5 使用。推荐使用 Mistral Vibe 工具。基本步骤包括：安装 Mistral Vibe、安装 Leanstral 1.5、启动智能体、可选安装 Lean LSP MCP，然后即可开始要求 Leanstral 处理定理、调试证明或为代码仓库做出贡献。

以下是对评论内容的总结，重点关注主要观点、论据及不同立场的平衡性，并保留关键引用（中英文）。

1. 对“bug发现示例”的质疑与辩护

• 质疑观点：评论1和7认为，文章提到的边界条件bug（Std.U64.MAX溢出）并非“测试通常遗漏”的典型例子，而是基础测试应覆盖的极端值。评论1指出：“It's certainly something that bad tests would miss or not think about, but I find that (a) careful people and (b) ML coding systems are actually really good at 'oh, I should test the extreme values'.” 评论7补充，该库“tiny, surprisingly-poorly tested, long-untouched (8y)”，且类似问题在发布前一周已被报告，因此示例说服力不足。
• 辩护观点：评论4（OpenAI员工）测试后认为，该bug“wasn't especially tricky; it's just a case of too few eyeballs on this repo”，但仍肯定自动化检测的价值。评论7也承认“automated detection is certainly useful”。

2. 对模型性能比较的批评

• 评论8指出，文章中的模型对比仅使用了半年前的旧模型，显得不够严谨：“'Our new model is better than all these Chinese models from 3 generations ago' is pretty funny to me.”

3. 对提示工程（Prompt Engineering）的讨论

• 评论3建议，专用模型应提供多样化的输入示例和提示构建指南，因为“you can get wildly different quality results from these sorts of models due to seemingly insignificant differences in prompt construction.” 作者认为模型作者最有资格提供初始建议。

4. 对Lean语言及形式化验证方向的评价

• 评论6表达了对Lean语言的热情：“Lean is such a wonderful language. So hyped by these releases.”
• 评论9则提出疑问，为何选择Lean 4而非Isabelle/HOL或TLA+进行形式化验证，并期待更多工具支持。

5. 对欧洲AI发展差距的担忧

• 评论10认为，欧洲在AI领域已落后，且差距可能难以弥补：“Europe is far far behind... the best and the brightest from Europe have no incentive to build in Europe when they can do it in America.”

总结：评论主要围绕模型示例的典型性、性能比较的时效性、提示工程的重要性、Lean语言的选择合理性，以及欧洲AI发展现状展开。多数评论对技术方向持肯定态度，但对具体示例和比较方法提出质疑。