Leanstral 模型发布:6B 活跃参数刷新数学证明 SOTA
Bam4d · x · 2026-08-07
Leanstral 是一系列针对 Lean 4 的通用代码智能体模型，总参数量 119B 但仅激活 6B。它直接在开源的 Mistral Vibe 代码智能体框架中运行，无需复杂的证明脚手架，仅通过上下文压缩和增加测试时计算即可平滑提升性能。
尽管体量不大，该模型在多项基准测试中表现优异：在 miniF2F 上达到饱和，在 PutnamBench 解决了 587/672 道题，并在 FATE-X 和 FLTEval 上分别创下 34% 和 43.2% 的新纪录。此外，基于该模型构建的自动化流水线还在真实开源仓库中发现了此前未知的 Bug。模型已基于 Apache-2.0 协议开源。
趣闻：作者在推文中吐槽，这篇论文此前因“科学贡献不足”被 arXiv 拒稿，随后才发布在 alphaXiv 上。
「编程与Agent」频道最新
- Stripe 展示 MCP 协议实测：用 iMessage 让 AI 助手直接买单 — jeff_weinstein · 2026-08-07
- Vercel 推出一行命令安装的 Agent 原生集成市场 — zeeg · 2026-08-07
- 开源安卓自动化工具 Taktik：多平台防封控评与私信 — tom_doerr · 2026-08-07
- 用 Python Hook 强制 Claude Code 遵守代码风格规范 — chaumian · 2026-08-07
- 多模型协同工作流：Kimi 编排、DeepSeek 执行、GPT 审查 — max_paperclips · 2026-08-07
- Cloudflare 实践：用 AI 子智能体将 Astro 开放 Issue 降 85% — JeremyCMorgan · 2026-08-07