Leanstral 1.5: Kelimpahan Pembuktian untuk Semua

 (mistral.ai)
1 poin oleh GN⁺ 4 jam lalu | 1 komentar | Bagikan ke WhatsApp
  • Di tengah tren penggunaan verifikasi formal yang makin mendekati pekerjaan pengembangan nyata, Mistral AI merilis Leanstral 1.5, model Apache-2.0 untuk Lean 4
  • Model ini hanya mengaktifkan 6B dari total 119B parameter, dan melalui pembelajaran menengah, fine-tuning terawasi, serta reinforcement learning CISPO untuk mempelajari penulisan bukti sekaligus pekerjaan pada repositori kode
  • Mencatat miniF2F 100%, PutnamBench 587/672, FATE-H 87%, dan FATE-X 34%, menunjukkan kinerja kuat pada benchmark pembuktian matematika dan evaluasi proof engineering nyata
  • Dalam verifikasi kode nyata, model ini membuktikan kompleksitas waktu O(log n) untuk pohon AVL dan menemukan 11 bug nyata di 57 repositori melalui pipeline Rust-to-Lean
  • Bobot model dan API gratis leanstral-1-5 telah dirilis, sehingga dapat langsung diterapkan untuk proof engineering praktis seperti pembuktian teorema, debugging bukti, dan kontribusi repositori

Rilis Leanstral 1.5 dan karakteristik model

  • Leanstral 1.5 adalah model yang dibuat untuk melakukan proof engineering di Lean 4
  • Lisensinya Apache-2.0, dengan skala model total 119B parameter dan 6B parameter aktif
  • Dengan meningkatkan kinerja verifikasi formal, model ini dapat digunakan tidak hanya untuk benchmark matematika, tetapi juga untuk verifikasi properti kode nyata
  • Model ini menuntaskan miniF2F, menyelesaikan 587 dari 672 soal PutnamBench, serta mencapai FATE-H 87% dan FATE-X 34%

Pelatihan 3 tahap yang mempelajari umpan balik bukti

  • Pelatihan terdiri dari 3 tahap: pembelajaran menengah, fine-tuning terawasi, dan reinforcement learning berbasis CISPO
  • Dua lingkungan digunakan dalam reinforcement learning
    • Lingkungan multi-turn: model menerima proposisi teorema, lalu membuktikan atau membantahnya, dan berulang kali memperbaiki bukti berdasarkan umpan balik compiler Lean
    • Jika bukti berhasil dikompilasi, proses dianggap sukses; jika tidak, loop berlanjut hingga soal terpecahkan atau anggaran habis
    • Lingkungan agen kode: model mengedit file layaknya developer di filesystem mentah, menjalankan perintah bash, dan memeriksa informasi target, error, serta tipe secara real-time melalui Lean language server
  • Lingkungan agen kode menangani tugas panjang seperti menyelesaikan bukti parsial dalam repositori, menulis lemma pembantu, dan terus bekerja bahkan setelah beberapa kali kompresi konteks
  • Kebenaran akhir diverifikasi di fork SafeVerify milik Mistral berdasarkan daftar teorema target

Benchmark matematika dan proof engineering

  • Evaluasi menggunakan miniF2F, PutnamBench, FATE-H/FATE-X, dan FLTEval
    • miniF2F adalah benchmark matematika formal yang mencakup soal dari tingkat dasar hingga tingkat IMO
    • PutnamBench terdiri dari 672 soal dari Putnam Mathematical Competition
    • FATE-H dan FATE-X masing-masing adalah benchmark aljabar abstrak tingkat pascasarjana dan doktoral
    • FLTEval mengevaluasi tingkat kesulitan proof engineering berdasarkan pull request nyata dari repositori Fermat’s Last Theorem
  • Pada miniF2F, model ini mencapai 100% di set validasi maupun set pengujian
  • Pada PutnamBench dan FATE-H/X, model ini dibandingkan dengan Goedel-Architect, Seed-Prover 1.5 high, dan AxProverBase tanpa panduan bukti bahasa alami
  • Kinerja FATE-H/X: {b:87,34}
  • FATE-H mencapai 87% dan FATE-X mencapai 34%, mencetak kinerja terbaik baru
  • Pada PutnamBench, model ini menyelesaikan 7 soal lebih banyak daripada Seed-Prover 1.5 high, dengan biaya sekitar 4 dolar per soal
    • Konfigurasi high Seed-Prover memakai anggaran 10 H20-days per soal dan biayanya diperkirakan lebih dari 300 dolar
    • Beberapa prover dengan peringkat lebih tinggi menerima panduan bukti bahasa alami, atau beroperasi dalam kondisi berbeda seperti Aleph Prover yang memerlukan biaya 54–68 dolar per soal

