Leanstral 1.5 dari Mistral tembus benchmark bukti matematika dan temukan bug nyata

Mistral merilis Leanstral 1.5, model open yang dirancang untuk menulis bukti formal di Lean 4. Angka utamanya: model ini menembus miniF2F sampai 100% di set validasi maupun test, benchmark yang sampai belakangan ini belum ada sistem yang bisa menuntaskannya. Model ini juga menyelesaikan 587 dari 672 soal di PutnamBench dan mencapai 87% di FATE-H untuk aljabar abstrak. Arsitekturnya mixture-of-experts dengan 119B parameter total tapi hanya 6B yang aktif, dirilis di bawah lisensi Apache-2.0, dan sudah tersedia sebagai API endpoint gratis serta di Hugging Face.

Bagian yang lebih menarik muncul saat model diberi ruang berpikir lebih banyak. Di PutnamBench, model menyelesaikan 44 soal dengan budget 50k token dan naik ke 587 soal pada 4 juta token, contoh jelas test-time scaling. Kemampuannya juga tidak berhenti di soal kontes. Diarahkan ke repositori open-source nyata, model menemukan sejumlah cacat, termasuk 5 yang belum pernah dilaporkan di GitHub. Salah satunya fungsi zigzag decoding di mana ekspresi (value + 1) mengalami overflow, membuat crash di mode debug dan diam-diam merusak data di mode release. Menjalankan seluruh set PutnamBench menghabiskan sekitar $4 per soal.

Kenapa ini penting

Kalau kamu menulis kode yang kebenarannya bisa dispesifikasikan, seperti kriptografi, parser, atau library low-level, sebuah proof engine yang menemukan bug overflow nyata dan hadir dengan open weights adalah sesuatu yang bisa kamu arahkan ke kode kamu sendiri sekarang, bukan sekadar demo. Hasil temuan bug itulah alasan untuk mencobanya, bukan skor benchmark-nya.