Model Berikutnya dari OpenAI, Astra, Baru Saja Memecahkan Sepuluh Masalah Matematika Terbuka Berusia Puluhan Tahun

Pada 1 Agustus, OpenAI menerbitkan laporan yang mengklaim model berikutnya, yang secara internal disebut Astra, telah menghasilkan temuan baru pada sepuluh masalah terbuka berbeda di bidang matematika. (Bukan, ini bukan masalah Hadiah Milenium, tetapi tetap signifikan.)

Yang patut dicatat: Solusi ini bukan sekadar kemajuan inkremental atas masalah-masalah tersebut; ini adalah penyelesaian yang sesungguhnya, diverifikasi dengan Lean. (Lean adalah bahasa pemrograman dan asisten pembuktian yang memaksa setiap langkah argumen matematis dijabarkan secara rinci agar dapat dibaca mesin.) 

Ini banyak untuk dicerna sekaligus. Dalam artikel ini, saya mengelompokkan masalah-masalahnya berdasarkan bidang dan menjelaskan secara garis besar apa yang terjadi, apa implikasinya bagi matematika sebagai sebuah bidang, serta menelisik apa lagi yang mungkin kita ketahui tentang Astra.

Apa Saja Sepuluh Masalah Itu?

Berikut masing-masing hasilnya, dalam istilah sederhana, beserta bidang matematika atau ilmu komputer spesifiknya.

Grup non-sofic

Bidang: Teori grup

Astra menghasilkan konstruksi eksplisit atas sebuah grup yang tidak dapat diaproksimasi, seberapa pun dekatnya, oleh struktur hingga besar — menutup pertanyaan yang terbuka sejak konsep grup "sofic" diperkenalkan pada 1999. Konstruksi ini disertai bukti bahwa tidak ada urutan aproksimasi hingga yang akan pernah berhasil, diformalkan dalam Lean sehingga logikanya dapat diperiksa secara mekanis.

Wikipedia sudah diperbarui:

Pengemasan bola

Bidang: Geometri berdimensi tinggi

Pertanyaannya adalah sepadat apa bola-bola identik yang tidak saling tumpang tindih dapat dikemas bersama saat jumlah dimensi bertambah. Astra membuktikan batas atas yang lebih ketat atas kerapatan itu di dimensi tinggi, peningkatan pertama atas batas khusus ini sejak 1978. Ini tidak memberikan metode pengemasan yang lebih baik — melainkan mempersempit sebaik apa pun metode di masa depan yang mungkin dicapai.

Kode biner dan sferis

Bidang: Teori pengkodean

Kode koreksi galat bekerja dengan menjaga agar pesan-pesan valid cukup berjauhan sehingga galat kecil tidak dapat mengubah satu pesan menjadi yang lain. Astra membuktikan batas yang jauh lebih ketat (meningkat secara eksponensial) atas berapa banyak pesan semacam itu yang dapat ada untuk jarak minimum tertentu, dengan hasil serupa untuk titik-titik yang tersebar di seluruh bola berdimensi tinggi.

Konjektur kekakuan Connes

Bidang: Aljabar operator

Alain Connes mengonjekturkan bahwa grup-grup tertentu selalu dapat direkonstruksi secara unik dari struktur aljabar, disebut aljabar von Neumann, yang dibangun darinya. Astra membantah ini dengan menghasilkan dua grup yang benar-benar berbeda namun menghasilkan aljabar yang sama, menunjukkan bahwa rekonstruksi tidak selalu bersifat satu-ke-satu.

Kompleksitas rangkaian aritmetika

Bidang: Teori kompleksitas komputasional

"Permanent", sebuah bilangan tunggal yang dihitung dari kisi bilangan, mahal untuk dihitung, dan para ahli kompleksitas ingin mengetahui jumlah langkah aritmetika minimum yang mungkin dibutuhkan metode apa pun. Astra membuktikan batas bawah baru yang lebih kuat atas minimum itu — jenis hasil yang terkenal sulit untuk digeser sama sekali.

Pengulangan paralel kuantum

Bidang: Teori kompleksitas kuantum

