Pandangan Matematikawan tentang Kemampuan Matematika AI

• Model bahasa baru OpenAI, o3, mencetak 25% pada benchmark matematika sulit FrontierMath, kembali menggoyahkan penilaian tentang apakah AI matematika bisa melampaui level sarjana
• FrontierMath adalah dataset tertutup yang dibuat Epoch AI, berisi ratusan soal matematika sulit yang menuntut jawaban numerik yang dapat diverifikasi otomatis, bukan “membuktikan teorema”
• Lima sampel yang dipublikasikan tidak mudah bahkan bagi matematikawan riset, dan Tao menilainya “sangat menantang”, tetapi Borcherds berpendapat menghasilkan jawaban numerik tidak sama dengan pembuktian orisinal
• Karena Elliot Glazer dari Epoch AI menyatakan bahwa 25% soal adalah “soal bergaya IMO/sarjana”, sulit memastikan sejauh mana skor 25% o3 benar-benar menunjukkan tingkat kesulitan yang dicapai, mengingat sifat dataset yang tertutup
• Bagi matematikawan, tujuan yang lebih penting daripada “temukan angka ini” adalah membuktikan teorema dengan benar dan menjelaskannya agar dapat dipahami manusia, sementara model bahasa dan pendekatan berbasis Lean memiliki keterbatasan yang berbeda

---

o3 dan FrontierMath Menggoyahkan Garis Dasar

• o3 adalah model bahasa baru OpenAI, dan mencatat skor 25% pada FrontierMath
• Sejak ChatGPT, model bahasa publik berkembang cepat, dan kemampuan menyelesaikan soal matematika juga dinilai dalam arus perkembangan tersebut
• FrontierMath adalah dataset soal matematika tertutup yang dibuat Epoch AI; abstrak makalahnya menyebut ada “ratusan” soal matematika sulit
• Jika dataset dibuka, model bahasa dapat mempelajari soal dan jawabannya, sehingga bahkan informasi dasar seperti jumlah soal pun diperlakukan dengan hati-hati
  • Jika soal dan jawaban dipublikasikan, model dapat mereproduksi jawaban yang sudah pernah dilihat
  • Karena itu, sulit bagi pihak luar untuk memverifikasi tingkat kesulitan nyata dan keterwakilan benchmark tertutup

Format dan Tingkat Kesulitan Soal FrontierMath

• Soal FrontierMath lebih dekat ke format “temukan angka ini”, bukan “buktikan teorema ini”
• Soal harus memiliki jawaban yang jelas dan dapat dihitung, serta dapat diverifikasi secara otomatis
• Jawaban dari lima contoh soal yang dipublikasikan semuanya bilangan bulat positif
  • Contoh jawaban mencakup 9811 dan 367707
  • Tiga jawaban lainnya lebih besar, dirancang agar sulit ditebak secara acak
• Sampel yang dipublikasikan tidak trivial bahkan bagi matematikawan riset
  • Penulis memahami pernyataan kelima soal tersebut
  • Soal ketiga dapat diselesaikan relatif cepat, dan untuk soal kelima penulis tahu cara menyelesaikannya dengan teknik standar menggunakan Weil conjectures for curves, tetapi tidak menghitung jawaban 13 digitnya
  • Penulis menilai soal pertama dan kedua tidak dapat ia selesaikan, dan untuk soal keempat ia merasa mungkin ada kemajuan jika berusaha, tetapi memilih membaca pembahasannya tanpa mencoba
• Mahasiswa matematika sarjana yang cerdas pada umumnya mungkin akan kesulitan menyelesaikan satu pun dari soal-soal ini
  • Soal pertama dinilai kemungkinan membutuhkan level doktoral atau lebih tinggi dalam teori bilangan analitik

Kelebihan dan Keterbatasan Benchmark Jawaban Numerik

• Alasan utama FrontierMath menggunakan soal dengan jawaban numerik adalah biaya penilaian
• Untuk mengevaluasi ratusan jawaban tipe “buktikan teorema”, diperlukan pakar manusia
  • Per 2024, penilaian pada level ini dianggap sulit diserahkan kepada mesin
• Sebaliknya, daftar jawaban numerik dapat dibandingkan komputer dengan sangat cepat
• Borcherds berpendapat matematikawan riset menghabiskan sebagian besar waktunya untuk mencari pembuktian dan ide, bukan angka
• Meski begitu, FrontierMath bernilai dalam bidang AI matematika
  • Dataset yang sulit sangat langka
  • Membuat dataset semacam ini sangat sulit atau mahal
  • Tulisan terbaru oleh Frieder dan lainnya membahas lebih dalam keterbatasan dataset AI matematika

Mengapa Skor 25% o3 Mengejutkan

• Dalam persepsi sebelumnya, AI matematika berada dekat level sarjana atau pra-sarjana
• AI menjadi sangat kuat pada soal bergaya olimpiade yang diselesaikan siswa SMA berbakat
• Dipandang jelas bahwa dalam setahun AI akan lulus ujian matematika sarjana
  • Ujian sarjana kadang berisi soal standar agar mahasiswa yang secara dasar memahami kuliah dapat lulus
  • Mesin dapat menjawab soal seperti ini dengan mudah
