Leanstral: agen open-source untuk rekayasa kode dan pembuktian formal yang andal

• Agen kode open-source pertama yang dirancang untuk Lean 4, dengan tujuan mengotomatiskan pembuktian formal (formal proof) untuk mengurangi beban verifikasi manusia
• Bobot model dirilis di bawah lisensi Apache 2.0, dan dapat langsung digunakan melalui lingkungan Mistral Vibe serta endpoint API gratis
• Menggunakan arsitektur sparse dengan 6B parameter aktif untuk mencapai efisiensi dan penghematan biaya, serta mendukung integrasi MCP seperti lean-lsp-mcp
• Pada benchmark FLTEval, mencatat skor lebih tinggi daripada model open-source besar seperti Qwen3.5, GLM5, dan Kimi-K2.5, serta menunjukkan performa serupa dengan biaya lebih dari 15 kali lebih murah dibanding Claude Sonnet
• Menawarkan pendekatan baru yang menggabungkan otomatisasi pembuktian formal dan peningkatan keandalan kode, dengan potensi penggunaan baik untuk matematika riset maupun pengembangan perangkat lunak mission-critical

---

Ikhtisar Leanstral

• Leanstral adalah agen kode open-source pertama untuk Lean 4, yang bekerja di lingkungan proof assistant untuk pembuktian formal
  • Lean 4 dapat merepresentasikan objek matematis yang kompleks (misalnya ruang perfectoid) dan spesifikasi perangkat lunak
  • Berbeda dari sistem pembuktian sebelumnya yang berfokus pada wrapper model umum atau masalah tunggal, Leanstral dilatih agar bekerja efisien pada formal repositories yang realistis
• Mengadopsi arsitektur sparse dengan 6B parameter aktif, menggabungkan parallel inference dengan kemampuan verifikasi Lean
• Mendukung integrasi MCP, sehingga kompatibel dengan protokol yang sering digunakan seperti lean-lsp-mcp

Rilis dan aksesibilitas

• Bobot model dirilis di bawah lisensi Apache 2.0 dan disediakan dalam mode agen di Mistral Vibe
• Dapat diakses siapa saja melalui endpoint API gratis (labs-leanstral-2603), dan umpan balik pengguna akan dikumpulkan untuk meningkatkan model berikutnya
• Laporan teknis dan alat evaluasi FLTEval juga dirilis bersama, untuk mengukur performa rekayasa pembuktian di dunia nyata melampaui evaluasi yang berfokus pada matematika

Evaluasi performa (Evaluation)

• Dievaluasi berdasarkan kemampuan menyelesaikan semua pembuktian formal dan definisi konsep matematika baru pada unit Pull Request dari proyek FLT
• Objek pembanding: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral vs. model open-source

• Leanstral-120B-A6B mencatat 26.3 poin (pass@2), lebih tinggi daripada GLM5 (16.6 poin) dan Kimi-K2.5 (20.1 poin)
• Sementara Qwen3.5 memperoleh 25.4 poin pada 4 kali eksekusi (pass@4), Leanstral meraih skor lebih tinggi dengan setengah jumlah eksekusi
• Dapat diskalakan secara linear hingga 29.3 poin (pass@4) pada tingkat biaya yang sama

Leanstral vs. lini produk Claude

• Menunjukkan keunggulan 2.6 poin dibanding Sonnet (26.3 vs 23.7), dengan biaya eksekusi $36 vs $549, lebih dari 15 kali lebih murah
• Mencatat 31.9 poin pada pass@16, 8 poin lebih tinggi daripada Sonnet
• Claude Opus 4.6 dengan performa tertinggi mencatat 39.6 poin, tetapi biayanya $1,650, yaitu 92 kali lebih tinggi dibanding Leanstral
• Semua benchmark dijalankan di lingkungan Mistral Vibe tanpa modifikasi

Model	Biaya($)	Skor
Haiku	184	23.0
Sonnet	549	23.7
Opus	1,650	39.6
Leanstral	18	21.9
Leanstral pass@2	36	26.3
Leanstral pass@4	72	29.3
Leanstral pass@8	145	31.0
Leanstral pass@16	290	31.9

Studi kasus (Case Studies)

