berita

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

Laporan Kebijaksanaan Baru

Editor: Departemen Editorial

[Pengantar Kebijaksanaan Baru] Baru saja, model matematika terbaru Google DeepMind memenangkan medali perak Olimpiade Matematika IMO! Tidak hanya menyelesaikan 4 dari 6 soal dengan nilai sempurna, hanya terpaut 1 poin dari medali emas, tetapi juga hanya membutuhkan waktu 19 detik untuk menyelesaikan soal ke-4.Kualitas dan kecepatan penyelesaian soal membuat para juri manusia yang mencetak gol tercengang .

AI telah memenangkan medali perak Olimpiade Matematika IMO!

Baru saja, Google DeepMind mengumumkan bahwa pertanyaan sebenarnya dari Olimpiade Matematika Internasional tahun ini dihasilkan oleh sistem AI miliknya sendiri.

Diantaranya, AI tidak hanya berhasil menyelesaikan 4 dari 6 soal, tetapi juga mendapat nilai penuh untuk setiap soal, yang setara dengan skor tertinggi medali perak - 28 poin.

Hasil ini hanya terpaut 1 poin dari medali emas!

Dari 609 peserta, hanya 58 yang meraih medali emas

Pada kompetisi resmi, kontestan manusia akan menyerahkan jawabannya dalam dua sesi, dengan batas waktu setiap kali 4,5 jam.

Menariknya, AI hanya membutuhkan beberapa menit untuk menjawab salah satu pertanyaan, namun pertanyaan lainnya membutuhkan waktu tiga hari penuh, yang bisa dikatakan sebagai timeout yang serius.

Yang memberikan kontribusi besar kali ini adalah dua sistem AI-AlphaProof dan AlphaGeometry 2.

Poin penting: IMO 2024 tidak ada dalam data pelatihan kedua AI ini.

Scott Wu, salah satu pendiri di balik insinyur AI Devin (peraih medali emas IOI tiga kali) mengeluh, “Ketika saya masih kecil, saya hanya punya olimpiade. Saya tidak pernah berpikir bahwa 10 tahun kemudian, olimpiade akan digantikan oleh AI . terselesaikan".

Pada kompetisi IMO tahun ini, terdapat enam soal kompetisi yang melibatkan aljabar, kombinatorik, geometri, dan teori bilangan. Enam jalur menjadi empat, mari kita rasakan tingkat AI——

Kemampuan penalaran matematis AI mengejutkan profesor

Kita semua tahu bahwa AI sebelumnya terbatas dalam menyelesaikan masalah matematika karena keterbatasan kemampuan penalaran dan data pelatihan.

Kedua pemain AI yang tampil bersama hari ini melanggar batasan ini. mereka masing-masing--

- AlphaProof, sistem baru untuk penalaran matematika formal berdasarkan pembelajaran penguatan

- AlphaGeometry 2, sistem pemecahan masalah geometri generasi kedua

Jawaban yang diberikan kedua AI dinilai sesuai aturan oleh matematikawan terkenal Profesor Timothy Gowers (Peraih Medali Emas IMO dan Peraih Medali Fields) dan Dr. Joseph Myers (peraih Medali Emas IMO dua kali dan Ketua Panitia Seleksi Soal IMO 2024) .

Pada akhirnya, AlphaProof dengan benar menyelesaikan dua pertanyaan aljabar dan satu pertanyaan teori bilangan. Salah satu pertanyaan tersulit diselesaikan hanya oleh 5 kontestan manusia di IMO tahun ini; AlphaGeometry 2 memecahkan pertanyaan geometri.

Hanya ada dua soal matematika kombinatorial yang belum terselesaikan.

Profesor Timothy Gowers juga sangat terkejut selama proses penilaian——

Bahwa suatu program dapat menghasilkan solusi yang tidak jelas merupakan suatu hal yang sangat mengesankan dan jauh melampaui apa yang saya harapkan mengingat kondisi terkini.

Bukti Alfa

AlphaProof adalah sistem yang mampu membuktikan proposisi matematika dalam bahasa formal Lean.

