Google DeepMind telah mengembangkan AlphaProof, sistem AI yang menyamai performa medali perak di Olimpiade Matematika Internasional 2024, mencetak 28 dari 42 poin. Sistem ini hanya kurang satu poin dari emas di kompetisi matematika sarjana paling bergengsi di dunia. Terobosan ini menunjukkan kemajuan dalam kemampuan AI untuk menangani bukti matematika kompleks.
Komputer telah lama unggul dalam perhitungan tetapi kesulitan dengan penalaran logis yang diperlukan untuk matematika lanjutan. AI baru dari Google DeepMind, AlphaProof, mengatasi ini dengan mencapai performa medali perak di Olimpiade Matematika Internasional 2024 (IMO), kompetisi matematika tingkat sekolah menengah teratas. IMO menampilkan enam soal senilai tujuh poin masing-masing, total 42 poin. Medali emas memerlukan 29 poin atau lebih, dicapai oleh 58 dari 609 peserta, sementara perak diberikan kepada mereka yang mencetak 22-28 poin, dengan 123 penerima. AlphaProof mencetak 28 poin, menyelesaikan empat soal secara independen untuk 21 poin dan mengandalkan AlphaGeometry 2 yang spesialis untuk soal geometri guna mencapai level perak.
Pengembangan AlphaProof dimulai dengan mengatasi keterbatasan data pelatihan untuk bukti matematika formal. Tim menggunakan perangkat lunak Lean, alat untuk definisi dan verifikasi matematika yang presisi. Untuk memperluas dataset, mereka melatih model bahasa besar Gemini untuk menerjemahkan pernyataan matematika bahasa alami ke Lean, menghasilkan sekitar 80 juta pernyataan formal. Seperti yang dijelaskan Thomas Hubert, peneliti DeepMind dan penulis utama, “Kesulitan utama bekerja dengan bahasa formal adalah bahwa ada sangat sedikit data.” Meskipun ada ketidaksempurnaan, “Ada banyak cara untuk memanfaatkan terjemahan aproksimasi,” tambahnya.
Arsitektur sistem mengambil dari AlphaZero milik DeepMind, menggabungkan jaringan saraf yang dilatih melalui trial and error dengan algoritma pencarian pohon untuk mengeksplorasi jalur bukti. Ia memberi hadiah pada bukti yang benar dan menghukum langkah-langkah tidak efisien, mempromosikan solusi elegan. Penambahan baru, Test-Time Reinforcement Learning (TTRL), memungkinkan AlphaProof menghasilkan variasi soal sulit untuk pelatihan saat itu juga, meniru pemecahan masalah manusia. “Kami mencoba mempelajari permainan ini melalui trial and error,” kata Hubert.
Namun, AlphaProof memerlukan bantuan manusia untuk memformalisasikan soal dalam Lean dan memakan waktu beberapa hari per soal menantang, mengonsumsi ratusan hari-TPU—jauh melampaui batas waktu manusia 4,5 jam per sesi. Hanya enam manusia yang menyelesaikan soal tersulit; AlphaProof adalah yang ketujuh. DeepMind mengakui biaya komputasi tinggi tetapi bertujuan mengoptimalkan untuk penggunaan lebih luas. “Kami tidak ingin berhenti di kompetisi matematika. Kami ingin membangun sistem AI yang benar-benar berkontribusi pada matematika tingkat penelitian,” kata Hubert. Tim berencana program penguji tepercaya untuk berbagi alat AlphaProof dengan ahli matematika.
Pekerjaan ini dirinci dalam makalah Nature 2025 (DOI: 10.1038/s41586-025-09833-y).