Jadi berita besar minggu ini adalah o3, model bahasa baru OpenAI, mendapat 25% di FrontierMath. Mari kita mulai dengan menjelaskan apa artinya ini.
Apa itu o3? Apa itu FrontierMath?
Model bahasa, seperti yang mungkin diketahui kebanyakan orang, adalah salah satu dari hal-hal seperti ChatGPT di mana Anda dapat mengajukan pertanyaan dan model tersebut akan menulis beberapa kalimat yang merupakan upaya untuk memberi Anda jawaban. Ada model bahasa sebelum ChatGPT, dan secara keseluruhan mereka bahkan tidak bisa menulis kalimat dan paragraf yang koheren. ChatGPT benar-benar model publik pertama yang koheren. Ada banyak model lain sejak itu. Saat ini mereka masih membaik dengan sangat cepat. Tidak ada yang tahu berapa lama lagi hal ini akan berlangsung, namun ada banyak orang yang mengeluarkan banyak uang untuk permainan ini, jadi sangatlah bodoh jika bertaruh bahwa kemajuan akan melambat dalam waktu dekat. o3 adalah model bahasa baru.
FrontierMath adalah kumpulan data rahasia dari “ratusan” soal matematika sulit, yang dikurasi oleh Epoch AI, dan diumumkan bulan lalu. “Ratusan” adalah kutipan dari kertas itu (baris pertama abstrak), tetapi saya pernah mendengar rumor bahwa ketika makalah tersebut diterbitkan, terdapat kurang dari 200 pertanyaan, meskipun saya telah mendengar rumor lain yang tampaknya lebih banyak lagi yang ditambahkan sejak saat itu. Sebagai seorang matematikawan akademis yang menghabiskan seluruh hidupnya berkolaborasi secara terbuka dalam masalah penelitian dan berbagi ide dengan orang lain, saya sedikit frustrasi karena di paragraf ini kita telah melihat lebih banyak pertanyaan daripada jawaban – saya bahkan tidak ingin memberi Anda penjelasan yang koheren. deskripsi beberapa fakta dasar tentang kumpulan data ini, misalnya ukurannya. Namun ada alasan bagus untuk kerahasiaan tersebut. Model bahasa dilatih pada database pengetahuan yang besar, jadi saat Anda membuat database soal matematika menjadi publik, model bahasa akan melatihnya. Dan kemudian jika Anda mengajukan pertanyaan kepada model seperti itu dari database, mereka mungkin akan memberikan jawaban yang sudah mereka lihat.
Seberapa sulit kumpulan data FrontierMath?
Jadi seperti apa pertanyaan di dataset FrontierMath? Inilah yang kami ketahui. Mereka tidak “buktikan teorema ini!” pertanyaan, mereka adalah “temukan nomor ini!” pertanyaan. Lebih tepatnya, makalah tersebut mengatakan “Masalah harus memiliki jawaban yang pasti dan dapat dihitung yang dapat diverifikasi secara otomatis”, dan dalam lima contoh masalah yang dipublikasikan dari kumpulan data (Lampiran A makalah, halaman 14 hingga 23) solusinya adalah semua bilangan bulat positif (satu jawaban adalah 9811, jawaban lainnya adalah 367707, dan tiga solusi terakhir bahkan lebih besar lagi — jelas pertanyaan-pertanyaan ini dirancang sedemikian rupa sehingga sangat kecil kemungkinannya untuk berhasil menebak secara acak). Contoh pertanyaannya tidak sepele, bahkan bagi ahli matematika riset. Saya memahami pernyataan kelima pertanyaan. Saya dapat melakukan yang ketiga dengan relatif cepat (saya telah melihat triknya sebelumnya bahwa fungsi yang memetakan n alami ke alfa^n adalah p-adically kontinu di n jika penilaian p-adic alpha-1 positif) dan saya tahu persis bagaimana mengerjakan yang ke-5 (ini adalah trik standar yang melibatkan dugaan Weil untuk kurva) tetapi saya tidak repot-repot mengerjakan aljabar untuk menemukan jawaban 13 digit yang tepat. Pertanyaan pertama dan kedua yang saya tahu tidak bisa saya lakukan, dan saya pikir saya mungkin bisa membuat kemajuan pada pertanyaan ke-4 jika saya berusaha sungguh-sungguh, tetapi pada akhirnya saya tidak mencobanya, saya hanya membaca solusinya. Saya menduga bahwa seorang sarjana matematika yang cerdas akan kesulitan untuk mengerjakan salah satu dari pertanyaan-pertanyaan ini. Untuk melakukan hal pertama, saya kira, Anda harus setidaknya menjadi mahasiswa PhD dalam teori bilangan analitik. Makalah FrontierMath berisi beberapa kutipan dari para ahli matematika tentang tingkat kesulitan soal. Tao (Fields Medal) mengatakan “Ini sangat menantang” dan menyarankan bahwa pertanyaan tersebut hanya dapat ditangani oleh seorang ahli domain (dan memang dua contoh pertanyaan yang dapat saya selesaikan adalah dalam bidang aritmatika, bidang keahlian saya; saya gagal melakukan semuanya) yang di luar daerah saya). Namun Borcherds (juga Fields Medal) dikutip di koran tersebut mengatakan bahwa mesin yang menghasilkan jawaban numerik “tidak sama dengan menghasilkan bukti asli”.
Jadi mengapa membuat kumpulan data seperti itu? Masalahnya adalah menilai solusi terhadap “ratusan” jawaban untuk “buktikan teorema ini!” pertanyaan itu mahal (seseorang tidak akan mempercayai mesin untuk melakukan penilaian pada tingkat ini, setidaknya pada tahun 2024, jadi seseorang harus membayar manusia yang ahli), sedangkan memeriksa apakah ratusan angka dalam satu daftar sesuai dengan ratusan angka di daftar lain dapat dilakukan dalam sepersekian detik oleh komputer. Seperti yang dikatakan Borcherds, peneliti matematika menghabiskan sebagian besar waktunya untuk mencoba menghasilkan bukti atau ide, dibandingkan angka, namun kumpulan data FrontierMath masih sangat berharga karena bidang AI untuk matematika sangat kekurangan kumpulan data yang sulit, dan menciptakan sebuah kumpulan data seperti ini membutuhkan kerja keras (atau setara dengan sangat mahal).
Jadi ada artikel tentang dataset di Sains dan saya dikutip di dalamnya mengatakan, “Jika Anda memiliki sistem yang dapat menguasai database tersebut, maka permainan berakhir bagi para ahli matematika.” Untuk memperjelas: Saya tidak ada hubungannya dengan kumpulan data tersebut, saya hanya melihat lima pertanyaan publik, dan mendasarkan komentar saya pada pertanyaan tersebut. Saya juga berkata, “Menurut pendapat saya, saat ini AI masih jauh dari kemampuan untuk menjawab pertanyaan-pertanyaan itu… tapi saya pernah salah sebelumnya”. Dan minggu ini ada pengumuman bahwa model bahasa o3 mendapat skor 25 persen pada kumpulan data. Saya terkejut.
Apa sebenarnya yang terjadi di sini?
Mengapa saya terkejut? Karena model mental saya tentang “AI” saat ini, ketika mengerjakan matematika, adalah “sarjana atau pra-sarjana”. Ia menjadi sangat baik dalam soal-soal “gaya Olimpiade” yang diberikan kepada siswa sekolah menengah yang cerdas. Dalam satu tahun, sudah jelas bahwa sistem AI akan lulus ujian matematika tingkat sarjana (terutama karena saat Anda menetapkan ujian matematika tingkat sarjana, idealnya Anda perlu memastikan bahwa Anda tidak gagal dalam 50 persen kelas, sehingga Anda lulus. beberapa pertanyaan standar yang sangat mirip dengan pertanyaan yang telah dilihat siswa, untuk memastikan bahwa mereka yang memiliki pemahaman dasar tentang kursus akan lulus ujian. Mesin akan dengan mudah dapat menyelesaikan pertanyaan tersebut). Namun tampaknya ada lompatan dari ide-ide inovatif pada tingkat sarjana/PhD awal yang melebihi ide-ide standar daur ulang kepada saya menjadi cukup besar. Misalnya saya sangat tidak terkesan dengan jawaban ChatGPT terhadap ujian Putnam yang baru-baru ini diposting Di Sini — sejauh yang saya bisa lihat hanya pertanyaan B4 yang dijawab dengan baik oleh mesin, sebagian besar jawaban lainnya bernilai paling banyak satu atau dua dari 10. Jadi saya berharap kumpulan data ini tetap tidak dapat diserang selama beberapa tahun.
Namun kegembiraan awal saya diredam oleh postingan dari Elliot Glazer dari Epoch AI di reddit dimana dia mengklaim bahwa sebenarnya 25 persen permasalahan dalam dataset adalah “masalah gaya IMO/undergrad”. Klaim ini sedikit membingungkan karena saya akan kesulitan menerapkan kata sifat tersebut pada salah satu dari lima masalah yang dipublikasikan secara publik dalam kumpulan data; bahkan yang paling sederhana pun menggunakan dugaan Weil untuk kurva (atau argumen brute force yang mungkin hampir mungkin tetapi akan sangat menyakitkan, karena melibatkan pemfaktoran polinomial 10^12 derajat 3 pada bidang berhingga, meskipun hal ini tentu saja dapat diparalelkan) . Hal ini tentu saja menimbulkan pertanyaan di benak saya tentang seberapa sebenarnya tingkat permasalahan dalam kumpulan data rahasia ini (atau apakah kelima pertanyaan publik tersebut benar-benar merupakan sampel yang representatif), namun ini bukanlah pengetahuan yang kemungkinan besar dapat kita akses. . Mengingat informasi baru bahwa 25 persen permasalahan terjadi pada tingkat sarjana, mungkin saya akan kembali bersikap tidak terkejut lagi, namun akan terkejut ketika AI semakin mendekati 50 persen pada kumpulan data, karena kinerjanya berada pada “tingkat yang setara” (seperti yang dijelaskan oleh Elliot — 50 persen pertanyaan berikutnya) adalah hal yang saya tunggu dari sistem ini — bagi saya ini akan mewakili sebuah terobosan besar.
Buktikan teorema ini!
Namun, seperti yang ditunjukkan Borcherds, meskipun kita memiliki mesin manusia super yang dapat “menemukan nomor ini!” pertanyaan, penerapannya masih terbatas di banyak bidang penelitian matematika, di mana pertanyaan kunci yang menarik biasanya adalah bagaimana “membuktikan teorema ini!”. Menurut saya, kisah sukses terbesar di tahun 2024 adalah DeepMind Bukti Alfayang menyelesaikan empat dari enam soal IMO (International Mathematics Olympiad) 2024. Ini bisa berupa “buktikan teorema ini!” atau pertanyaan “temukan nomor dan buktikan lebih lanjut bahwa itu adalah nomor yang benar” dan untuk tiga pertanyaan di antaranya, keluaran mesin adalah bukti Lean yang diformalkan sepenuhnya. Bersandar adalah pembukti teorema interaktif dengan perpustakaan matematika yang solid matematikalib berisi banyak teknik yang diperlukan untuk menyelesaikan masalah IMO dan masih banyak lagi; Solusi sistem DeepMind telah diperiksa oleh manusia dan diverifikasi sebagai solusi “nilai penuh”. Namun, kami kembali ke tingkat sekolah menengah atas; Meskipun soal-soalnya sangat sulit, penyelesaiannya hanya menggunakan teknik tingkat sekolah. Pada tahun 2025 saya yakin kita akan melihat mesin berkinerja pada standar tingkat emas di IMO. Namun hal ini sekarang memaksa kita untuk membuka kaleng “penilaian” worm yang telah saya sebutkan satu kali, dan saya akan menyelesaikan postingan ini dengan membicarakannya lebih banyak lagi.
Siapa yang menandai mesin?
Juli 2025. Saya dapat membayangkan situasi berikut. Selain ratusan anak sekolah terpintar di dunia yang masuk IMO, akan ada mesin yang masuk. Meski begitu, semoga saja tidak terlalu banyak. Karena sistemnya akan ada dua jenis. Akan ada sistem yang mengirimkan jawaban dalam bahasa pemeriksa bukti komputer seperti Lean (atau Rocq, Isabelle, atau banyak lainnya). Dan akan ada model bahasa yang mengirimkan jawaban dalam bahasa manusia. Perbedaan besar antara kedua pengajuan ini adalah: jika penanda memverifikasi bahwa penyataan Jika pertanyaan telah diterjemahkan dengan benar ke dalam pemeriksa bukti komputer, maka yang perlu mereka lakukan hanyalah memeriksa apakah bukti tersebut telah dikompilasi dan pada dasarnya mereka mengetahui bahwa ini adalah solusi “nilai penuh”. Untuk model bahasa kita akan menghadapi situasi seperti solusi Putnam yang buruk di atas – komputer akan menulis sesuatu, akan terlihat meyakinkan, namun manusia harus membacanya dengan cermat dan menilainya, dan tentu saja tidak ada jaminan bahwa itu akan berhasil. akan menjadi solusi “nilai penuh”. Borcherds benar dalam mengingatkan komunitas AI bahwa “buktikan teorema ini!” adalah hal yang benar-benar ingin kita lihat sebagai ahli matematika, dan model bahasa saat ini setidaknya kurang akurat dibandingkan manusia ahli dalam hal penalaran logis. Saya takut akan serangan gencar yang tak terhindarkan dalam satu atau dua tahun dari “bukti” model bahasa hipotesis Riemann yang hanya akan berisi klaim yang tidak jelas atau tidak akurat di tengah 10 halaman matematika yang benar yang harus dilalui manusia untuk menemukannya. garis yang tidak tahan. Di sisi lain, pembuktian teorema setidaknya memiliki urutan besarnya lebih akurat: setiap kali saya melihat Lean tidak menerima argumen manusia dalam literatur matematika, manusia telah salah.
Faktanya, sebagai ahli matematika, kami ingin melihat lebih dari sekedar “buktikan teorema ini!”. Kami ingin melihat “membuktikan teorema ini dengan benar, dan menjelaskan apa yang membuat pembuktian tersebut bekerja dengan cara yang dapat dipahami oleh kita sebagai manusia”. Dengan pendekatan model bahasa saya khawatir (banyak) tentang “benar” dan dengan pendekatan pembuktian teorema saya khawatir tentang “dengan cara yang kita sebagai manusia pahami”. Masih banyak hal yang harus dilakukan. Kemajuan saat ini terjadi dengan sangat cepat. Tapi kita masih jauh. Kapan kita akan “mengatasi hambatan sarjana”? Tidak ada yang tahu.
