berita

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Laporan Jantung Mesin

Departemen Editorial Jantung Mesin

Dengan menggunakan model besar Gemini dan algoritma pembelajaran penguatan AlphaZero, Anda dapat menguasai geometri, aljabar, dan teori bilangan.

Bagi AI, Olimpiade Matematika tidak lagi menjadi masalah.

Pada hari Kamis, kecerdasan buatan Google DeepMind menyelesaikan suatu prestasi: menggunakan AI untuk memecahkan pertanyaan sebenarnya dari Olimpiade Matematika Internasional IMO tahun ini, dan hanya selangkah lagi untuk memenangkan medali emas.

Kompetisi IMO yang baru berakhir minggu lalu ini memiliki enam soal yang melibatkan aljabar, kombinatorik, geometri, dan teori bilangan. Sistem AI hybrid yang diusulkan oleh Google menjawab empat pertanyaan dengan benar dan mencetak 28 poin, mencapai level medali perak.

Awal bulan ini, profesor tetap UCLA Terence Tao baru saja mempromosikan AI Mathematical Olympiad (AIMO Progress Award) dengan hadiah jutaan dolar. Tanpa diduga, tingkat penyelesaian masalah AI telah meningkat ke level ini sebelum bulan Juli.

IMO, kerjakan soal secara bersamaan dan jawab soal yang paling sulit dengan benar.

IMO merupakan kompetisi matematikawan muda tertua, terbesar dan paling bergengsi yang diadakan setiap tahun sejak tahun 1959. Baru-baru ini, kompetisi IMO juga telah diakui secara luas sebagai tantangan besar di bidang pembelajaran mesin, dan menjadi tolok ukur ideal untuk mengukur kemampuan penalaran matematis tingkat lanjut dari sistem kecerdasan buatan.

Pada kompetisi IMO tahun ini, AlphaProof dan AlphaGeometry 2 yang dikembangkan oleh tim DeepMind bersama-sama mencapai terobosan penting.

Diantaranya, AlphaProof adalah sistem pembelajaran penguatan untuk penalaran matematika formal, dan AlphaGeometry 2 adalah versi perbaikan dari sistem penyelesaian geometri DeepMind, AlphaGeometry.

Terobosan ini menunjukkan potensi kecerdasan umum buatan (AGI) dengan kemampuan penalaran matematis tingkat lanjut untuk membuka bidang ilmu pengetahuan dan teknologi baru.

Lantas, bagaimana sistem AI DeepMind berpartisipasi dalam kompetisi IMO?

Sederhananya, permasalahan matematika ini terlebih dahulu diterjemahkan secara manual ke dalam bahasa matematika formal agar sistem AI dapat memahaminya. Pada kompetisi resmi, kontestan manusia menyerahkan jawabannya dalam dua sesi (dua hari), dengan batas waktu 4,5 jam untuk setiap sesi. Sistem AI yang terdiri dari AlphaProof+AlphaGeometry 2 memecahkan satu masalah dalam beberapa menit, namun membutuhkan waktu tiga hari untuk menyelesaikan masalah lainnya. Meskipun jika Anda mengikuti aturan dengan ketat, waktu sistem DeepMind telah habis. Beberapa orang berspekulasi bahwa ini mungkin melibatkan banyak brute force cracking.

AlphaProof memecahkan dua soal aljabar dan satu soal teori bilangan dengan menentukan jawaban dan membuktikan kebenarannya, kata Google. Ini termasuk masalah tersulit dalam kompetisi, yang hanya diselesaikan oleh lima kontestan di IMO tahun ini. Dan AlphaGeometry 2 membuktikan masalah geometri.

Solusi yang diberikan oleh AI: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

Peraih medali emas IMO dan Peraih Medali Bidang Timothy Gowers dan peraih medali emas IMO dua kali Dr. Joseph Myers, ketua Komite Seleksi Masalah IMO 2024, menilai solusi yang diberikan oleh sistem gabungan sesuai dengan aturan penilaian IMO.

Masing-masing dari enam pertanyaan bernilai 7 poin, dengan total skor maksimal 42 poin. Sistem DeepMind mendapat skor akhir 28, artinya keempat soal yang diselesaikannya mendapat skor sempurna – setara dengan skor tertinggi pada kategori medali perak. Ambang batas medali emas tahun ini adalah 29 poin, dan 58 dari 609 pemain di kompetisi resmi memenangkan medali emas.

Grafik ini menunjukkan performa sistem kecerdasan buatan Google DeepMind dibandingkan kompetitor manusia di IMO 2024. Sistem ini mencetak 28 poin dari total 42 poin, mencapai level yang sama dengan peraih medali perak kompetisi. Selain itu, tahun ini 29 poin bisa merebut medali emas.

AlphaProof: metode penalaran formal

Di antara sistem AI hybrid yang digunakan oleh Google, AlphaProof adalah sistem terlatih yang menggunakan bahasa formal Lean untuk membuktikan pernyataan matematika. Ini menggabungkan model bahasa terlatih dengan algoritma pembelajaran penguatan AlphaZero.

Diantaranya, bahasa formal memberikan keuntungan penting untuk memverifikasi kebenaran penalaran matematis secara formal. Hingga saat ini, penggunaannya dalam pembelajaran mesin masih terbatas karena jumlah data yang ditulis manusia sangat terbatas.

Sebaliknya, metode berbasis bahasa alami, meskipun memiliki akses ke sejumlah besar data, menghasilkan langkah-langkah penalaran dan solusi perantara yang tampaknya masuk akal namun tidak benar.

