Artificial Intelligence dan Machine Learning Mengubah Cara Manusia Berinteraksi dengan Mesin
Artificial Intelligence (AI) dan Machine Learning (ML) adalah bidang yang sedang tren saat ini. Kemajuan yang pesat dalam AI telah mengubah cara manusia berinteraksi dengan mesin. Salah satu aspek penting dalam kecerdasan manusia adalah penalaran. Beberapa pendekatan pembuktian teorema telah diteliti, seperti Automated theorem proving (ATP), yang merupakan proses menghasilkan bukti secara otomatis untuk teorema yang dinyatakan dalam logika formal. Namun, ATP memiliki tantangan karena ruang pencarian yang besar. Oleh karena itu, muncul paradigma baru yang disebut Interactive theorem proving (ITP), di mana ahli manusia berinteraksi dengan alat perangkat lunak yang disebut proof assistants untuk membangun bukti.
LeanDojo: Solusi Open-source untuk Theorem Proving Berbasis LLM
Dalam bidang theorem proving, Large language models (LLMs) telah menunjukkan kemampuan yang luar biasa dalam menghasilkan kode. Namun, LLMs menghadapi kesulitan dalam theorem proving karena kekurangan dalam faktualitas dan halusinasi. Untuk mengatasi keterbatasan ini, tim peneliti dari Caltech, NVIDIA, MIT, UC Santa Barbara, dan UT Austin memperkenalkan LeanDojo. LeanDojo adalah toolkit open-source untuk theorem proving berbasis LLM yang dibangun di sekitar proof assistant bernama Lean, yang populer di kalangan matematikawan.
LeanDojo memiliki kemampuan ekstraksi data yang memungkinkan model berkomunikasi dengan Lean secara programatik. Hal ini memungkinkan mereka melihat keadaan bukti, melakukan tindakan atau taktik bukti, dan mendapatkan umpan balik dari Lean. Selain itu, LeanDojo juga memberikan anotasi yang sangat rinci tentang premis dalam bukti, yang sangat berharga untuk pemilihan premis dalam theorem proving. Berkat kemampuan ekstraksi data LeanDojo, para peneliti juga telah mengembangkan ReProver, yang merupakan prover berbasis LLM pertama yang diperkuat dengan retrieval untuk pemilihan premis dari perpustakaan matematika yang besar.
ReProver dirancang untuk lebih mudah diakses dan hemat biaya dibandingkan metode sebelumnya yang bergantung pada dataset pribadi dan membutuhkan sumber daya komputasi yang besar. ReProver membutuhkan daya komputasi yang lebih sedikit dan dapat dilatih dengan hanya satu GPU per minggu. Kemampuan analisis program LeanDojo digunakan oleh mekanisme retrieval ReProver untuk menemukan premis yang mudah diakses dan menghasilkan contoh konkret tentang apa yang mungkin salah. Hasil eksperimen menunjukkan bahwa ReProver memiliki performa yang baik dibandingkan dengan metode tanpa retrieval dan GPT-4 saat menggunakan dataset benchmark ini untuk pelatihan dan evaluasi.
Dalam rangka penelitian dan evaluasi lebih lanjut, tim peneliti telah mengembangkan dataset benchmark baru yang terdiri dari 96.962 teorema dan bukti yang diekstraksi dari perpustakaan matematika Lean. Dataset benchmark ini memiliki pembagian data yang menantang, yang membutuhkan prover untuk menggeneralisasi teorema yang bergantung pada premis baru yang tidak digunakan selama pelatihan. Hasil eksperimen menunjukkan bahwa ReProver memiliki performa yang baik dibandingkan dengan metode tanpa retrieval dan GPT-4 saat menggunakan dataset benchmark ini untuk pelatihan dan evaluasi.
Secara keseluruhan, solusi open-source ini untuk theorem proving berbasis LLM menjanjikan untuk masa depan. Dengan menyediakan alat, data, model, dan benchmark yang mudah diakses, solusi ini mengatasi hambatan kode dan data pribadi serta kebutuhan komputasi yang besar. LeanDojo dan ReProver membuka pintu bagi pengembangan lebih lanjut dalam bidang theorem proving berbasis LLM.
Disarikan dari: Sumber