Batas kemampuan kecerdasan buatan dengan cepat bergerak maju ke dalam domain kompleks penalaran formal yang ketat. Hari ini, tim Seed dari ByteDance telah mengungkap lompatan signifikan di bidang ini dengan merilis Seed Prover 1.5, sebuah model khusus yang dirancang untuk menghasilkan dan memverifikasi pembuktian matematika formal. Iterasi baru ini menunjukkan kemampuan luar biasa untuk menangani masalah mulai dari kompetisi tingkat SMA elit hingga matematika tingkat pascasarjana lanjutan, menandakan potensi pergeseran paradigma dalam cara mesin dapat membantu dan berpotensi mengotomatisasi penelitian matematika yang mendalam.
Tolok Ukur Baru dalam Pembuktian Teorema Otomatis
Seed Prover 1.5 milik ByteDance bukanlah chatbot serba guna; ini adalah mesin yang disetel dengan baik untuk penalaran matematika formal. Fungsi utamanya adalah mengambil pernyataan matematika dan menghasilkan bukti lengkap yang dapat diverifikasi mesin, ditulis dalam bahasa pemrograman Lean, sebuah sistem yang digunakan oleh matematikawan untuk memastikan kebenaran logis yang mutlak. Kehebatan model ini ditunjukkan pada beberapa tolok ukur publik yang paling menantang. Yang paling menonjol, ia menghasilkan bukti yang dapat diverifikasi untuk lima masalah pertama dari International Mathematical Olympiad (IMO) 2025 hanya dalam 16,5 jam. Ketika dinilai berdasarkan standar IMO historis, performa ini setara dengan skor 35 dari 42, sebuah hasil yang akan mengamankan medali emas dalam kompetisi sebelumnya. Pencapaian ini sendiri menandai momen penting bagi AI dalam matematika formal.
Tolok Ukur Kinerja Kunci untuk Seed Prover 1.5:
| Tolok Ukur | Deskripsi | Kinerja Seed Prover 1.5 | Konteks Hasil |
|---|---|---|---|
| IMO 2025 (P1-P5) | Kompetisi matematika tingkat SMA teratas. | Menghasilkan bukti yang dapat diverifikasi dalam 16,5 jam. | Skor 35/42, memenuhi standar historis Medali Emas. |
| Putnam 2025 | Kompetisi matematika sarjana utama di Amerika Utara. | Menyelesaikan 11 dari 12 soal dalam 9 jam. | Menunjukkan kemampuan kuat di tingkat elit sarjana. |
| Putnam Historical | Kumpulan lengkap soal Putnam masa lalu. | Menyelesaikan 88% soal. | Menetapkan kinerja yang kuat di berbagai gaya soal. |
| Fate-H | Mewakili tingkat kesulitan matematika setara gelar Master. | Menyelesaikan 80% soal. | State-of-the-Art (SOTA) baru untuk model penalaran formal. |
| Fate-X | Mewakili tingkat kesulitan matematika setara gelar Doktoral. | Menyelesaikan 33% soal. | SOTA baru; menunjukkan kemampuan menangani masalah tingkat penelitian. |
Skala dari Kesulitan Sarjana hingga Doktoral
Kemampuan model ini melampaui masalah Olimpiade. Dalam tes terhadap kompetisi bergengsi Putnam, ujian yang sangat sulit untuk mahasiswa sarjana di Amerika Utara, Seed Prover 1.5 menyelesaikan 11 dari 12 masalah dari kontes 2025 dalam 9 jam. Secara lebih sistematis, ia berhasil menyelesaikan 88% masalah di seluruh dataset Putnam historis. Untuk mengukur performanya pada matematika tingkat penelitian lanjutan, tim mengevaluasinya pada tolok ukur Fate-H dan Fate-X, yang masing-masing mewakili tingkat kesulitan masalah tingkat magister dan doktoral. Di sini, Seed Prover 1.5 menyelesaikan 80% masalah Fate-H dan 33% masalah Fate-X yang sangat sulit, menetapkan rekor state-of-the-art baru untuk model penalaran formal pada evaluasi ini.
Mesin di Balik Terobosan: Pembelajaran Penguatan Agen Berskala Besar
Peningkatan dramatis dibandingkan pendahulunya dikaitkan dengan metodologi pelatihan baru yang digambarkan sebagai "Pembelajaran Penguatan Agen (RL) berskala besar." Pendekatan ini melampaui pelatihan standar pada dataset statis. Sebaliknya, model AI bertindak sebagai "agen" otonom yang secara aktif menjelajahi ruang pencarian yang luas dari langkah-langkah pembuktian yang mungkin. Ia belajar dengan mencoba membangun bukti, menerima umpan balik tentang keberhasilannya, dan terus menyempurnakan strateginya. Proses iteratif dan peningkatan diri ini adalah kunci untuk mengembangkan penalaran multi-langkah yang canggih yang diperlukan untuk matematika tingkat tinggi, yang mengarah pada peningkatan signifikan dalam kemampuan model dan efisiensinya dalam menemukan bukti.
Spesifikasi Teknis Inti:
- Fungsi Utama: Pembuktian teorema otomatis dan penalaran matematika formal.
- Format Keluaran: Menghasilkan kode bukti lengkap yang dapat diverifikasi mesin dalam pembuktir teorema Lean.
- Inovasi Pelatihan Kunci: Pembelajaran Penguatan Agen Berskala Besar (RL), memungkinkan eksplorasi dan penyempurnaan strategi pembuktian secara mandiri.
- Ketersediaan: Laporan teknis dan kode bukti diterbitkan pada 24 Desember 2025. API publik direncanakan untuk rilis di masa depan.
- Pengembang: Tim Seed ByteDance.
Implikasi dan Aksesibilitas Masa Depan
Rilis Seed Prover 1.5, disertai dengan laporan teknis dan kode bukti yang tersedia untuk umum, membuka jalan baru untuk kolaborasi antara AI dan matematikawan manusia. Ini dapat berfungsi sebagai asisten yang kuat, memeriksa kebenaran bukti kompleks, menyarankan strategi pembuktian potensial, atau mengeksplorasi konjektur. ByteDance telah mengumumkan rencana untuk membuka API untuk model ini, yang akan memungkinkan peneliti dan pengembang untuk mengintegrasikan kemampuan penalaran lanjutan ini ke dalam proyek mereka sendiri. Per 24 Desember 2025 pagi, pengumuman ini menempatkan ByteDance di garis depan ceruk penting dan berkembang pesat dalam penelitian AI, dengan implikasi jangka panjang potensial untuk penemuan dan verifikasi ilmiah.