Google DeepMind membangun jembatan antara dua bidang yang saling melengkapi ini dengan menyempurnakan model Gemini untuk secara otomatis menerjemahkan pernyataan masalah bahasa alami menjadi pernyataan formal, sehingga menciptakan perpustakaan besar masalah formal dengan tingkat kesulitan yang berbeda-beda.

Mengingat masalah matematika, AlphaProof menghasilkan kandidat solusi dan kemudian membuktikannya dengan mencari langkah pembuktian yang mungkin di Lean. Setiap solusi bukti yang ditemukan dan diverifikasi digunakan untuk memperkuat model bahasa AlphaProof dan meningkatkan kemampuannya untuk memecahkan masalah berikutnya yang lebih menantang.

Untuk melatih AlphaProof, Google DeepMind membuktikan atau menyangkal jutaan soal matematika yang mencakup berbagai kesulitan dan topik dalam minggu-minggu menjelang kompetisi IMO. Loop pelatihan juga diterapkan selama kompetisi untuk memperkuat pembuktian varian masalah kompetisi yang dihasilkan sendiri hingga solusi lengkap ditemukan.

Infografis proses loop pelatihan penguatan AlphaProof: Sekitar satu juta masalah matematika informal diterjemahkan ke dalam bahasa matematika formal oleh jaringan formal. Pemecah masalah kemudian mencari bukti atau penolakan masalah di jaringan, secara bertahap melatih dirinya sendiri untuk memecahkan masalah yang lebih menantang menggunakan algoritma AlphaZero.

AlphaGeometri 2 yang lebih kompetitif

AlphaGeometry 2 adalah versi AI matematika AlphaGeometry yang ditingkatkan secara signifikan yang muncul di majalah Nature tahun ini. Ini adalah sistem hibrida neuro-simbolis di mana model bahasa didasarkan pada Gemini dan dilatih dari awal pada data sintetis yang jauh lebih banyak daripada pendahulunya. Hal ini membantu model memecahkan masalah geometri yang lebih menantang, termasuk masalah gerak benda dan persamaan sudut, proporsi, atau jarak.

AlphaGeometry 2 menampilkan mesin simbolis yang dua kali lipat lebih cepat dari pendahulunya. Ketika masalah baru ditemui, mekanisme berbagi pengetahuan baru memungkinkan kombinasi tingkat lanjut dari pohon pencarian yang berbeda untuk memecahkan masalah yang lebih kompleks.

Sebelum kompetisi tahun ini, AlphaGeometry 2 dapat memecahkan 83% dari semua masalah geometri IMO historis selama 25 tahun terakhir, dibandingkan dengan hanya 53% dari pendahulunya. Di IMO 2024, AlphaGeometry 2 menyelesaikan soal 4 dalam waktu 19 detik setelah menerima formalisasinya.

Contoh soal 4 memerlukan pembuktian bahwa jumlah ∠KIL dan ∠XPY sama dengan 180°. AlphaGeometry 2 mengusulkan untuk membangun titik E pada garis BI sedemikian rupa sehingga ∠AEB = 90°. Titik E membantu memberi makna pada titik tengah L ruas garis AB, sehingga tercipta banyak pasangan segitiga sebangun, seperti ABE ~ YBI dan ALE ~ IPC, untuk membuktikan kesimpulannya.

Google DeepMind juga melaporkan bahwa sebagai bagian dari pekerjaan IMO, para peneliti juga bereksperimen dengan sistem penalaran bahasa alami baru berdasarkan Gemini dan sistem penalaran bahasa alami yang canggih, dengan harapan dapat mencapai kemampuan pemecahan masalah tingkat lanjut. Sistem ini tidak memerlukan penerjemahan pertanyaan ke dalam bahasa formal dan dapat dikombinasikan dengan sistem AI lainnya. Pada ujian soal kompetisi IMO tahun ini, "menunjukkan potensi yang besar".

Google terus mengeksplorasi metode AI untuk memajukan penalaran matematis dan berencana untuk segera merilis rincian teknis lebih lanjut tentang AlphaProof.

Kami sangat antusias dengan masa depan di mana ahli matematika akan menggunakan alat AI untuk mengeksplorasi hipotesis, mencoba pendekatan baru yang berani untuk memecahkan masalah yang sudah lama ada, dan dengan cepat menyelesaikan elemen pembuktian yang memakan waktu—dan sistem AI seperti Gemini akan membuat perbedaan besar dalam hal ini. matematika dan banyak lagi. Aspek penalaran yang luas menjadi lebih kuat.

tim peneliti

Google mengatakan penelitian baru ini didukung oleh Olimpiade Matematika Internasional, dan sebagai tambahan:

Pengembangan AlphaProof dipimpin oleh Thomas Hubert, Rishi Mehta, dan Laurent Sartran; kontributor utama termasuk Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland dan Grace Margand.

Diantaranya, Aja Huang, Julian Schrittwieser, Yannick Schroecker dan anggota lainnya juga merupakan anggota inti makalah AlphaGo 8 tahun lalu (2016). Delapan tahun lalu, AlphaGo, yang mereka bangun berdasarkan pembelajaran penguatan, menjadi terkenal. Delapan tahun kemudian, pembelajaran penguatan kembali bersinar di AlphaProof. Seseorang mengeluh di lingkaran pertemanan: RL sudah kembali!

Pekerjaan AlphaGeometry 2 dan inferensi bahasa alami dipimpin oleh Thang Luong. Pengembangan AlphaGeometry 2 dipimpin oleh Trieu Trinh dan Yuri Chervonyi, dengan kontribusi penting dari Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang, dan Marcelo Menegali.

Selain itu, David Silver, Quoc Le, Hassabis dan Pushmeet Kohli bertanggung jawab untuk mengoordinasikan dan mengelola keseluruhan proyek.

Konten referensi:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/