Menangani perubahan versi Lean

• Memasukkan pertanyaan StackExchange tentang error terkait alias tipe yang muncul di Lean 4.29.0-rc6
• Leanstral mereproduksi lingkungan masalah dan mendiagnosis secara akurat persoalan definitional equality
• Menyarankan penggunaan abbrev alih-alih def, sehingga tactic rw kembali berfungsi dengan normal
• Menjelaskan dengan jelas kepada pengguna penyebab masalah dan alasan solusinya

Penalaran dan transformasi program

• Mengonversi definisi program dari Rocq ke Lean, termasuk implementasi notasi kustom
• Sebagai contoh, membuktikan bahwa perintah plus2 menjalankan operasi menambahkan 2 ke variabel X
• Menyelesaikan dan membuktikan theorem di Lean hanya berdasarkan spesifikasi Rocq yang diberikan

Cara penggunaan

• Integrasi Mistral Vibe: dapat langsung digunakan dengan perintah /leanstall
• Labs API: dapat diakses secara gratis atau berbiaya rendah
• Unduh model: dapat dijalankan langsung di bawah lisensi Apache 2.0

Makna penting

• Leanstral adalah upaya open-source pertama yang menggabungkan pembuatan kode dan otomatisasi pembuktian formal
• Menunjukkan potensi pemanfaatan di matematika riset, pengembangan perangkat lunak yang dapat diverifikasi, dan perancangan sistem berkeandalan tinggi
• Dinilai sebagai infrastruktur verifikasi kode baru yang sekaligus menghadirkan efisiensi biaya dan keterbukaan

[GN⁺]

Komentar Hacker News

• Menarik melihat orang mulai menyadari pola bahwa kini agen bisa diberi spesifikasi perilaku yang diinginkan, lalu menulis kode sesuai spesifikasi tersebut
  Baik memakai TDD, alat verifikasi, atau pendekatan lain, seiring waktu rangkaian verifikasi seperti ini akan menumpuk menjadi repositori dokumentasi yang bisa dieksekusi, yang menunjukkan “bagaimana seharusnya sistem bekerja”
  Pendekatan ini jauh lebih kuat daripada spesifikasi Markdown biasa, karena yang ditangkap dalam kode bukan sekadar niat, melainkan perilaku detail
  Semakin kompleks perangkat lunak, semakin terbatas pendekatan tradisi lisan ala “tanya saja ke Jim”

  • Rasanya bedanya tidak terlalu besar. Kode pada akhirnya hanyalah ekspresi lain dari informasi yang juga bisa ditulis di file .md
    Ketelitian dan konteks bisa hilang ketika resolusi berubah
    Saya setuju dengan TDD atau pengembangan yang berpusat pada verifikasi, tetapi menuliskannya dalam bentuk kode bukanlah tujuan akhirnya
    Sudah ada jutaan baris pengujian, jadi yang realistis adalah mengembangkannya berdasarkan itu
  • Saya rasa baru setelah AI hadir, realitas yang diimpikan TDD akhirnya menjadi mungkin
  • Pendekatan ini menarik, tetapi tulisan blognya membingungkan
    Saya penasaran Lean sebenarnya membantu di bagian mana.
    Misalnya, apakah state machine dibuktikan di Lean lalu dipindahkan ke Dart?
    Saya tidak terlalu paham Lean, jadi sulit menilai apakah ini pendekatan yang realistis

• Seperti juga disebut dalam podcast terbaru Jack Clark (co-founder Anthropic) dan Ezra Klein, ada banyak pembahasan bahwa alignment model itu relatif dan keberagaman itu penting
  Ada pendapat bahwa model Mistral tertinggal dibanding model frontier lain, tetapi bereksperimen dengan beragam teknik alignment dan perusahaan tetap penting bagi ekosistem

  • Pada akhirnya saya rasa waktu yang akan menyelesaikannya

• Contoh keberhasilan nyatanya mengingatkan saya pada Red Green TDD dari Simon Willison
  Proses Leanstral membuat kode pengujian untuk mereproduksi lingkungan kegagalan dan menemukan masalah definitional equality sangat mengesankan

  • Jika agen menulis pengujiannya sendiri, saya jadi penasaran apakah jaminan ketepatan akan lebih tinggi dibanding saat kode dan tes ditulis terpisah
  • Menurut saya TDD pada akhirnya mirip dengan prompt engineering. Intinya adalah memberi tujuan yang jelas kepada agen