Ini menggabungkan model bahasa besar yang telah dilatih sebelumnya dengan algoritma pembelajaran penguatan AlphaZero, yang belajar sendiri untuk menguasai catur, shogi, dan Go.

Keuntungan utama bahasa formal adalah bahasa tersebut dapat diverifikasi secara formal untuk pembuktian yang melibatkan penalaran matematis. Namun, penerapannya dalam pembelajaran mesin masih terbatas karena terbatasnya jumlah data relevan yang ditulis oleh manusia.

Sebaliknya, pendekatan berbasis bahasa alami, meskipun memiliki akses terhadap sejumlah besar data, dapat menghasilkan langkah-langkah dan solusi penalaran perantara yang masuk akal, namun salah.

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

Saat memecahkan masalah, AlphaProof menghasilkan kandidat solusi dan membuktikan atau menyangkalnya dengan mencari kemungkinan langkah pembuktian di Lean.

Setiap bukti yang ditemukan dan diverifikasi digunakan untuk memperkuat model bahasa AlphaProof sehingga dapat menyelesaikan permasalahan yang lebih sulit di masa mendatang.

Untuk melatih AlphaProof, para peneliti membuktikan atau menyangkal jutaan pertanyaan yang mencakup berbagai tingkat kesulitan dan topik matematika dari minggu-minggu menjelang dan selama kompetisi.

Selama kompetisi, mereka juga menerapkan loop pelatihan dengan memperkuat pembuktian variasi masalah kompetisi yang dihasilkan sendiri hingga solusi lengkap ditemukan.

Infografis alur loop pelatihan pembelajaran penguatan AlphaProof: sekitar satu juta masalah matematika informal diterjemahkan oleh jaringan formal ke dalam bahasa matematika formal; jaringan pemecah kemudian secara bertahap melatih dirinya sendiri menggunakan algoritma AlphaZero dengan mencari bukti atau sanggahan dari masalah tersebut , untuk memecahkan masalah yang lebih menantang

AlfaGeometri 2

AlphaGeometry 2, versi AlphaGeometry yang ditingkatkan, adalah sistem hibrida saraf-simbolis yang dilatih dari awal berdasarkan model bahasa Gemini.

Berdasarkan data sintetik yang jauh lebih banyak dibandingkan generasi sebelumnya, ia dapat memecahkan masalah geometri yang lebih sulit, termasuk persamaan yang melibatkan gerak benda, sudut, proporsi, jarak, dll.

Selain itu, ia dilengkapi mesin simbolis yang dua kali lipat lebih cepat dari pendahulunya. Ketika masalah baru ditemui, sistem ini menggunakan mekanisme berbagi pengetahuan baru yang memungkinkan kombinasi tingkat lanjut dari pohon pencarian yang berbeda untuk memecahkan masalah yang lebih kompleks.

Sebelum berpartisipasi dalam IMO tahun ini, AlphaGeometry 2 telah mencapai banyak keberhasilan: mampu menyelesaikan 83% permasalahan geometri IMO dalam 25 tahun terakhir, sedangkan generasi pertama hanya mampu menyelesaikan 53%.

Di IMO ini, kecepatan AlphaGeometry 2 mengejutkan semua orang - dalam waktu 19 detik setelah menerima pertanyaan formal, ia menyelesaikan pertanyaan 4!

Soal 4 memerlukan bukti bahwa jumlah ∠KIL dan ∠XPY sama dengan 180°. AlphaGeometry 2 merekomendasikan pembuatan titik E pada garis BI sedemikian rupa sehingga ∠AEB=90°.Titik E membantu menentukan titik tengah L AB sehingga membentuk banyak pasangan segitiga yang sebangun, seperti ABE ~ YBI dan ALE ~ IPC, sehingga membuktikan kesimpulannya

Proses pemecahan masalah AI

Perlu disebutkan bahwa pertanyaan-pertanyaan ini pertama-tama akan diterjemahkan secara manual ke dalam bahasa matematika formal sebelum diserahkan ke AI.
P1

Secara umum, soal pertama (P1) di setiap tes IMO relatif mudah.

