Leanstral 1.5

 (docs.mistral.ai)
1 poin oleh GN⁺ 3 jam lalu | 1 komentar | Bagikan ke WhatsApp
  • Leanstral 1.5 adalah model yang diperbarui dan disesuaikan untuk rekayasa pembuktian formal Lean 4, ditujukan untuk pembuktian teorema otomatis dan formalisasi otomatis
  • Skala model terdiri dari total 119B parameter dan 6.5B parameter aktif, dengan asumsi pemrosesan konteks pembuktian dan dokumen yang panjang
  • Pengidentifikasi yang disediakan adalah labs-leanstral-1-5, dan di dokumentasi ditampilkan sebagai model Labs v1.5
  • Panjang konteks adalah 256k, dan item harga ditampilkan sebagai $0, menekankan aksesibilitas untuk eksperimen dan evaluasi
  • Dapat digunakan bersama API Chat Completions, function calling, agents, structured outputs, OCR, Document QnA, FIM, embeddings, moderations, audio, dan batch processing

Model yang disesuaikan untuk pembuktian formal Lean 4

  • Leanstral 1.5 adalah versi pembaruan dari model rekayasa pembuktian formal Lean 4
  • Target optimasi utamanya adalah pembuktian teorema otomatis dan formalisasi otomatis
  • Pengidentifikasi model disediakan sebagai labs-leanstral-1-5

Skala model dan atribut dasar

  • Konfigurasi parameter ditampilkan sebagai 119B total parameters, 6.5B active
  • Panjang konteks adalah 256k
  • Item harga ditampilkan sebagai $0
  • Kategori rilis adalah Labs v1.5

API percakapan, agen, dan output terstruktur

Pemrosesan dokumen, pelengkapan kode, dan embeddings

Keamanan, audio, dan pemrosesan batch

Bacaan terkait

