AI DeepMind menyelesaikan soal Olimpiade Matematika Internasional pada tingkat medali perak

 (deepmind.google)
3 poin oleh GN⁺ 2024-07-26 | 3 komentar | Bagikan ke WhatsApp
  • AlphaProof dan AlphaGeometry 2 dari Google DeepMind berhasil menyelesaikan soal Olimpiade Matematika Internasional
    • AlphaProof: sistem penalaran matematis berbasis reinforcement learning
    • AlphaGeometry 2: sistem pemecahan soal geometri yang ditingkatkan
    • Kedua sistem tersebut menyelesaikan 4 dari 6 soal pada Olimpiade Matematika Internasional (IMO) tahun ini, mencapai performa setara medali perak

Pencapaian AI dalam menyelesaikan masalah matematika yang kompleks

  • Pengenalan IMO

    • Kompetisi matematika remaja tertua dan paling bergengsi yang diadakan setiap tahun sejak 1959
    • Soal kompetisi mencakup aljabar, kombinatorika, geometri, teori bilangan, dan bidang lainnya
    • Banyak peraih Fields Medal berasal dari IMO

  • Tantangan IMO bagi sistem AI

    • AlphaProof dan AlphaGeometry 2 menyelesaikan soal IMO tahun ini
    • Soal dinilai sesuai aturan resmi kompetisi
    • AlphaProof menyelesaikan 2 soal aljabar dan 1 soal teori bilangan
    • AlphaGeometry 2 menyelesaikan 1 soal geometri
    • Dua soal kombinatorika tidak berhasil diselesaikan
    • Total memperoleh 28 dari 42 poin, mencapai performa setara medali perak

AlphaProof: pendekatan penalaran formal

  • Cara kerja AlphaProof

    • Membuktikan proposisi matematika dalam bahasa formal Lean
    • Menggabungkan model bahasa yang telah dipra-latih dengan algoritma reinforcement learning AlphaZero
    • Menerjemahkan soal bahasa alami menjadi proposisi formal untuk menyelesaikan soal dengan berbagai tingkat kesulitan
    • Saat soal diberikan, AlphaProof menghasilkan kandidat solusi lalu membuktikan atau membantahnya
    • Hasil yang berhasil dibuktikan memperkuat model bahasa AlphaProof sehingga meningkatkan kemampuan menyelesaikan soal yang lebih sulit

  • Proses pelatihan

    • Dilatih dengan membuktikan atau membantah jutaan soal
    • Selama periode kompetisi pun loop pelatihan diterapkan untuk membuktikan variasi soal

AlphaGeometry 2 yang lebih kompetitif

  • Peningkatan pada AlphaGeometry 2

    • Model bahasa berbasis Gemini dan sistem hibrida neural-simbolik
    • Dilatih dengan data sintetis 10 kali lebih banyak daripada versi sebelumnya
    • Kecepatan dan akurasi penyelesaian soal geometri meningkat
    • Menggunakan mekanisme berbagi pengetahuan saat menyelesaikan soal baru

  • Pencapaian IMO 2024

    • Menyelesaikan 83% soal geometri IMO selama 25 tahun terakhir
    • Menyelesaikan soal nomor 4 pada kompetisi tahun ini hanya dalam 19 detik

Frontier baru dalam penalaran matematis

  • Eksperimen sistem penalaran bahasa alami

    • Eksperimen sistem penalaran bahasa alami berbasis Gemini
    • Dapat menyelesaikan soal tanpa menerjemahkannya ke bahasa formal
    • Menjelajahi kemungkinan untuk digabungkan dengan sistem AI lain

  • Prospek ke depan

    • Matematikawan dapat berkolaborasi dengan alat AI untuk mengeksplorasi hipotesis baru, mencoba pendekatan pemecahan masalah, dan mempersingkat proses pembuktian
    • Sistem AI seperti Gemini meningkatkan kemampuan matematika dan penalaran umum