Netizen berkata, "P1 hanya membutuhkan pengetahuan matematika SMA, dan pemain manusia biasanya menyelesaikannya dalam waktu 60 menit."

Soal pertama IMO 2024 terutama mengkaji sifat-sifat bilangan real α, dan memerlukan pencarian bilangan real α yang memenuhi kondisi tertentu.

AI memberikan jawaban yang benar - α adalah bilangan bulat genap. Jadi, bagaimana sebenarnya jawabannya?

Pada langkah pertama penyelesaian masalah, AI terlebih dahulu memberikan teorema bahwa himpunan kiri dan kanan adalah sama.

Himpunan di sebelah kiri menyatakan bahwa semua bilangan real α yang memenuhi syarat, untuk sembarang bilangan bulat positif n, n dapat membagi ⌊i*α⌋ dari 1 sampai n; himpunan di sebelah kanan menyatakan bahwa ada bilangan bulat k, k adalah bilangan genap, dan bilangan real α sama dengan k.

Pembuktian berikut ini terbagi menjadi dua arah.

Buktikan terlebih dahulu bahwa himpunan di sebelah kanan merupakan himpunan bagian (arah sederhana) dari himpunan di sebelah kiri.

Kemudian buktikan bahwa himpunan di sebelah kiri merupakan himpunan bagian dari himpunan di sebelah kanan (arah sukar).

Hingga akhir kode, AI menghasilkan persamaan kunci ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), menggunakan persamaan tersebut untuk membuktikan bahwa α pasti merupakan bilangan genap.

Terakhir, DeepMind merangkum tiga aksioma yang diandalkan AI dalam proses pemecahan masalah: propext, Classical.choice, dan Quot.sound.

Berikut proses penyelesaian masalah P1 secara lengkap: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

Soal kedua mengkaji hubungan antara pasangan bilangan bulat positif (a, b), yang melibatkan sifat pembagi persekutuan terbesar.

Jawaban yang dipecahkan oleh AI adalah:

Teoremanya adalah untuk pasangan bilangan bulat positif (a, b) yang memenuhi kondisi tertentu, himpunannya hanya dapat memuat (1,1).

Dalam proses pemecahan masalah berikut, strategi pembuktian yang diadopsi oleh AI adalah membuktikan terlebih dahulu bahwa (1,1) memenuhi kondisi yang diberikan, dan kemudian membuktikan bahwa ini adalah satu-satunya solusi.

Buktikan bahwa (1,1) adalah penyelesaian akhir dengan menggunakan g=2, N=3.

Tunjukkan bahwa jika (a,b) adalah penyelesaiannya, maka ab+1 harus membagi g.

Dalam proses ini, AI menggunakan teorema Euler dan properti operasi modular untuk penalaran.

Terakhir, buktikan bahwa a=b=1 adalah satu-satunya solusi yang mungkin.

Berikut proses penyelesaian masalah P2 secara lengkap: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

Halaman 4

P4 adalah soal pembuktian geometri yang memerlukan pembuktian hubungan sudut geometri tertentu.

Seperti disebutkan di atas, ini diselesaikan oleh AlphaGeometry 2 dalam 19 detik, mencetak rekor baru.

Bergantung pada solusi yang diberikan, seperti halnya AlphaGeometry generasi pertama, titik tambahan di semua solusi secara otomatis dihasilkan oleh model bahasa.

Buktinya, semua pelacakan sudut menggunakan eliminasi Gaussian, dan d(AB)−d(CD) sama dengan sudut arah dari AB ke CD (modulo π).

Selama proses pemecahan masalah, AI akan secara manual menandai pasangan segitiga sebangun dan segitiga kongruen (ditandai dengan warna merah).

Selanjutnya adalah langkah-langkah penyelesaian masalah AlfaGeometri yang diselesaikan dengan menggunakan “metode rekontradiksi”.

Pertama gunakan Lean untuk memformalkan proposisi yang perlu dibuktikan dan memvisualisasikan konstruksi geometris.

Langkah-langkah kunci dalam pembuktian adalah sebagai berikut.

