AI dari China ini Hanya Butuh 80 jam Pecahkan Soal Matematika yang Bertahan 12 Tahun

Terobosan baru dalam dunia kecerdasan buatan (AI) kembali mencuri perhatian. Sebuah sistem AI yang dikembangkan tim peneliti dari Peking University berhasil memecahkan persoalan matematika yang telah bertahan selama 12 tahun hanya dalam waktu 80 jam, dengan intervensi manusia yang nyaris tidak ada.

Dikutip dari TechRadar, masalah tersebut merupakan sebuah dugaan (conjecture) dalam bidang aljabar komutatif yang pertama kali diajukan oleh Dan Anderson pada 2014. 

Selain menemukan solusi, sistem AI ini juga mampu memverifikasi pembuktiannya secara mandiri, sebuah capaian yang selama ini menjadi tantangan besar dalam penelitian matematika.

Dalam makalah prapublikasi yang diunggah di arXiv, tim peneliti menyebut keberhasilan ini sebagai contoh nyata otomasi riset matematika. 

“Dengan kerangka ini, kami berhasil menyelesaikan masalah terbuka dalam aljabar komutatif dan secara otomatis memformalkan pembuktiannya dengan hampir tanpa campur tangan manusia,” tulis mereka.

Keberhasilan ini ditopang oleh sistem AI berbasis dua agen yang bekerja secara terintegrasi. Agen pertama, Rethlas, berfungsi sebagai mesin penalaran yang mengeksplorasi berbagai strategi solusi dengan bantuan basis data teorema matematika.

Setelah menemukan kemungkinan pembuktian, agen kedua, Archon, mengambil alih untuk mengubah hasil tersebut menjadi format formal yang bisa diuji oleh sistem pembuktian matematika berbasis mesin.

Proses verifikasi dilakukan menggunakan Lean 4, sebuah bahasa pemrograman sekaligus alat pembuktian teorema interaktif yang memiliki pustaka ratusan ribu definisi dan teorema matematika.

Menariknya, selama proses berlangsung, peneliti menyebut tidak ada penilaian matematis yang harus dilakukan oleh manusia. Sistem bekerja secara otonom, mulai dari eksplorasi ide hingga validasi hasil.

Tim peneliti mencatat, sistem ini mampu menyelesaikan tugas matematika dengan kecepatan yang melampaui kemampuan manusia, bahkan untuk pekerjaan yang biasanya membutuhkan kolaborasi lintas disiplin.

Meski demikian, mereka mengakui intervensi seorang matematikawan tetap dapat mempercepat proses, khususnya dalam mengarahkan tahap verifikasi.

Lebih jauh, sistem ini dinilai mampu menjembatani kesenjangan antara penalaran matematis berbasis bahasa alami dan verifikasi formal berbasis mesin—dua hal yang selama ini sering berjalan terpisah dalam riset matematika.

“Penelitian ini menunjukkan paradigma baru, di mana sistem penalaran informal dan formal dapat bekerja bersama untuk menghasilkan hasil yang terverifikasi,” tulis tim peneliti.

Meski menjanjikan, temuan ini masih berstatus prapublikasi dan belum melalui proses peer review. Artinya, validasi independen dari komunitas ilmiah masih diperlukan untuk memastikan keakuratannya.

Selain itu, masalah yang berhasil dipecahkan tergolong relatif spesifik dan belum sebanding dengan tantangan matematika besar seperti Hipotesis Riemann atau persoalan P vs NP.

Namun demikian, bagi bidang yang selama berabad-abad sulit diotomatisasi, capaian ini menjadi tonggak penting.