Sistem pembuktian matematika Google DeepMind, AlphaProof Nexus, resmi terbit di Science. Penulis pertama makalah tercatat atas nama Tsoukalas, dan seluruh tim peneliti berasal dari DeepMind. Penelitian ini lebih dulu dirilis sebagai pracetak pada akhir Mei; kali ini yang terbit adalah versi jurnal setelah melalui telaah sejawat.
Rapor hasilnya tidak berubah: sistem mencoba 353 soal Erdős yang belum terpecahkan dan menyelesaikan 9 soal, 2 di antaranya sudah menggantung selama 56 tahun. Dari 492 konjektur terbuka di OEIS, basis data barisan bilangan bulat, sebanyak 44 berhasil dibuktikan. Sistem ini juga menjawab satu pertanyaan tentang fungsi Hilbert dalam geometri aljabar yang menggantung sekitar 15 tahun, dan memperbaiki satu batas yang sudah diketahui dalam optimisasi min-max.
Satu Gemini, satu kompilator Lean
Fondasi sistem ini adalah Gemini 3.1 Pro. Model menyusun draf bukti dalam bahasa formal Lean, kompilator Lean memeriksa setiap kali ada langkah yang diubah, dan pesan galatnya langsung diumpankan kembali ke percobaan berikutnya. Selama proses itu, manusia hanya melihat hasilnya di akhir.
Makalah memerinci empat versi:
- Versi A: putaran "hasilkan lalu verifikasi" yang paling polos, model besar menulis dan kompilator menilai;
- Versi B: A ditambah AlphaProof, pembukti buatan DeepMind sebelumnya, yang khusus mengisi potongan bukti yang hilang;
- Versi C: menambahkan mekanisme evolusi, dengan beberapa subagen berbagi satu kumpulan draf bukti yang diurutkan berdasarkan skor Elo;
- Versi D: semua hal di atas digabung, dipakai untuk menggarap soal-soal Erdős.
Hasil yang paling menarik adalah bahwa versi A juga membuktikan sendiri seluruh 9 soal Erdős tersebut, hanya saja biayanya lebih besar pada beberapa soal tersulit. Biaya inferensi yang dikutip The Decoder adalah beberapa ratus dolar AS per soal. Para penulis menyatakan dalam makalah:
"power of compiler feedback in grounding LLM reasoning"
(Umpan balik kompilator mampu membumikan penalaran model bahasa besar.)
Sejumlah catatan dari akademisi Spanyol
Pada hari makalah itu terbit, Science Media Centre Spanyol meminta tanggapan beberapa akademisi setempat, dan pendapat mereka terbelah dua.
Pablo Haya Coll, peneliti di UAM, menilai metode ini dapat secara sistematis menghasilkan penemuan matematika yang bobotnya nyata. Josep Curto dari UOC memberikan penilaian "a dazzling display of technical capability marred by significant methodological inconsistencies", yang kurang lebih berarti secara teknis menakjubkan tetapi secara metodologis jelas tidak konsisten. Ia menyebut tiga hal. Versi A dan D menyelesaikan soal yang sama, yang menunjukkan bahwa kompleksitas kerangka kerja belum tentu menentukan kemampuan menemukan. Biaya hanya dihitung untuk putaran yang berhasil, dan perhitungan versi B dan D juga tidak memasukkan biaya inferensi AlphaProof sendiri. Lalu, Lean hanya menjamin bahwa bukti berlaku untuk "pernyataan yang tertulis"; apakah pernyataan itu menerjemahkan soal aslinya dengan setia tetap harus diperiksa manual oleh matematikawan, dan makalah itu sendiri mengakui pernah terjadi kesalahan formalisasi.
Javier Aramayona, direktur ICMAT, mengkhawatirkan hal lain: munculnya banyak hasil yang "diketahui benar, tetapi tak seorang pun benar-benar memahaminya" dapat melemahkan tahap pemahaman dalam riset matematika serta proses pelatihan peneliti muda. Teodoro Calonge dari Universitas Valladolid berbicara lebih lugas, bahwa bidang ini masih punya ruang perbaikan yang cukup besar.
Para penulis juga menuliskan sendiri batasannya. Tingkat keberhasilan AI secara keseluruhan pada soal Erdős sekitar 1% hingga 2%, dan soal yang terselesaikan umumnya yang relatif mudah, terkonsentrasi pada kombinatorika, optimisasi konveks, dan teori bilangan, yakni bidang yang pustaka Mathlib-nya sudah tebal dan soalnya mudah dipecah menjadi subtujuan. Soal yang menuntut penemuan banyak teori baru pada dasarnya tidak terjangkau oleh sistem ini.
Menyambungkan beberapa peristiwa tahun ini
Pada Mei, situs ini melaporkan model OpenAI yang menaklukkan konjektur Erdős berusia 80 tahun. Pada September, terjadi perselisihan soal pencantuman nama antara para matematikawan dan OpenAI. Pada 6 Oktober, OpenAI merilis 722 naskah matematika buatan AI sekaligus di GitHub, memakai repositori sumber terbuka berlisensi Apache 2.0, tanpa melalui jurnal. Laporan The Decoder menyebut bahwa sekelompok matematikawan yang dipimpin Terence Tao kemudian menyerukan boikot terhadap cara ini.
Perbedaan jalur kedua perusahaan terlihat jelas di sini. OpenAI memilih jumlah besar dan terbuka, lalu menyerahkan penyaringan kepada komunitas. DeepMind memilih jumlah yang jauh lebih sedikit, tetapi setiap butirnya lolos kompilator Lean dan juga lolos telaah jurnal. Pihak yang terakhir ini juga menempatkan Lean secara hati-hati dalam makalahnya; kutipan aslinya, verifikasi formal "can serve as a filter for determining which proofs merit human review", yaitu sebagai penyaring untuk menentukan bukti mana yang layak dilihat manusia.
Hitung-hitungan kasar: dengan biaya beberapa ratus dolar per soal, biaya inferensi untuk 9 soal Erdős jauh di bawah gaji sebulan seorang peneliti pascadoktoral. Namun dengan acuan yang ditunjuk Curto, berapa besar tagihan akan bertambah setelah putaran yang gagal dan pemanggilan AlphaProof dimasukkan, makalah ini belum memberikan angka. DeepMind telah menaruh bukti-bukti dan sebagian penjelasannya di repositori alphaproof-nexus-results di GitHub, sehingga matematikawan luar dapat memeriksanya satu per satu.
Sumber: makalah jurnal Science, The Decoder, CocoLoop, tanggapan pakar dari Science Media Centre Spanyol; isi makalah telah dicek untuk 9 soal Erdős terselesaikan dari 353, 44 konjektur OEIS terbukti dari 492, dan pembagian peran keempat versi agen.