Teori klasik menyatakan bahwa membuat dua pemain yang tidak berkomunikasi mengulangi sebuah permainan sulit berkali-kali secara paralel membuat kecurangan menjadi jauh lebih kecil kemungkinannya untuk berhasil. Astra membuktikan jaminan yang sama tetap berlaku bahkan ketika para pemain berbagi keterikatan kuantum, memperluas prinsip klasik yang mendasar ke ranah kuantum.

Masalah vektor terdekat

Bidang: Kriptografi berbasis kisi

Diberikan kisi titik-titik yang berulang (lattice) dan sebuah lokasi target, masalah ini menanyakan titik kisi terdekat — masalah yang diyakini sangat sulit di dimensi tinggi, itulah sebabnya ia menopang sebagian enkripsi tahan kuantum. Astra membuktikan bahwa bahkan mengaproksimasi jawabannya, dalam faktor polinomial tertentu, tetap terbukti sulit, memperkuat kriptografi yang dibangun di atasnya.

Konjektur volume Ehrhart

Bidang: Geometri diskret dan cembung

Untuk suatu bentuk cembung yang satu-satunya titik kisi interiornya tepat berada di titik beratnya, para matematikawan ingin mengetahui volume terbesar yang mungkin dimiliki bentuk semacam itu pada dimensi berapa pun. Astra menghitung volume maksimum itu untuk setiap dimensi, menuntaskan konjektur tersebut secara umum.

Bilangan Ramsey multicolor

Bidang: Teori Ramsey / kombinatorika

Dengan cukup banyak orang dan cukup banyak kategori hubungan di antara mereka, pada akhirnya Anda dijamin menemukan tiga orang yang semuanya terhubung oleh kategori yang sama. Astra membuktikan bahwa ukuran kelompok minimum yang dibutuhkan tumbuh lebih cepat daripada laju eksponensial tetap mana pun seiring bertambahnya jumlah kategori, menyelesaikan masalah Erdős 183.

Konjektur bilangan ekstremal

Bidang: Teori graf ekstremal

Cabang matematika ini menanyakan berapa banyak koneksi yang dapat dimiliki sebuah jaringan sambil tetap menghindari pola kecil tertentu yang dilarang. Astra menuntaskan dua konjektur terkait di sini, yang berkaitan dengan masalah Erdős 146 dan 180, memperjelas sepadat apa jaringan semacam itu dapat menjadi sebelum pola-pola tersebut tak terhindarkan.

Masing-masing ini telah terbuka setidaknya selama satu dekade; beberapa telah bertahan selama tiga puluh tahun atau lebih, termasuk masalah yang dikerjakan oleh para peraih Turing Award di sisi ilmu komputer teoretis dari daftar tersebut.

Tunggu, Apakah Sebuah Kontra-Contoh Itu Jenis Bukti yang "Mudah"?

Siapa saya untuk mengatakan hal negatif di sini, tetapi saya tahu ini adalah pertanyaan atau reaksi umum, terutama dari orang-orang yang cukup mengenal matematika.

Hal yang paling sering dikatakan orang sebagai kritik: Beberapa hasil ini adalah kontra-contoh alih-alih teori umum baru. Gagasan ini penting karena sebuah kontra-contoh menjawab pertanyaan ya/tidak tetapi tidak, dengan sendirinya, memberi tahu Anda mengapa polanya patah atau memberikan keluarga objek serupa untuk dipelajari berikutnya, sedangkan hal lain, seperti teorema klasifikasi atau teknik baru, membuka lebih banyak pintu.

Saya akan mengatakan kritik ini berlaku secara umum, tetapi tidak tepat jika dijadikan penolakan menyeluruh atas seluruh kumpulan masalah ini. Pertama, hasil grup non-sofic bukanlah perubahan kecil pada hampir-solusi yang sudah ada — ini adalah konstruksi pertama dari jenisnya setelah 27 tahun di mana tidak ada seorang pun yang memilikinya sama sekali, dan teknik di baliknya diperkirakan dapat digeneralisasi untuk menemukan yang lain.

Kedua, beberapa dari sembilan hasil lainnya, termasuk batas pengemasan bola dan hasil kesukaran CVP, bukanlah kontra-contoh sama sekali; itu adalah peningkatan langsung atas batas-batas yang ada. 

Apa yang Masih Belum Terselesaikan

