OpenAI Klaim Model AI Rahasia Pecahkan Ratusan Soal Matematika Rumit

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.