Bagaimana AI dan SAT Memecahkan Masalah Matematika Terberat Dunia

Marijn Heule adalah seorang peneliti yang menggunakan alat khusus bernama satisfiability (SAT) untuk memecahkan masalah matematika yang sudah lama dianggap tidak dapat dipecahkan. Masalah-masalah ini berhubungan dengan bidang geometri dan kombinatorika yang sulit dan sudah bertahan selama puluhan tahun tanpa solusi. SAT sendiri adalah teknologi AI simbolik yang sederhana namun kuat karena memecah masalah menjadi pernyataan yang hanya bisa bernilai benar atau salah. Keunggulan SAT adalah kemampuannya dalam menguji apakah ada cara untuk mengisi nilai-nilai benar atau salah dalam sebuah formula logika agar memenuhi semua aturan yang berlaku. Dalam hal ini, alat SAT berperan seperti menyelesaikan teka-teki besar yang sangat kompleks, bukan menjalankan perhitungan biasa. Marijn Heule memiliki keahlian dalam membuat representasi masalah yang tepat agar SAT bisa bekerja sangat efektif dalam menguji bukti matematika. Belakangan ini, Heule melihat potensi besar jika SAT digabungkan dengan model bahasa besar (LLM) seperti AI yang bisa memahami dan menghasilkan bahasa manusia. LLM dapat membantu membuat terjemahan otomatis masalah yang kompleks ke dalam format SAT secara lebih baik. Ketika LLM memberikan solusi yang kurang tepat, SAT dapat mengevaluasi ulang dengan memberikan contoh kesalahan sehingga LLM dapat belajar dan memperbaiki solusinya. Kolaborasi antara manusia, LLM, dan SAT dapat menghasilkan pembuktian matematika yang kuat dan dapat dipercaya bila dikombinasikan dengan sistem formal proof checker seperti Lean, yang memastikan semua bagian pembuktian memang benar-benar lengkap dan konsisten. Dengan begitu, kombinasi ini dapat mempercepat penyelesaian masalah matematika besar tanpa menggantikan peran manusia sepenuhnya. Meskipun ada kritik terhadap bukti yang terlalu bergantung pada komputer karena kurangnya pemahaman manusia secara langsung, Heule menekankan bahwa kepercayaan dan validitas pembuktian otomatis adalah hal yang lebih penting daripada pemahaman intuitif. AI akan menjadi mitra penting matematika masa depan yang membantu manusia menyelesaikan teka-teki paling sulit lewat kerja sama antara kreativitas manusia dan kekuatan komputasi.