Beberapa hal patut dipantau saat ini dibedah oleh komunitas dalam beberapa hari, minggu, dan bulan mendatang:

• Belum ada telaah sejawat. Ini telah diverifikasi dengan Lean dan ditinjau secara informal oleh para matematikawan yang melihat pra-cetak, tetapi belum ada yang melalui proses jurnal bereferensi. 
• Kepengarangan masih dinegosiasikan. OpenAI menyatakan bertanggung jawab atas naskah dan formalisasi Lean, sementara mengatribusikan argumen matematisnya sendiri kepada model. Replikasi independen atas proses (berbeda dengan verifikasi bukti) sulit dilakukan saat ini.

Apa Artinya Ini bagi Matematika

Perubahan paling langsung adalah pada apa yang mungkin benar-benar dikerjakan para matematikawan. Jika sebuah masalah terbuka yang terumuskan baik dapat diserahkan kepada model dan diperiksa dengan Lean, hambatannya bergeser dari "apakah ada yang bisa menyelesaikan ini" menjadi "apakah kita mengajukan pertanyaan yang tepat dan memformalkannya dengan benar." Keahlian merumuskan masalah yang baik dan mengetahui mana yang layak diserang adalah keterampilan nyata yang dikembangkan matematikawan dari pengalaman. 

Ada juga pertanyaan pendanaan dan kredibilitas yang mengemuka. Hibah riset, promosi jabatan, dan penghargaan secara historis dibangun di atas kelangkaan: masalah-masalah ini cukup sulit sehingga menyelesaikan satu menyiratkan sesuatu tentang penyelesainya. Jika hasil yang dibantu AI menjadi rutinitas, bidang ini perlu cara baru untuk memberi sinyal mana yang benar-benar sulit dibandingkan mana yang kini dapat dijangkau dengan beberapa ribu dolar inferensi. Tentu, orang kebanyakan tidak sepenuhnya memahami masalah-masalah ini. Mereka yang memiliki pelatihan sungguhan memahaminya, dan itu tidak berubah. Jadi pengetahuan matematika justru makin berharga. 

Bagaimana Orang Bereaksi

Reaksi di media sosial kurang terbagi soal apakah buktinya valid, dan lebih pada apa yang menjadi buktinya.

Sebagian menganggap kecepatannya sendiri sebagai berita utama: sepuluh masalah berusia puluhan tahun terselesaikan sekaligus, lintas bidang yang tidak terkait, lebih cepat daripada yang bisa ditinjau para ahli. Pertanyaan untuk ke depan: "Akankah kita mampu mengimbangi pemeriksaan semua ini?"

Yang lain berargumen bahwa ini kurang berbicara tentang AI secara umum daripada yang terlihat. Matematika adalah domain langka di mana karya model dapat diperiksa secara otomatis dan menyeluruh. Sebagian besar masalah dunia nyata tidak menawarkan kunci jawaban bawaan dan otomatis seperti itu. Menurut pandangan ini, capaian tersebut nyata, tetapi mungkin lebih banyak mengatakan bahwa matematika luar biasa cocok untuk AI.

Arus komentar ketiga: Sebuah bukti yang benar tetapi belum benar-benar diaudit atau diserap sepenuhnya belum benar-benar dipahami, hanya diverifikasi. Menemukan teorema dan memahami artinya, dalam pandangan ini, adalah dua pekerjaan yang berbeda.

Penutup

Para matematikawan mengatakan hasil grup non-sofic tampak seperti sesuatu yang autentik: pertanyaan terbuka yang sesungguhnya dan telah berlangsung selama puluhan tahun dalam teori grup, ditutup oleh konstruksi eksplisit yang dianggap serius oleh para matematikawan di bidangnya. Sembilan hasil lainnya, jika dipandang bersama, mewakili serangkaian kemajuan yang luas dan secara teknis substansial di ranah matematika murni.

Yang belum terjadi adalah bagian yang lebih lambat: telaah sejawat, replikasi proses pencarian, dan bidang ini benar-benar membangun di atas hasil-hasil tersebut. Bagian itu memakan waktu lebih lama daripada sebuah posting blog, dan di sanalah kita benar-benar akan mengetahui seberapa besar dampaknya. Kami akan terus memberi kabar.