• Model ini memang dilatih untuk tugas tertentu, tetapi performanya masih di bawah Opus
  Opus memang 6 kali lebih mahal, tetapi tampaknya sepadan

  • Idenya bagus, tetapi pada akhirnya kualitas lebih utama daripada kepercayaan
    Saya paham startup Eropa dengan modal lebih kecil membidik ceruk seperti ini, tetapi sepertinya sulit berujung pada pendapatan besar
  • Keandalan benchmark memang samar, tetapi kalau melihat hasil pass@2 atau pass@3, kesannya bisa berubah
    Akan lebih menarik jika dibandingkan dengan model seperti Codex
  • Model ini open source, jadi bisa dijalankan secara lokal. Bukankah itu poin yang cukup penting?

• Saya suka konsep “kode yang dapat dipercaya”
  Tapi patokan perbandingannya membingungkan. Mereka menekankan bahwa ini lebih murah daripada Haiku, padahal Haiku sendiri lemah untuk tugas ini dan Leanstral lebih lemah lagi
  Jika tujuannya akurasi, saya tidak paham kenapa “murah tapi kurang bagus” dianggap penting
  Meski begitu, Opus juga tidak sempurna, jadi kalau skalanya diperbesar mungkin hasilnya bisa lebih baik

  • Dari grafik terlihat performa meningkat ketika jumlah pass ditambah
    Pada 2 kali percobaan, hasilnya lebih baik daripada Haiku dan Sonnet, dan pada 16 kali percobaan hasilnya mendekati Opus sambil tetap lebih efisien secara biaya
  • Sebenarnya sederhana — cukup minta di prompt “hanya keluaran yang dapat dipercaya”

• Dari sudut pandang orang yang tidak mengenal Lean, saya penasaran apakah ini punya nilai langsung
  Apakah ini akan otomatis menambahkan pembuktian ke kode dalam bahasa seperti Go, atau cukup sekadar mendukung keragaman model terbuka?

  • Kemungkinan besar agen akan membuat spesifikasi Lean4, lalu perangkat lunak dievaluasi berdasarkan spesifikasi itu
    Tetapi pada akhirnya spesifikasi Lean4 itu sendiri menjadi artefak perangkat lunak
    Kalau begitu, kita kembali ke masalah memverifikasi apakah spesifikasi tersebut benar — pada akhirnya tinjauan manusia tetap diperlukan

• Saya sudah memperkirakan arus seperti ini sejak beberapa minggu lalu, dan senang ternyata benar
  Di era LLM, tampaknya yang akan lebih penting daripada keterbacaan kode bagi manusia adalah kemampuan dibuktikan dan efisiensi token
  Dengan menggabungkan Lean dan Rust, mungkin kita bisa menuju dunia di mana “hanya kode yang sudah dibuktikan yang bisa dikompilasi”
  Diskusi terkait saya rangkum di komentar sebelumnya

  • Namun, sistem pembuktian apa pun tidak benar-benar menjamin “pembuktian yang benar”
    Sistem itu hanya menjamin bahwa pembuktian tersebut valid secara logis
    Memahami sepenuhnya apa yang dibuktikan oleh suatu pembuktian sama sulitnya dengan memahami program itu sendiri, tetapi ada manfaat berupa pendalaman cara berpikir dalam prosesnya

• Menyenangkan melihat “open source” tidak cuma jadi slogan, tetapi benar-benar dirilis sebagai bobot berlisensi Apache-2.0

  • Namun menurut standar komunitas, jika modelnya tidak bisa direproduksi, itu hanya open weights, bukan “open source”

• Menurut berita resmi Mistral
  Claude Opus mencatat skor 39.6 dengan biaya 1.650 dolar,
  Leanstral pass@8 mencatat 31.0 dengan biaya 145 dolar, dan pass@16 mencatat 31.9 dengan biaya 290 dolar,
  sehingga efisiensi performa terhadap biaya terbilang cukup tinggi