Skalabilitas pada anggaran penalaran panjang dan FLTEval

  • Di PutnamBench, kinerja Pass@8 Leanstral 1.5 naik secara mulus dan monoton seiring peningkatan anggaran token
  • Dalam eksperimen yang menaikkan anggaran token per upaya dari 25k hingga 4M, jumlah soal yang terselesaikan meningkat sebagai berikut
    • 50k token: 44 soal
    • 200k token: 244 soal
    • 1M token: 493 soal
    • 4M token: 587 soal
  • Perilaku yang terus melakukan penalaran, pengeditan file, dan perbaikan selama jutaan token tanpa berhenti pada bukti panjang berujung pada peningkatan kinerja
  • FLTEval juga dirilis sepenuhnya sebagai open source
  • Di FLTEval, Leanstral 1.5 meningkatkan pass@1 dari 21,9 menjadi 28,9, dan pass@8 dari 31,9 menjadi 43,2
  • pass@8 sebesar 43,2 melampaui 39,6 milik Opus 4.6, dengan biaya sekitar seper-tujuhnya
  • Model ini juga menunjukkan kinerja lebih unggul daripada model open source yang 3–10 kali lebih besar

Contoh verifikasi kode nyata

  • Pembuktian kompleksitas waktu pohon AVL

    • Pohon AVL adalah pohon pencarian biner self-balancing yang mempertahankan tinggi O(log n) melalui rebalancing saat penyisipan dan penghapusan
    • Leanstral 1.5 memverifikasi bahwa penyisipan dan penghapusan pada implementasi nyata memiliki kompleksitas O(log n)
    • Tugas ini membutuhkan induksi struktural yang mencerminkan struktur rekursif pohon, pemrosesan pelacakan waktu berbasis monad, dan analisis kasus menyeluruh atas jalur rebalancing
    • Pembuktian berjalan melalui lebih dari 2,7 juta token dan 22 kali kompresi konteks
    • Leanstral secara sistematis menguraikan tiap lapisan monad TimeM untuk menampilkan komputasi yang bercampur dengan alur kontrol
    • Untuk penyisipan, model ini menetapkan batas 48 langkah per satuan tinggi dan batas yang mendekati suku konstan, lalu menghubungkan tinggi dan ukuran pohon dalam relasi logaritmik

  • Menemukan bug dalam kode Rust

    • Eksperimen deteksi bug terdiri dari pipeline tempat Aeneas mengubah kode Rust menjadi Lean, lalu Leanstral menyimpulkan maksud pengguna dari kode dan menghasilkan properti konsistensi
    • Leanstral mencoba membuktikan setiap properti 4 kali; jika semuanya gagal, model ini mencoba membuktikan negasinya 4 kali lagi
    • Dari 57 repositori, 47 properti yang dilanggar ditandai, dan 11 di antaranya menunjuk ke bug nyata
    • Dari bug nyata tersebut, 5 bug sebelumnya belum pernah dilaporkan di GitHub
    • Salah satu kasus ditemukan pada fungsi zigzag decoding sign di library datrs/varinteger
    • Saat input berupa Std.U64.MAX, ekspresi (value + 1) mengalami overflow
    • Dalam mode debug, terjadi crash, sedangkan dalam mode release terjadi korupsi data secara diam-diam
    • Edge case ini adalah kasus yang mudah terlewat oleh pengujian dan fuzzing umum