Ringkasan GN⁺

  • AlphaProof dan AlphaGeometry 2 menunjukkan potensi AI dalam penalaran matematis
  • Mencapai performa setara medali perak di Olimpiade Matematika Internasional, membuktikan kemampuan AI dalam memecahkan soal matematika
  • Membuka kemungkinan bagi matematikawan untuk berkolaborasi dengan AI dalam menjelajahi pendekatan pemecahan masalah yang baru
  • Proyek dengan fungsi serupa mencakup model pemrosesan bahasa alami seperti GPT-3 dari OpenAI

Bacaan terkait

3 komentar

 
chabulhwi 2024-07-26

Semakin banyak matematikawan yang berkontribusi pada pengembangan pustaka matematika formal, akan semakin mudah membuat AI matematika dengan kinerja tinggi. Setahu saya, saat ini ada 3 orang Korea yang sedang memindahkan teori matematika yang mereka formalkan sendiri ke dalam bahasa asisten pembuktian Lean ke pustaka matematika Lean, Mathlib.

Tahun lalu saya ikut sedikit berpartisipasi dalam pekerjaan memindahkan Mathlib dari Lean 3 ke Lean 4, dan tahun ini saya membuktikan satu teorema yang belum terselesaikan di pustaka baterai Lean 4.
 
GN⁺ 2024-07-26
Komentar Hacker News

  • Komentar pertama

    • Sangat antusias dengan proyek ini, tetapi tidak jelas seberapa besar kontribusi komputer dalam proses menerjemahkan soal matematika ke bahasa formal
    • Dari solusi yang dapat diunduh, tidak jelas apakah itu diputuskan manusia selama proses penerjemahan atau ditemukan oleh komputer

  • Komentar kedua

    • Di IMO, medali diberikan kepada 50% peserta, dan rasio medali emas, perak, dan perunggu adalah 1:2:3
    • Mengesankan bahwa AI menyelesaikan soal lebih baik daripada 75% siswa
    • Namun, waktu yang dibutuhkan AI untuk menyelesaikan soal berbeda dari waktu yang diberikan kepada siswa dalam ujian, sehingga perbandingan langsung tidak tepat

  • Komentar ketiga

    • AlphaGeometry menyelesaikan soal yang terbatas, tetapi metode kali ini akan berdampak lebih luas pada matematika
    • Mereka sedang mengimplementasikan pipeline yang mengubah matematika bahasa alami menjadi matematika terformalisasi, dan ini juga dapat mempelajari pembangunan teori dasar
    • Ini adalah cawan suci untuk proof assistant, dan akan membantu manusia memformalisasi matematika dengan lebih alami

  • Komentar keempat

    • Jika sistem membutuhkan 3 hari untuk menyelesaikan soal, ini pada dasarnya tidak berbeda dari brute force sederhana
    • Ini bukan penalaran yang sesungguhnya

  • Komentar kelima

    • Menggunakan Lean
    • Ini penting bukan hanya untuk soal matematika, tetapi juga secara umum untuk menghindari hasil yang tidak bermakna
    • Berharap lebih banyak orang menulis tipe dalam sistem seperti Lean

  • Komentar keenam

    • Iri pada orang-orang yang terlibat dalam proyek ini
    • Memajukan teknologi mutakhir pasti sangat menyenangkan dan memuaskan

  • Komentar ketujuh

    • Diskusi terbaik berlangsung di obrolan Zulip milik LeanProver

  • Komentar kedelapan

    • Peraih Fields Medal Tim Gowers memberikan ringkasan yang baik yang menjelaskan peringatan utama dan memberi konteks

  • Komentar kesembilan

    • Pembuktian teorema adalah permainan satu pemain dengan ruang pencarian yang sangat besar
    • Kontributor terbesar AlphaProof adalah para pengembang Lean dan Mathlib
    • Kurangnya formalisasi dalam makalah matematika telah menghambat upaya otomatisasi

  • Komentar kesepuluh

    • Mesin telah mengungguli manusia dalam catur selama puluhan tahun
    • Namun, orang-orang masih menonton Magnus Carlsen
    • Manusia tertarik pada tindakan manusia lain
    • Mesin hanya menarik sejauh berguna bagi manusia
 
chabulhwi 2024-07-26

  • Komentar ketujuh

    • Diskusi terbaik berlangsung di chat Zulip LeanProver

Diskusi terbaik itu bisa dilihat di sini. https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…