AI di Olimpiade Matematika Internasional: Bagaimana AlphaProof dan AlphaGeometry 2 Mencapai Standar Medali Perak

Penalaran matematika adalah aspek vital dari kemampuan kognitif manusia, yang mendorong kemajuan dalam penemuan ilmiah dan pengembangan teknologi. Ketika kita berusaha mengembangkan kecerdasan buatan umum yang sesuai dengan kognisi manusia, memberikan AI dengan kemampuan penalaran matematika yang maju adalah penting. Sementara sistem AI saat ini dapat menangani masalah matematika dasar, mereka bergelut dengan penalaran kompleks yang diperlukan untuk disiplin matematika lanjutan seperti aljabar dan geometri. Namun, hal ini mungkin berubah, karena Google DeepMind telah membuat kemajuan signifikan dalam meningkatkan kemampuan penalaran matematika sistem AI. Kemajuan ini dibuat di Olimpiade Matematika Internasional (IMO) 2024. Didirikan pada tahun 1959, IMO adalah kompetisi matematika tertua dan paling bergengsi, yang menantang siswa sekolah menengah dari seluruh dunia dengan masalah dalam aljabar, kombinatorik, geometri, dan teori bilangan. Setiap tahun, tim-tim muda matematikawan bersaing untuk menyelesaikan enam masalah yang sangat menantang. Tahun ini, Google DeepMind memperkenalkan dua sistem AI: AlphaProof, yang fokus pada penalaran matematika formal, dan AlphaGeometry 2, yang mengkhususkan diri dalam menyelesaikan masalah geometri. Sistem AI ini berhasil menyelesaikan empat dari enam masalah, dengan performa setara dengan medali perak. Dalam artikel ini, kita akan menjelajahi bagaimana sistem-sistem ini bekerja untuk menyelesaikan masalah matematika.

AlphaProof: Menggabungkan AI dan Bahasa Formal untuk Pembuktian Teorema Matematika

AlphaProof adalah sistem AI yang dirancang untuk membuktikan pernyataan matematika menggunakan bahasa formal Lean. Ini mengintegrasikan Gemini, model bahasa pra-dilatih, dengan AlphaZero, algoritma pembelajaran penguatan yang terkenal karena menguasai catur, shogi, dan Go.

Gemini menerjemahkan pernyataan masalah bahasa alami menjadi formal, menciptakan perpustakaan masalah dengan tingkat kesulitan yang bervariasi. Ini memiliki dua tujuan: menerjemahkan bahasa alami yang tidak tepat menjadi bahasa formal yang tepat untuk memverifikasi bukti matematika dan menggunakan kemampuan prediktif Gemini untuk menghasilkan daftar solusi yang mungkin dengan presisi bahasa formal.

Ketika AlphaProof menghadapi masalah, itu menghasilkan solusi potensial dan mencari langkah-langkah bukti di Lean untuk memverifikasi atau membantahnya. Ini pada dasarnya adalah pendekatan neuro-simbolik, di mana jaringan saraf, Gemini, menerjemahkan instruksi bahasa alami menjadi bahasa formal simbolik Lean untuk membuktikan atau membantah pernyataan. Serupa dengan mekanisme permainan mandiri AlphaZero, di mana sistem belajar dengan bermain game melawan dirinya sendiri, AlphaProof melatih dirinya dengan mencoba membuktikan pernyataan matematika. Setiap upaya bukti memperbarui model bahasa AlphaProof, dengan bukti yang sukses memperkuat kemampuan model untuk menangani masalah yang lebih menantang.

Untuk Olimpiade Matematika Internasional (IMO), AlphaProof dilatih dengan membuktikan atau membantah jutaan masalah yang mencakup berbagai tingkat kesulitan dan topik matematika. Pelatihan ini berlanjut selama kompetisi, di mana AlphaProof memperbarui solusinya sampai menemukan jawaban lengkap untuk masalah-masalah tersebut.

AlphaGeometry 2: Mengintegrasikan LLM dan AI Simbolik untuk Menyelesaikan Masalah Geometri

AlphaGeometry 2 adalah iterasi terbaru dari seri AlphaGeometry, yang dirancang untuk menangani masalah geometri dengan presisi dan efisiensi yang ditingkatkan. Membangun pada fondasi pendahulunya, AlphaGeometry 2 menggunakan pendekatan neuro-simbolik yang menggabungkan model bahasa besar (LLM) dengan AI simbolik. Integrasi ini menggabungkan logika berbasis aturan dengan kemampuan prediktif jaringan saraf untuk mengidentifikasi titik-titik bantu, yang penting untuk menyelesaikan masalah geometri. LLM di AlphaGeometry memprediksi konstruksi geometri baru, sementara AI simbolik menerapkan logika formal untuk menghasilkan bukti.