• Namun lompatan dari sekadar memakai ulang ide standar menuju ide inovatif level sarjana lanjut atau awal doktoral dianggap besar
• Jawaban ChatGPT baru-baru ini untuk ujian Putnam berada di bawah ekspektasi
  • Tampaknya hanya B4 yang dijawab mesin dengan layak
  • Sebagian besar jawaban lain dinilai berada di level 1–2 poin dari 10
• Karena alasan ini, FrontierMath diperkirakan hampir tidak akan bisa ditembus selama beberapa tahun

Ketidakpastian yang Ditinggalkan Dataset Tertutup

• Elliot Glazer dari Epoch AI menyatakan di Reddit bahwa 25% soal FrontierMath adalah soal bergaya IMO/sarjana
• Pernyataan ini tampak kurang cocok dengan lima soal yang dipublikasikan
  • Bahkan soal termudah dalam sampel publik memiliki pendekatan yang menggunakan Weil conjectures for curves
  • Atau bisa saja membutuhkan metode brute force yang menyakitkan: memfaktorkan polinomial kubik berderajat 10^12 di atas medan hingga
• Informasi ini menyisakan pertanyaan tentang tingkat kesulitan dataset tertutup yang sebenarnya dan apakah lima soal publik merupakan sampel yang representatif
• Karena dataset tertutup, pertanyaan ini sulit diverifikasi
• Jika 25% memang soal level sarjana, skor 25% o3 mungkin tidak terlalu mengejutkan
• Terobosan besar yang diharapkan adalah saat AI menunjukkan performa bermakna pada 50% soal berikutnya yang digambarkan sebagai “qual level”

“Buktikan Teorema” Masih Merupakan Masalah Berbeda

• Dalam riset matematika, pertanyaan penting biasanya adalah “buktikan teorema ini”
• Bahkan jika muncul mesin dengan performa supermanusia pada soal pencarian angka, penerapannya di banyak area riset matematika bisa tetap terbatas
• Salah satu keberhasilan terbesar pada 2024 adalah AlphaProof dari DeepMind
  • AlphaProof menyelesaikan 4 dari 6 soal IMO 2024
  • Soal-soalnya bertipe “buktikan teorema” atau “temukan angka dan buktikan bahwa angka itu benar”
  • Tiga di antaranya dihasilkan sebagai pembuktian Lean yang sepenuhnya diformalkan
• Lean adalah pembukti teorema interaktif, dan mathlib adalah pustaka matematika yang mencakup banyak teknik yang diperlukan untuk menyelesaikan soal IMO dan lebih dari itu
• Jawaban sistem DeepMind diperiksa manusia dan diverifikasi sebagai jawaban “nilai penuh”
• Namun, sekalipun soal IMO sangat sulit, solusinya hanya memakai teknik level sekolah, sehingga pada dasarnya kembali lagi ke soal level SMA
• Pada 2025, diperkirakan mesin akan menunjukkan performa setingkat medali emas IMO

Siapa yang Akan Menilai Jawaban Mesin?

• Kita dapat membayangkan situasi pada IMO Juli 2025 di mana bukan hanya siswa manusia, tetapi juga mesin ikut berpartisipasi
• Sistem mesin dapat terbagi menjadi dua jenis
  • Sistem yang menyerahkan jawaban dalam bahasa pemeriksa pembuktian komputer seperti Lean, Rocq, atau Isabelle
  • Model bahasa yang menyerahkan jawaban dalam bahasa manusia
• Untuk jawaban yang diserahkan dalam bahasa pemeriksa pembuktian, yang perlu dipastikan hanyalah apakah pernyataan soal diterjemahkan dengan benar
  • Setelah pembuktiannya berhasil dikompilasi, pada praktiknya kita tahu itu adalah jawaban “nilai penuh”
• Model bahasa yang menyerahkan jawaban bahasa alami berbeda
  • Walaupun jawabannya tampak meyakinkan, juri manusia harus membacanya dengan saksama dan menilainya
  • Tidak ada jaminan bahwa itu jawaban bernilai penuh
• Model bahasa dianggap setidaknya satu orde magnitudo kurang akurat dibanding pakar manusia dalam penalaran logis
• Ada kekhawatiran bahwa “pembuktian” model bahasa untuk hipotesis Riemann dapat mencampurkan pernyataan yang ambigu atau tidak akurat di tengah 10 halaman matematika yang benar
• Sebaliknya, pembukti teorema dianggap setidaknya satu orde magnitudo lebih akurat
  • Ketika Lean tidak menerima argumen dalam literatur matematika manusia, dalam kasus yang pernah dilihat penulis, pihak manusialah yang keliru

Tujuan yang Tersisa: Pembuktian Benar dan Pemahaman Manusia

• Yang diinginkan matematikawan bukan sekadar “buktikan teorema”, melainkan pembuktian yang benar dan penjelasan yang dapat dipahami manusia
• Dalam pendekatan model bahasa, “akurasi” tetap menjadi kekhawatiran besar
• Dalam pendekatan pembukti teorema, kekhawatirannya adalah “cara yang dapat dipahami manusia”
• Masih sangat banyak pekerjaan yang harus dilakukan
• Laju kemajuan memang cepat, tetapi tidak ada yang tahu kapan hambatan level sarjana akan terlampaui