Leanstral 1.5 dari Mistral: model open-weight yang membuktikan teorema dan menemukan bug nyata

Mistral merilis Leanstral 1.5, model open-weight yang dibangun untuk pembuktian formal di Lean 4, dan angkanya luar biasa konkret. Model ini meraih 100% pada set validasi dan test miniF2F serta menyelesaikan 587 dari 672 soal PutnamBench, sebuah benchmark yang diambil dari matematika kompetisi. Total parameternya 119B tapi hanya 6B yang aktif pada satu waktu, dan weight-nya tersedia di Hugging Face dengan lisensi Apache-2.0 plus endpoint API gratis.

Yang membuatnya layak diperhatikan di luar tabel benchmark adalah cara kerjanya sebagai agent. Ia menyunting file bukti dan membaca umpan balik dari language server Lean untuk memperbaiki percobaannya, dan performanya naik seiring compute: diberi anggaran 4 juta token alih-alih 50.000, jumlah soal yang diselesaikan melonjak dari 44 menjadi 587. Pada satu bukti soal AVL tree, ia menembus lebih dari 2,7 juta token lewat 22 kali pemadatan bukti. Ia juga menemukan bug integer overflow nyata di datrs/varinteger, sebuah repo Rust aktif, saat memverifikasi kode, bukan sekadar mengerjakan latihan. Menurut Mistral, pada FLTEval model ini mengungguli Claude Opus 4.6 dengan biaya sekitar sepertujuhnya.

Kenapa ini penting

Kalau kamu menulis software yang kebenarannya harus dibuktikan, bukan hanya diuji, model open yang menjalankan verifikasi formal secara agentic sekaligus menemukan bug nyata adalah sesuatu yang kini bisa kamu coba tanpa membayar lab frontier. Selisih biaya terhadap model tertutup pada tugas yang sama adalah angka yang perlu ditimbang terhadap workload kamu sendiri sebelum memutuskan.