标签
介绍 Leanstral 1.5，一个119B参数（6B活跃）的开放模型，用于Lean 4的形式化证明工程，在miniF2F上达到100%，在PutnamBench和FATE基准测试上达到最先进分数，并发现了开源仓库中先前未知的漏洞。
今天，我们发布 Le Chaton L∃∀N，即 Leanstral 1.5。它在研究生代数基准测试 FATE-H 和 FATE-X 上实现了 SOTA 性能，并在 PutnamBench 上改进了帕累托前沿（Pareto Frontier），以 x10 更低的预算解决了 587/672 个问题。