Distribusi dan cara penggunaan

  • Bobot model dirilis di Hugging Face
  • Endpoint API gratis tersedia di kartu model dengan nama leanstral-1-5
  • Mistral Vibe direkomendasikan sebagai lingkungan penggunaan
  • Prosedur awalnya adalah menyiapkan Mistral Vibe, menginstal Leanstral 1.5, menjalankan agen, secara opsional menginstal Lean LSP MCP, lalu memulai pekerjaan pembuktian
  • Lean LSP MCP disarankan untuk diinstal dengan menambahkannya ke ~/.vibe/config.toml
  • Jika belum ada server MCP yang sudah ada, Anda mungkin perlu menghapus mcp_servers = []
  • Leanstral dapat digunakan untuk menyelesaikan teorema, debugging bukti, dan pekerjaan kontribusi repositori

Bacaan terkait

1 komentar

 
GN⁺ 4 jam lalu
Pendapat Hacker News

  • Kritik bahwa Mistral sulit bersaing dengan model besar memang valid, tetapi menurut saya pada kenyataannya mereka berfokus pada menyediakan fitur tertentu dengan kualitas tinggi pada model kecil
    Saya memakai Mistral untuk tugas seperti OCR atau analisis berkas, dan jika menaruh 100 dolar di akun, layanan itu bisa berjalan setahun tanpa perlu khawatir soal volume permintaan
    Biayanya sangat kecil, jadi meskipun tidak bisa bersaing dengan Opus 4.8, nilainya tetap cukup besar

    • Saya penasaran seberapa kompetitif sebenarnya untuk OCR
      Kualitas lumayan dengan harga murah terasa lebih seperti pasar niche dibanding membayar 10 kali lipat untuk kualitas terbaik demi mengurangi kesalahan nantinya
    • Orang-orang bodoh Eropa itu ternyata mengoptimalkan untuk membuat produk yang bagus, bukan untuk memaksimalkan uang /s
    • Saya tidak yakin “memproses dokumen setahun dengan biaya di bawah 100 dolar per tahun” sehebat kedengarannya. Setidaknya dari sudut pandang daya saing Eropa, itu berarti Mistral menetapkan batas atas pendapatan terlalu rendah
      OCR sudah hampir menjadi komoditas, dan juga disediakan secara bawaan oleh model open source atau tempat seperti AWS
      Selain itu, dengan label harga 100 dolar per tahun, sulit membangun loyalitas, dan karena tidak ada biaya perpindahan, pelanggan bisa langsung pergi jika muncul harga yang lebih rendah
      Jika alat murah yang mudah ditiru tidak memiliki customer lock-in, itu lebih dekat ke fitur daripada bisnis
      Dari sisi pembeli memang bagus, tetapi jika ingin perusahaan Eropa dalam jangka panjang bersaing dengan pesaing global lewat kapabilitas produk, ini terlihat seperti strategi yang buruk

  • Pekerjaannya sendiri bagus, tetapi contoh penemuan bug terasa aneh
    Disebutkan bahwa pada fungsi sign untuk decoding zigzag, input Std.U64.MAX membuat (value + 1) overflow, sehingga crash di mode debug dan terjadi korupsi senyap di mode rilis, tetapi saya tidak yakin ini bisa disebut kondisi batas yang “biasanya terlewat” oleh pengujian
    Kalau pengujiannya buruk mungkin terlewat, tetapi orang yang teliti atau sistem coding berbasis machine learning cukup baik dalam berpikir “saya harus menguji nilai ekstrem”. Apalagi jika kodenya mem-parsing input pengguna
    Saya penasaran apakah mereka juga menemukan bug yang lebih menarik, tetapi memakai contoh ini karena sulit dijelaskan dengan cepat

    • Terutama bagian “fuzzing pun melewatkannya” terasa aneh. Fuzzing yang pernah saya lihat umumnya memang sengaja mengeksplorasi nilai batas
      Untuk library encoding seperti ini, fuzzing adalah ekspektasi dasar dari kode yang layak, dan saya rasa hampir pasti akan tertangkap dalam hitungan detik
      Nyatanya, ketika saya membuat pengujian round-trip yang sangat sederhana dengan proptest, dalam kurang dari satu detik muncul puluhan kegagalan dan hasil berikut:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • Sulit mengatakan ini “biasanya terlewat”, tetapi karena memang benar-benar ada, ini adalah bug yang kadang-kadang terlewat
      Keuntungan memakai Lean terlihat pada berkurangnya kebutuhan untuk secara cerdas memilih contoh apa yang harus diuji
    • Ini hanyalah quality assurance dasar. Jika pengujian melewatkan hal seperti ini, berarti kegunaannya jauh lebih terbatas daripada yang biasanya kita harapkan
      Saya jadi penasaran dengan latar belakang para penulisnya
    • Ini cuma promosi sampah
      Semua sistem property-based testing yang ditemukan sekitar tahun 1980 mengeksplorasi nilai batas
      Pengujian nyata bisa saja sulit karena semantik C dan C++, atau ketiadaannya. Sebab compiler boleh mengatakan “tes lulus” untuk semua input yang mengarah ke undefined behavior

  • Di tengah tulisan ada beberapa perbandingan dengan LLM kelas frontier, tetapi semuanya model dari setengah tahun lalu
    Jadi cukup lucu karena kesannya seperti “model baru kami lebih baik daripada model-model Tiongkok tiga generasi lalu”

    • Ini adalah model 6 miliar parameter, jadi kelasnya benar-benar berbeda. Justru “small language model kelas frontier” lebih sesuai untuk diharapkan
    • Setuju, tetapi hanya fakta bahwa ini open weight dan relatif kecil saja sudah layak jadi headline. Model ini berjalan cukup baik

  • Library itu adalah https://github.com/datrs/varinteger
    Masalah yang sama sudah muncul di repositori ini seminggu sebelum paper-nya dipublikasikan, jadi kemungkinan memang benar: https://github.com/datrs/varinteger/issues/8
    Saya tidak tahu apakah orang ini karyawan Leanstral, atau Leanstral hanya mengambil isu ini begitu saja
    Library ini kecil, pengujiannya sangat buruk secara mengejutkan, dan hampir tidak disentuh selama 8 tahun: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    Unduhannya sekitar 1.000 per hari, jadi tampaknya rendah: https://crates.io/crates/varinteger
    Karena itu, sulit menyebutnya keberhasilan besar yang layak dijadikan satu-satunya contoh. Deteksi otomatis memang berguna, tetapi saya tidak yakin ini pencapaian yang menonjol di subbidang ini
    Saya belum pernah memakai LLM untuk penulisan proof, tetapi karena data latihnya cenderung kurang, tidak mengejutkan jika hasilnya lebih kasar daripada model coding umum
    Sebagai catatan, https://crates.io/crates/varinteger mencantumkan https://github.com/mafintosh/varinteger-rs, tetapi alamat itu dialihkan ke https://github.com/datrs/varinteger, jadi meski tampak berbeda, kelihatannya ini library yang sama

    • Masalah dengan proof adalah terkadang sulit menyampaikan nilainya
      Intinya bukan menemukan bug, melainkan membuktikan bahwa jenis bug tertentu tidak ada di bawah asumsi tertentu
      Namun cerita ini sulit dijual, jadi marketing sering bergeser ke arah “kami menemukan bug ini”

  • Apakah ini bisa berguna bahkan bagi orang yang sama sekali tidak mengenal Lean? Saya ingin memverifikasi perangkat lunak yang sedang dikerjakan, tetapi tidak punya pengalaman verifikasi formal
    Saya penasaran apakah dengan spesifikasi, kode, dan waktu belajar yang terbatas saja bisa mendapatkan hasil yang layak pakai

    • Bagian yang ingin dibuktikan memang harus dipahami, tetapi tidak perlu memahami seluruh proses pembuktiannya
      Rasanya lebih mirip membaca tipe Haskell daripada matematika, hanya saja kosakatanya banyak dipinjam dari matematika
    • Jika membaca bagian “Bug Discovery: Finding Hidden Flaws” dalam tulisannya, tampaknya mereka memulai hanya dengan kode Rust lalu menggunakan model untuk menemukan masalah di Rust open source
      Mungkin kita juga bisa dibantu lewat percakapan untuk menulis kode Lean guna memverifikasi aplikasi, tetapi saya tidak yakin
    • Setidaknya kita harus memahami teorema apa yang ingin dibuktikan tentang kode, dan bagaimana mengekspresikannya di Lean
      Kalau tidak, kita tidak bisa memverifikasi output-nya
      Secara mekanis, mungkin saja ada suatu proposisi yang terbukti benar menurut pemeriksaan, tetapi jika tidak tahu apa arti proposisi itu dan apakah ia mencakup hal yang sebenarnya ingin diverifikasi, itu tidak ada artinya
    • Dari keadaan sama sekali tidak mengenal Lean4, dalam sekitar 6 bulan saya sampai pada titik memakai Lean4 untuk sebagian besar coding, dan proses ini sangat dipercepat berkat bantuan AI
      Mengejutkan betapa konsisten dan lancarnya model-model ini dalam Lean4. Bukan hanya model kelas terdepan, model lokal kecil pun begitu, dan rasanya LLM memang memahami Lean4 dengan baik
      Masih ada jalan panjang sebelum bisa disebut ahli Lean4, tetapi sekarang saya tidak lagi benar-benar memerlukan bantuan untuk membuat program yang berguna
      Bahkan dengan pengetahuan yang hampir nol, kemampuan untuk memercayai bagian-bagian yang belum sepenuhnya dipahami sangat meningkatkan kecepatan belajar. Mendapatkan program yang bisa diandalkan meski dengan pengetahuan yang belum sempurna itu praktis dan juga memotivasi
      Rasanya batasannya tidak ditentukan oleh seluruh langkah pembuktian perantara, melainkan oleh bagian bahasa yang menjelaskan aksioma dan permukaan proposisi kita sendiri. Seiring waktu, untuk melakukan lebih banyak hal kita harus memahami lebih banyak, tetapi dalam arti tertentu kita bisa bekerja dengan aman pada level N+1
      Terlepas dari perannya sebagai theorem prover, Lean4 juga merupakan bahasa pemrograman yang menyenangkan, dan kecepatannya luar biasa
      Saya menggunakannya dengan io_uring, dan dalam banyak kasus jauh lebih cepat daripada C++/libuv atau Rust/Tokio
      Kadang jika terlihat ekor besar pada metrik seperti latensi p99.99, perlu tuning seperti mengganti angka ke fixed-width, tetapi C++ dan Rust pun tetap perlu tuning

  • Menarik bahwa Lean 4 didorong untuk verifikasi formal
    Saya kira ranah ini lebih milik Isabelle/HOL dan TLA+
    Setidaknya saya akan berharap ada model yang dilatih untuk memakai ketiganya. Isabelle/Isar juga tampak lebih baik untuk derivasi maju dalam aljabar linear; ada yang bisa menjelaskan?

    • Memang benar Lean lebih sedikit diadopsi untuk verifikasi perangkat lunak dibanding Isabelle atau Rocq, yaitu Coq lama
      Di bidang ini, bahkan Agda cenderung lebih banyak dipakai
      Namun Lean saat ini mendapatkan momentum yang cukup besar sebagai alternatif, terutama karena kemampuannya sebagai bahasa pemrograman fungsional serbaguna
      Secara pribadi, saya menganggap pendekatan berbasis logika Hoare atau logika pemisahan lebih praktis karena lebih mudah menyelaraskan kebutuhan dan spesifikasi. Saya menyukai Dafny dan F*

  • Lucu juga melihat para developer menyelipkan penyebutan Le Chaton Fat dalam pengumuman Twitter
    Terlepas dari apakah mereka benar-benar terlibat dalam Le Chaton Fat atau tidak, rasanya model “general-purpose besar” yang benar-benar baru akan segera hadir
    Karena mereka menyebutnya langsung bahkan setelah kehebohan media, saya jadi menantikannya. Semoga namanya lebih kreatif daripada “Large 4”

  • Leanstral 1.5 bisa dicoba di OpenATP terbaru
    OpenATP adalah paket Python open source sekaligus CLI untuk automated theorem prover bergaya agen, dengan dukungan bawaan untuk dijalankan secara lokal di Docker atau secara remote di sandbox Modal
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com