Ketika dihadapkan pada masalah geometri, LLM AlphaGeometry mengevaluasi banyak kemungkinan, memprediksi konstruksi yang penting untuk penyelesaian masalah. Prediksi-prediksi ini berfungsi sebagai petunjuk berharga, memandu mesin simbolik ke arah deduksi yang akurat dan maju ke arah solusi. Pendekatan inovatif ini memungkinkan AlphaGeometry untuk menangani tantangan geometri kompleks yang melampaui skenario konvensional.

Salah satu peningkatan kunci di AlphaGeometry 2 adalah integrasi LLM Gemini. Model ini dilatih dari awal pada data sintetis yang jauh lebih banyak daripada pendahulunya. Pelatihan ekstensif ini memungkinkannya menangani masalah geometri yang lebih sulit, termasuk yang melibatkan gerakan objek dan persamaan sudut, rasio, atau jarak. Selain itu, AlphaGeometry 2 menampilkan mesin simbolik yang beroperasi dua kali lipat lebih cepat, memungkinkannya untuk menjelajahi solusi alternatif dengan kecepatan yang belum pernah terjadi sebelumnya. Kemajuan-kemajuan ini membuat AlphaGeometry 2 menjadi alat yang kuat untuk menyelesaikan masalah geometri yang rumit, menetapkan standar baru di bidang ini.

AlphaProof dan AlphaGeometry 2 di IMO

Tahun ini di Olimpiade Matematika Internasional (IMO), peserta diuji dengan enam masalah yang beragam: dua dalam aljabar, satu dalam teori bilangan, satu dalam geometri, dan dua dalam kombinatorik. Peneliti Google menerjemahkan masalah-masalah ini ke dalam bahasa matematika formal untuk AlphaProof dan AlphaGeometry 2. AlphaProof menangani dua masalah aljabar dan satu masalah teori bilangan, termasuk masalah paling sulit dalam kompetisi, yang hanya diselesaikan oleh lima peserta manusia tahun ini. Sementara itu, AlphaGeometry 2 berhasil menyelesaikan masalah geometri, meskipun tidak menyelesaikan dua tantangan kombinatorik.

Setiap masalah di IMO bernilai tujuh poin, dengan total maksimum 42 poin. AlphaProof dan AlphaGeometry 2 meraih 28 poin, dengan skor sempurna pada masalah yang mereka selesaikan. Ini menempatkan mereka di ujung atas kategori medali perak. Ambang batas medali emas tahun ini adalah 29 poin, yang diraih oleh 58 dari 609 peserta.

Lompatan Berikutnya: Bahasa Alami untuk Tantangan Matematika

AlphaProof dan AlphaGeometry 2 telah menunjukkan kemajuan yang mengesankan dalam kemampuan sistem AI untuk menyelesaikan masalah matematika. Namun, sistem-sistem ini masih bergantung pada ahli manusia untuk menerjemahkan masalah matematika ke dalam bahasa formal untuk diproses. Selain itu, belum jelas bagaimana keterampilan matematika khusus ini dapat diintegrasikan ke dalam sistem AI lain, seperti untuk menjelajahi hipotesis, menguji solusi inovatif untuk masalah lama, dan mengelola aspek-aspek waktu yang menghabiskan waktu dari bukti.

Untuk mengatasi keterbatasan ini, peneliti Google sedang mengembangkan sistem penalaran bahasa alami berdasarkan Gemini dan penelitian terbaru mereka. Sistem baru ini bertujuan untuk meningkatkan kemampuan penyelesaian masalah tanpa memerlukan terjemahan bahasa formal dan dirancang untuk berintegrasi dengan mulus dengan sistem AI lain.

Ringkasan

Kinerja AlphaProof dan AlphaGeometry 2 di Olimpiade Matematika Internasional adalah lompatan besar ke depan dalam kemampuan AI untuk menangani penalaran matematika kompleks. Kedua sistem menunjukkan kinerja setara dengan medali perak dengan menyelesaikan empat dari enam masalah yang menantang, menunjukkan kemajuan signifikan dalam pembuktian formal dan penyelesaian masalah geometri. Meskipun pencapaian mereka, sistem AI ini masih bergantung pada input manusia untuk menerjemahkan masalah ke dalam bahasa formal dan menghadapi tantangan integrasi dengan sistem AI lain. Penelitian masa depan bertujuan untuk meningkatkan sistem-sistem ini lebih lanjut, kemungkinan dengan mengintegrasikan penalaran bahasa alami untuk memperluas kemampuan mereka di berbagai tantangan matematika.