1 komentar

 
GN⁺ 3 jam lalu
Komentar Hacker News

  • Karena penasaran aku daftar, isi saldo ke akun, lalu coba pakai, tapi ternyata tidak bisa. Karena dibilang ini model Labs, aku coba menyalakan Labs, dan kali ini malah muncul kesalahan yang tidak diketahui. Saat mau menghubungi dukungan pelanggan sesuai petunjuk, ternyata tidak ada dukungan pelanggan, cuma FAQ asal jadi
    FAQ-nya terlihat seperti dibuat dengan vibe coding dan pencariannya juga payah, jadi apa pun pertanyaan yang dimasukkan, jawabannya selalu sama sekali tidak relevan. Lalu aku sadar: kalau AI memang jago urusan dukungan pelanggan, kenapa perusahaan AI tidak memberikan dukungan pelanggan dengan AI mereka sendiri?

    • Sebenarnya mereka memang memakainya. Contohnya Cursor. Lihat diskusi lama “Cursor IDE support hallucinates lockout policy, causes user cancellations”[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Tidak pernah ada yang mengira AI itu bagus untuk dukungan pelanggan. AI cuma membuat dukungan pelanggan murah, dan banyak perusahaan memang sejak dulu tidak peduli pada kualitas dukungan pelanggan, jadi mereka senang karena biayanya bisa dipangkas lebih jauh
      Dari sudut pandang perusahaan yang kesal karena harus mengeluarkan uang untuk memperbaiki masalah nyata, itu justru dukungan pelanggan yang “bagus”
    • Aku tertawa sekaligus merasa miris melihat komentar ini. Rasanya sangat khas Uni Eropa. Butuh 18 bulan untuk mendapatkan satu kontrak perusahaan di EU, dan hari ini setelah kutandatangani lalu kukirim balik, yang datang malah autoresponder: “Maaf, saya sedang cuti sampai akhir Juli...”
      Selama setahun terakhir berhubungan dengan orang ini, ini sudah autoresponder cuti keempat yang kuterima
    • Aneh dan bikin frustrasi, tapi aku bisa memakai model ini gratis meskipun sama sekali tidak pernah menautkan metode pembayaran apa pun
    • Orang-orang ini tidak membalas email. qwant juga begitu
      Sampelnya memang cuma dua, tapi jadi membuatku berasumsi bahwa perusahaan Prancis tampaknya tidak terlalu suka dihubungi dalam bahasa Inggris

  • Ini sedikit topik lain, tapi cukup menyedihkan bahwa EU pada dasarnya tidak punya apa-apa di pasar LLM frontier yang sesungguhnya. Terutama kalau mengingat belakangan ini AS benar-benar membatasi akses ke model-model yang paling mutakhir
    Apakah ini murni karena kurangnya pendanaan dan infrastruktur?

    • Mistral umumnya menang di area yang memang mereka pilih untuk ditarungkan, dan saat ini itu yang dibutuhkan
      Lebih akurat membandingkan AS atau Tiongkok dengan melihat seberapa besar kontribusi ekonomi Prancis, bukan seluruh ekonomi EU, terhadap model frontier. Skalanya memang tidak cukup besar. Sebaliknya, lebih baik melihat apa yang bisa dicapai dengan skala kecil itu, dan produk niche seperti Leanstral dan Voxtral adalah hasilnya
    • Kurang lebih benar
      Prancis dan Jerman adalah ekonomi terbesar di EU; Prancis punya Mistral, dan Jerman punya lembaga yang sifatnya seperti modal ventura dengan dukungan pemerintah. Lembaga itu sangat bangga mengumumkan 125 juta euro (<150 juta dolar) untuk membantu para peneliti Eropa mencapai frontier baru pada model berdaulat[1]
      Uang itu pun tidak diberikan ke satu pemenang tunggal, melainkan dibagi ke beberapa penerima. Sebagai langkah awal ini bagus, tetapi tepatnya itu akan pantas disebut langkah awal kalau terjadi 3–4 tahun lalu. Sangat disayangkan
      [1] (bahasa Jerman) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Baik software secara umum maupun AI adalah pasar yang makin menguntungkan yang sudah besar. Perusahaan besar AS mampu menyapu bersih talenta Eropa dan perusahaan Eropa yang sedang naik daun, dan memang itulah yang mereka lakukan. Kalau tidak ingin mengakuisisi, mereka juga bisa menekan lewat harga sampai bangkrut
      Kita hidup dalam ekonomi kolonial yang menjadikan modal manusia sebagai bahan mentah, dan semuanya mengalir ke AS. Kalau ingin menghindarinya, kita harus berhenti memainkan permainan yang sekarang dan, seperti Tiongkok, membangun industri yang kompetitif lewat kebijakan industri yang sungguh-sungguh. Selama beberapa dekade terakhir tidak ada kemauan untuk itu, tetapi Trump dengan sangat jelas menunjukkan kembalinya negara, dan Eropa pun perlahan mulai mengakuinya
    • Mistral sudah menggalang lebih dari 4 miliar dolar, jadi itu memang uang yang besar, tapi tetap bukan level OpenAI/Anthropic/xAI
      Bagian yang sulit adalah membenarkan pengembangan LLM murni secara finansial. Model-modelnya sangat mirip satu sama lain. OpenAI pada awalnya membenarkannya dengan narasi “organisasi amal” untuk riset murni, Anthropic pecah dari sana dengan alasan OpenAI tidak cukup peduli pada keselamatan. Elon berkata bahwa jika dia tidak membuat Grok, AI akan pura-pura sadar dan tidak jujur, dan Google membuat Gemini karena pada dasarnya mereka adalah titik awalnya, dan riset AI memang misi inti yang diberikan Larry dan Sergey sejak pendirian perusahaan. Hanya saja sempat ditahan lama karena alasan finansial
      Motivasi model-model Tiongkok sejujurnya tidak jelas. Aku belum pernah melihat penjelasan yang meyakinkan, hanya hipotesis. Tetapi melihat bagaimana model-model itu dirilis gratis atau dengan harga yang terlalu murah, motivasinya juga tampaknya bukan finansial
      Sebaliknya, Mistral adalah perusahaan biasa. Mereka tidak punya donor kaya yang menaburkan uang karena percaya pada narasi takdir kosmis, jadi apa yang mereka lakukan harus dibenarkan lewat ROI. Kalau begitu, pelatihan LLM skala besar nyaris otomatis tersingkir
      Regulasi EU juga harus dipertimbangkan. Dulu saat aku memeriksanya, ada banyak aturan aneh yang mematikan kemungkinan industri teknologi Eropa. Di Inggris bahkan ada aturan bahwa internet hanya boleh di-crawl untuk tujuan riset
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Dan tanpa First Amendment, risiko dituntut karena apa yang diucapkan model jauh lebih besar. Lihat saja kasus Jerman yang membawa Google ke pengadilan karena konten yang dimasukkan model ke halaman hasil pencarian
      Jadi keuntungannya tidak jelas, sementara risiko hukumnya sangat besar
    • EU tidak punya pasar bersama yang benar-benar berfungsi, terutama untuk pasar modal. Populasinya lebih besar daripada AS dan total ekonominya pun lebih besar, tetapi itu tidak banyak berarti jika sumber dayanya tidak bisa dihimpun secara efisien
      Apakah di Eropa mungkin menghimpun 100 miliar dolar untuk satu lab baru? Kalau tidak, ya sudah selesai dan sebaiknya menyerah saja

  • Kebetulan. Tadi pagi saya baru saja merilis OpenATP. OpenATP adalah paket Python open-source sekaligus CLI untuk pembukti teorema otomatis bergaya agen
    Ini juga mencakup dukungan Leanstral melalui harness Vibe milik Mistral. Model Leanstral produksi sebelumnya sudah dihentikan pada 22 Mei, dan saya berencana memperbarui paket ini agar mengarah ke Leanstral 1.5 secepat mungkin
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • 404 ya?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • Saya kurang paham kebijakan bobot-nya. Situs ini membuatnya terlihat seperti bobotnya bersifat terbuka karena berlisensi Apache, tetapi saya tidak bisa menemukan tautan unduhnya
    Profil Hugging Face-nya tampaknya hanya menyediakan snapshot lama[0]. Apakah ada yang tahu apakah bobotnya bisa diunduh, dan kalau bisa, di mana mendapatkannya?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Saya juga mendapat “Page not found”. Apakah ada yang berhasil mengaksesnya? Ini tentang apa?

  • Diskusi tentang Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 dan Idris 2 diremehkan, dan karena memberikan jaminan tambahan, keduanya sangat mungkin sangat bagus untuk dipakai LLM dalam coding

  • Sekarang muncul 404

  • Saya mendaftar karena berita ini, tetapi untuk memakai “Code”, apakah harus menghubungkan GitHub? Terasa terlalu membatasi