OpenAI Klaim Model AI Rahasia Pecahkan Ratusan Soal Matematika Rumit

OpenAI baru saja memublikasikan 722 naskah matematika melalui platform GitHub pada hari Selasa lalu. Seluruh naskah tersebut dihasilkan oleh model kecerdasan buatan internal yang hingga saat ini belum dirilis ke publik.

Seorang perwakilan OpenAI menyatakan bahwa hampir seluruh hasil kerja tersebut berasal dari satu perintah atau prompt tunggal kepada satu agen AI. Meski demikian, perusahaan mengakui bahwa beberapa soal mungkin memerlukan percobaan lebih dari sekali untuk diselesaikan.

Klaim ini muncul sebagai terobosan signifikan dalam bidang matematika yang sangat kompleks. Namun, tidak semua akademisi memberikan respons positif atau merasa yakin dengan pengumuman tersebut.

Matematikawan dari Massachusetts Institute of Technology, Andrew Sutherland, meminta bukti nyata atas klaim tersebut. Menurutnya, klaim mengenai penyelesaian soal matematika dalam sekali percobaan oleh satu agen AI harus dianggap belum terverifikasi sebelum modelnya dirilis agar bisa diuji oleh pihak luar.

Naskah yang dirilis terbagi dalam 372 kelompok hasil terkait. Satu kelompok dapat berisi teorema utama beserta argumen pendukung, konsekuensi dari teorema tersebut, atau pembuktian alternatif.

Jumlah 722 merujuk pada total naskah yang diterbitkan, bukan jumlah masalah matematika yang berhasil dipecahkan. Pihak OpenAI menyebutkan telah memberikan sekitar 4.000 soal kepada model mereka dan hanya memublikasikan hasil yang dinilai cukup signifikan.

Berdasarkan catatan OpenAI, rata-rata hasil pengerjaan memerlukan daya komputasi setara dengan tiga jam pemrosesan ChatGPT Pro. Hal ini berbeda jauh dengan klaim penyelesaian Navier-Stokes bulan lalu yang melibatkan 10.000 agen selama 88 jam.

OpenAI telah menyediakan ringkasan penalaran untuk 10 hasil penelitian tersebut. Namun, hanya 162 dari 722 naskah yang menyertakan hasil utama yang telah diverifikasi oleh sistem komputer bernama Lean.

Lean adalah perangkat lunak yang berfungsi memeriksa setiap langkah logika secara mekanis. Hanya sekitar 22 persen dari total koleksi naskah yang telah melalui proses formalisasi tersebut.

Pihak OpenAI sendiri mengakui bahwa tidak semua naskah memiliki formalisasi Lean. Mereka secara terbuka menyatakan bahwa beberapa hasil yang belum diformalisasi kemungkinan memiliki kesalahan logika.

Pemeriksaan melalui Lean hanya mengonfirmasi bahwa pembuktian mengikuti pernyataan seperti yang tertulis dalam perangkat lunak tersebut. Hal ini tidak menjamin bahwa pernyataan tersebut sesuai dengan masalah aslinya atau bahwa hasilnya merupakan temuan baru yang penting.

Di sinilah banyak peneliti mulai meragukan kredibilitas pengumuman ini. The Institute for Advanced Study di Princeton, New Jersey, memberikan pernyataan resmi mengenai kekhawatiran mereka terhadap perkembangan ini.

Lembaga tersebut menekankan bahwa saat ini AI mampu mengeluarkan argumen matematika tanpa dipahami, diverifikasi, atau dipertanggungjawabkan oleh manusia yang memberikan perintah. Mereka meyakini pemahaman manusia tetap menjadi aspek paling utama dalam ilmu pengetahuan.

Di sisi lain, Profesor Abhishek Saha merasa antusias dengan perkembangan ini. Ia menyebut hari ini sebagai momen besar bagi dunia matematika, meskipun ia mencatat bahwa sebagian besar masalah yang diselesaikan masuk dalam kategori kemajuan luar biasa dalam program yang sudah ada.

Sebagian besar masalah dalam koleksi ini menarik, namun bukan terobosan yang mengubah tatanan dunia seperti Millennium Problems. Pengecualian hanya berlaku untuk satu masalah, yaitu Quasi-Riemann Hypothesis.

Rilis ini dianggap belum memenuhi rekomendasi kelompok penasihat dari Institute for Advanced Study pada 29 September lalu. Rekomendasi tersebut mencakup nama model, prompt yang digunakan, ringkasan alur berpikir, durasi waktu, serta biaya komputasi untuk setiap hasil.

OpenAI hanya memublikasikan angka rata-rata komputasi dan 10 ringkasan penalaran tanpa menyertakan perintah spesifik. Mereka beralasan bahwa saat ini perusahaan masih berupaya merilis model tersebut secara bertanggung jawab.

Daniel Litt, matematikawan dari University of Toronto, memiliki pandangan berbeda. Ia berpendapat tidak ada alasan bagi perusahaan untuk merahasiakan jawaban dari soal-soal matematika tersebut dari masyarakat luas.

Sebagai perbandingan, perusahaan Anthropic menempuh jalur berbeda bulan lalu saat merilis bukti Fermat's Last Theorem yang sudah diverifikasi oleh Lean. Mereka memublikasikan seluruh 13 juta baris pembuktian secara terbuka di GitHub untuk diakses publik.