Lihat gambar di bawah untuk proses penyelesaian masalah selengkapnya: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

Hal.6

Pertanyaan IMO keenam adalah "bos utama", yang mengeksplorasi sifat-sifat fungsi dan memerlukan pembuktian kesimpulan spesifik tentang bilangan rasional.

AI memecahkan, c=2.

Pertama-tama mari kita lihat pernyataan teorema, yang mendefinisikan properti "fungsi Aquaesulian" dan menyatakan bahwa untuk semua fungsi tersebut, himpunan nilai f(r)+f(-r) memiliki paling banyak 2 elemen.

Strategi pembuktiannya adalah dengan membuktikan terlebih dahulu bahwa untuk setiap fungsi Aquaesulian, himpunan nilai f(r)+f(-r) memiliki paling banyak 2 elemen. Kemudian buatlah fungsi Aquaesulian tertentu sehingga f(r)+f(-r) memiliki tepat 2 nilai yang berbeda.

Buktikan bahwa ketika f(0)=0, f(x)+f(-x) mempunyai paling banyak dua nilai yang berbeda, dan buktikan bahwa tidak ada fungsi Aquaesulian f(0)≠0.

Bangunlah fungsi f(x)=-x+2⌈x⌉ dan buktikan bahwa fungsi tersebut merupakan fungsi Aquaesulian.

Terakhir, buktikan bahwa untuk fungsi ini, f(-1)+f(1) =0 dan f(1/2)+f(-1/2)=2 adalah dua nilai yang berbeda.

Berikut proses penyelesaian masalah selengkapnya: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Anda bisa mengerjakan soal matematika Olimpiade, tapi bisakah Anda membedakan mana yang lebih besar, 9.11 atau 9.9?

Andrew Gao, peneliti di Universitas Stanford dan Sequoia, menegaskan pentingnya terobosan AI ini—

Kuncinya adalah soal tes IMO terbaru tidak termasuk dalam set pelatihan. Hal ini penting karena menunjukkan bahwa AI dapat menangani masalah baru yang tidak terlihat.

Selain itu, permasalahan geometri yang berhasil diselesaikan oleh AI selalu dianggap sangat menantang karena sifat ruang yang terlibat (membutuhkan pemikiran intuitif dan imajinasi spasial).

Jim Fan, ilmuwan senior di Nvidia, memposting artikel panjang yang mengatakan bahwa model besar adalah keberadaan misterius——

Mereka bisa meraih medali perak di olimpiade matematika dan sering melakukan kesalahan pada pertanyaan seperti "Angka mana yang lebih besar, 9,11 atau 9,9?"

Tidak hanya Gemini, GPT-4o, Claude-3.5, dan Llama-3 juga tidak bisa menjawab 100% benar.

Dengan melatih model AI, kita menjelajahi area luas di luar kecerdasan kita.Dalam prosesnya, kami menemukan area yang sangat aneh - sebuah planet ekstrasurya yang terlihat seperti Bumi tetapi penuh dengan lembah yang aneh

Hal ini tampaknya tidak masuk akal, namun kami dapat menjelaskannya menggunakan distribusi data pelatihan:

AlphaProof dan AlphaGeometry 2 dilatih tentang bukti formal dan mesin simbolik khusus domain. Sampai batas tertentu, mereka lebih baik dalam memecahkan masalah Olimpiade khusus, meskipun mereka dibangun di atas LLM tujuan umum. Kumpulan pelatihan GPT-4o dicampur dengan sejumlah besar data kode GitHub, yang mungkin jauh melebihi data matematika. Di antara versi perangkat lunak, "v9.11 > v9.9" mungkin sangat mengganggu distribusi data. Oleh karena itu, kesalahan ini sampai batas tertentu dapat dimengerti.

Kepala pengembang Google mengatakan bahwa model yang dapat memecahkan masalah matematika dan fisika yang sulit adalah jalur utama menuju AGI, dan hari ini kami telah mengambil langkah lain di jalur tersebut.

Netizen lain mengatakan terlalu banyak informasi minggu ini.

Referensi:

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

https://x.com/DrJimFan/status/1816521330298356181