OpenBMB merilis open source pipeline MathForm untuk formalisasi matematika otomatis secara utuh: bobot model 8B, dataset Lean 4 terverifikasi sekitar 367 ribu contoh, kode evaluasi, dan skrip Pass@k, semuanya dirilis bersamaan. Model ini ada di Hugging Face dengan lisensi Apache 2.0, dibangun di atas basis Qwen3-8B dengan presisi bobot BF16. Proyek ini dikerjakan oleh tim OpenBMB yang didukung bersama oleh Laboratorium NLP Universitas Tsinghua dan ModelBest (面壁智能), dengan makalah terkait diajukan ke arXiv pertengahan bulan ini, ditulis oleh 10 penulis.
Formalisasi otomatis adalah menerjemahkan pernyataan matematika berbahasa alami ke bahasa formal yang bisa diverifikasi mesin seperti Lean 4. Kesulitannya bukan pada terjemahan harfiah. Hierarki tipe dan sistem definisi di Mathlib sangat besar — istilah seperti 'fungsi kontinu' atau 'grup hingga' dalam suatu pernyataan harus dipetakan secara tepat ke definisi yang sesuai di pustaka tersebut, sekaligus memastikan pernyataan hasil formalisasi tetap bermakna sama dengan pernyataan aslinya. Salah satu saja meleset, compiler tetap bisa saja meloloskannya.
Bagaimana data ini dibuat
Pipeline MathForm terdiri dari empat tahap. Perencana (planner) lebih dulu mencari konsep matematika dalam pernyataan tersebut di Mathlib, dengan alat pencarian LeanExplore mengembalikan 22 hasil teratas setiap kali; model kemudian menghasilkan pernyataan Lean 4 berdasarkan konteks hasil pencarian itu. Kandidat kemudian melewati pemeriksaan format dan uji kompilasi secara berurutan, lalu dinilai konsistensi semantiknya oleh model besar sebagai juri; jalur yang lolos direkonstruksi mundur menjadi jejak pelatihan yang bersih.
Satu angka dalam makalah ini menunjukkan pentingnya iterasi: ronde-ronde berikutnya menyumbang tambahan 31,0% dari seluruh sampel yang dipertahankan. Artinya, jika hanya dilakukan satu kali generasi lalu yang gagal langsung dibuang, hampir sepertiga data yang bisa dipakai akan hilang sia-sia.
Tahap pencarian (retrieval) adalah bagian paling hemat biaya dari desain ini. Meminta model mengingat sendiri nama dan signature persis dari sebuah definisi di Mathlib pada dasarnya sama saja dengan mengujinya menghafal pustaka yang terus diperbarui. Dengan menyerahkan pustaka itu ke alat pencarian dan membiarkan model hanya menyusun hasilnya, jumlah parameter yang dibutuhkan pun turun secara alami. Ini juga menjelaskan mengapa model 8B bisa menyaingi model 32B: keduanya sebenarnya tidak sedang mengerjakan tugas yang sama.
Dataset yang dihasilkan diberi nama FormalVerse, berisi sekitar 367 ribu sampel terverifikasi, bersumber dari DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath, OpenR1-Math, ditambah materi dari buku teks klasik. Dataset ini sudah mendapat 358 like di Hugging Face.
Rapor hasil dan dua cara membacanya
Jalur pelatihannya adalah fine-tuning terawasi diikuti reinforcement learning. Evaluasi mencakup enam benchmark: FormalMATH-Lite dan DeepSeek-ProverBench menggunakan matematika kompetisi, CombiBench menguji matematika kombinatorik, sedangkan seri FATE dibagi menjadi tingkat M, H, dan X berdasarkan tingkat kesulitan aljabar.
MathForm-8B mencatat rata-rata Pass@8 pemeriksaan sintaks sebesar 88,06%, dan rata-rata pemeriksaan konsistensi 72,37%; tingkat kelulusan konsistensi pada tiga level FATE berturut-turut adalah 97,33%, 63,00%, dan 37,00%. Kelompok pembanding meliputi Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B, serta versi 7B/8B dan 32B dari StepFun-Formalizer, Goedel-Formalizer-V2, dan ReForm. Model 8B ini melampaui beberapa model formalisasi khusus 32B pada sejumlah test set.
Selisih antara dua metrik ini lebih informatif daripada skor absolutnya. Pemeriksaan sintaks hanya menanyakan apakah kodenya berhasil dikompilasi; pemeriksaan konsistensi menanyakan apakah pernyataan hasil formalisasi benar-benar bermakna sama dengan soal aslinya. Selisih 88% berbanding 72%, belasan poin persentase di tengahnya itulah bottleneck sesungguhnya dari pipeline ini saat ini. Sesuatu yang berhasil dikompilasi belum tentu teorema yang ingin dibuktikan.
Ambang batasnya turun hingga level satu workstation
Situs ini beberapa hari lalu menulis tentang peringatan Terence Tao: bukti yang dihasilkan AI bisa menumpuk sampai tak ada yang sempat membacanya semua. Formalisasi justru menjadi separuh jawaban lain dari persoalan itu — selama sebuah bukti bisa lolos compiler Lean, bisa tidaknya dipahami manusia bukan lagi syarat untuk menerimanya. Syaratnya adalah pernyataan itu sendiri harus diterjemahkan dengan benar, dan angka 37% di FATE-X menunjukkan masih ada jarak cukup jauh untuk sampai ke titik itu.
Hitungan kasarnya, model 8B yang dimuat dengan BF16 membutuhkan sekitar 16GB VRAM, sementara model 32B pada presisi yang sama butuh sekitar 64GB. Yang pertama bisa dijalankan dengan satu GPU konsumen 24GB, sedangkan yang kedua butuh multi-GPU atau kartu kelas profesional. Bagi jurusan matematika di kampus, komunitas proof assistant, dan tim kecil, ambang batas perangkat keras untuk menjalankan pipeline formalisasi turun dari level klaster ke level satu mesin saja. Dataset dan skrip evaluasi yang ikut dirilis sekaligus membuat biaya untuk mereplikasi atau mengoreksi hasilnya ikut turun.
Deretan nama di tabel perbandingan juga menunjukkan betapa ramainya bidang ini sekarang: Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm — semuanya model formalisasi khusus yang muncul dalam satu-dua tahun terakhir, dan semuanya open source. Formalisasi tidak seperti chat serba guna yang perbedaannya ditentukan oleh besarnya komputasi; yang menentukan di sini adalah kepiawaian membangun data dan loop verifikasi yang berjalan baik, sehingga skala parameter justru jadi variabel yang relatif kurang penting. Kecepatan dari demo di makalah sampai bisa dirilis sebagai open source ini lebih cepat dari perkiraan kebanyakan orang.
Sumber: repositori dan model card OpenBMB, CocoLoop, praprint arXiv 2608.14221, halaman dataset Hugging Face; angka skala parameter, lisensi, jumlah sampel FormalVerse, dan metodologi Pass@8 per benchmark telah diverifikasi silang.