仅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」频道最新
- DHH 深圳行：Omarchy Meetup 超 400 人报名，小米高管现场演示 — LoganGrasby · 2026-10-16
- shadcn 转发 ShadHub：GitHub Registry 目录站上线，可即时提交收录 — shadcn · 2026-10-16
- Sarvam 联手 Figma:基于 Indus 的 Agent 可经 MCP 直接在 Figma 里做设计 — itsOmSarraf_ · 2026-10-16
- 独立开发者给 Mac VM 应用加 MCP：让 agent 搞坏一次性克隆而非真机 — ScholarBackground836 · 2026-10-16
- ComfyUI 拖拽失效排查：第三方节点包劫持 drop 事件 — Inside_Chocolate_967 · 2026-10-16
- 为什么别人家的AI很强你的很拉：Agent四件套拆解 — yangyi · 2026-10-16