仅60亿活跃参数，Leanstral定理证明刷新多项SOTA
AlbertQJiang · x · 2026-08-07
Leanstral 是一个用于 Lean 4 定理证明的通用代码智能体系列模型。它总参数量达 119B，但活跃参数仅为 6B。与传统专用证明器不同，Leanstral 直接在开源的 Mistral Vibe 代码智能体框架中运行，仅依靠上下文压缩，无需复杂的测试时扩展方法，其性能随单问题 token 预算的增加而平滑提升。
尽管体量不大，该模型的成绩却媲美众多庞大且闭源的系统：
- 在 miniF2F 基准上达到饱和状态。
- 解决了 PutnamBench 中的 587/672 个问题。
- 在 FATE-X 上达到 34%，在真实仓库评测 FLTEval 上达到 43.2%，均创下新的 SOTA。
除了竞赛数学，它还能处理真实代码库中的研究生级别数学和代码验证问题。基于该模型构建的全自动化流水线甚至发现了开源软件中此前未知的漏洞。目前该模型已基于 Apache-2.0 许可证开源。
所属事件:Leanstral 模型发布刷新定理证明 SOTA(2 条相关)→
「编程与Agent」频道最新
- 实测Claude Code缓存超时陷阱：闲置一小时成本暴涨13倍 — teortaxesTex · 2026-08-07
- Cloudflare 发布 OS 平台：为每位员工配备专属 AI 智能体 — yangyi · 2026-08-07
- 开发者实测：用 Codex 语音模式为 Reachy Mini 机器人搭线束 — SergioPaniego · 2026-08-07
- 1.5人团队六周构建AI智能体，替代20年医疗计费经验 — alex_verem · 2026-08-07
- Claurst：基于 Rust 的开源终端编码智能体 — tom_doerr · 2026-08-07
- 开源 Skill 把长文转小红书图文，支持 5 种风格不漏字 — yihui_indie · 2026-08-07