Pada hari Kamis, Google DeepMind diumumkan Sistem AI yang disebut AlphaProof dan AlphaGeometry 2 dilaporkan memecahkan empat dari enam masalah dari tahun ini Olimpiade Matematika Internasional (menurut saya), mencapai skor yang setara dengan medali perak. Raksasa teknologi itu mengklaim bahwa ini menandai pertama kalinya AI mencapai tingkat kinerja ini dalam kompetisi matematika bergengsi—tetapi seperti biasa dalam AI, klaimnya tidak sejelas yang terlihat.
Google mengatakan AlphaProof menggunakan pembelajaran penguatan untuk membuktikan pernyataan matematika dalam bahasa formal yang disebut BersandarSistem ini melatih dirinya sendiri dengan membuat dan memverifikasi jutaan bukti, secara bertahap menangani masalah yang lebih sulit. Sementara itu, AlphaGeometry 2 digambarkan sebagai versi yang ditingkatkan dari Google mode AI pemecahan geometri sebelumnyaIsekarang didukung oleh model bahasa berbasis Gemini yang dilatih pada data yang jauh lebih banyak.
Menurut Google, matematikawan terkemuka Tuan Timothy Gowers Dan Dokter Joseph Myers menilai solusi model AI menggunakan aturan resmi IMO. Perusahaan melaporkan sistem gabungannya memperoleh 28 dari 42 poin yang mungkin, hanya sedikit di bawah ambang batas medali emas 29 poin. Ini termasuk skor sempurna pada soal tersulit dalam kompetisi, yang menurut Google hanya dipecahkan oleh lima kontestan manusia tahun ini.
Kontes matematika yang tidak ada duanya
IMO, yang diadakan setiap tahun sejak 1959, mempertandingkan matematikawan pra-perguruan tinggi elit dengan soal-soal yang sangat sulit dalam aljabar, kombinatorik, geometri, dan teori bilangan. Kinerja pada soal-soal IMO telah menjadi tolok ukur yang diakui untuk menilai kemampuan penalaran matematika sistem AI.
Google menyatakan bahwa AlphaProof terselesaikan dua soal aljabar dan satu soal teori bilangan, sementara AlphaGeometry 2 menangani soal geometri. Model AI dilaporkan gagal memecahkan dua soal kombinatorik. Perusahaan mengklaim sistemnya memecahkan satu soal dalam hitungan menit, sementara yang lain membutuhkan waktu hingga tiga hari.
Google mengatakan bahwa mereka pertama-tama menerjemahkan soal-soal IMO ke dalam bahasa matematika formal agar dapat diproses oleh model AI-nya. Langkah ini berbeda dari kompetisi resmi, di mana kontestan manusia bekerja langsung dengan pernyataan soal selama dua sesi berdurasi 4,5 jam.
Google melaporkan bahwa sebelum kompetisi tahun ini, AlphaGeometry 2 dapat memecahkan 83 persen masalah geometri IMO historis dari 25 tahun terakhir, naik dari tingkat keberhasilan pendahulunya sebesar 53 persen. Perusahaan mengklaim sistem baru tersebut memecahkan masalah geometri tahun ini dalam 19 detik setelah menerima versi formal.
Keterbatasan
Meskipun Google mengklaim sebaliknya, Sir Timothy Gowers menawarkan perspektif yang lebih bernuansa mengenai model Google DeepMind dalam benang diposting di X. Sambil mengakui pencapaian tersebut sebagai “jauh melampaui apa yang dapat dilakukan oleh pembuktian teorema otomatis sebelumnya,” Gowers menunjukkan beberapa kualifikasi utama.
“Kualifikasi utamanya adalah bahwa program tersebut membutuhkan waktu lebih lama daripada pesaing manusia—untuk beberapa soal lebih dari 60 jam—dan tentu saja kecepatan pemrosesan yang jauh lebih cepat daripada otak manusia yang malang,” tulis Gowers. “Jika pesaing manusia diberi waktu sebanyak itu untuk setiap soal, mereka pasti akan mendapat skor lebih tinggi.”
Gowers juga mencatat bahwa manusia menerjemahkan masalah secara manual ke dalam bahasa formal Lean sebelum model AI mulai bekerja. Ia menekankan bahwa sementara AI melakukan penalaran matematika inti, langkah “autoformalisasi” ini dilakukan oleh manusia.
Mengenai implikasi yang lebih luas untuk penelitian matematika, Gowers menyatakan ketidakpastian. “Apakah kita sudah mendekati titik di mana matematikawan menjadi tidak relevan? Sulit untuk mengatakannya. Saya kira kita masih kurang satu atau dua terobosan dari itu,” tulisnya. Ia menyarankan bahwa waktu pemrosesan sistem yang lama menunjukkan bahwa sistem itu belum “memecahkan matematika”, tetapi mengakui bahwa “jelas ada sesuatu yang menarik terjadi saat sistem itu beroperasi.”
Bahkan dengan keterbatasan ini, Gowers berspekulasi bahwa sistem AI tersebut dapat menjadi alat penelitian yang berharga. “Jadi, kita mungkin akan segera memiliki program yang memungkinkan matematikawan memperoleh jawaban atas berbagai pertanyaan, asalkan pertanyaan tersebut tidak terlalu sulit—sesuatu yang dapat diselesaikan dalam beberapa jam. Itu akan sangat berguna sebagai alat penelitian, meskipun tidak mampu memecahkan masalah yang masih terbuka.”
