Peneliti Departemen Matematika MIT David Roe ’06 dan Andrew Sutherland ’90, PhD ’07 termasuk di antara penerima perdana Renaissance Philanthropy dan XTX Markets’ Hibah AI untuk Matematika.
Empat alumni Mit tambahan — Anshula Gandhi ’19, Viktor Kunčak SM ’01, PhD ’07; Greaja Ranade ’07; dan Damiiano testa phd ’05 — juga diasah untuk proyek penyelesaian.
29 proyek pemenang pertama akan mendukung ahli matematika dan peneliti di universitas dan organisasi yang berupaya mengembangkan sistem kecerdasan buatan yang membantu memajukan penemuan dan penelitian matematika di beberapa tugas utama.
Roe dan Sutherland, bersama Chris Birkbeck dari University of East Anglia, akan menggunakan hibah mereka untuk meningkatkan pembuktian teorema otomatis dengan membangun hubungan antar L-Fungsi dan Basis Data Bentuk Modular (LMFDB) dan Perpustakaan matematika Lean4 (matematika).
“Pembukti teorema otomatis cukup terlibat secara teknis, namun pengembangannya kekurangan sumber daya,” kata Sutherland. Dengan teknologi AI seperti model bahasa besar (LLM), hambatan untuk masuk ke alat-alat formal ini berkurang dengan cepat, sehingga kerangka kerja verifikasi formal dapat diakses oleh para ahli matematika yang bekerja.
Mathlib adalah perpustakaan matematika besar berbasis komunitas untuk Bersandar pembukti teorema, sistem formal yang memverifikasi kebenaran setiap langkah dalam pembuktian. Mathlib saat ini berisi di urutan 105 hasil matematika (seperti lemma, proposisi, dan teorema). LMFDB, sumber daya online kolaboratif yang sangat besar yang berfungsi sebagai semacam “ensiklopedia” teori bilangan modern, berisi lebih dari 109 pernyataan konkrit. Sutherland dan Roe adalah redaktur pelaksana LMFDB.
Hibah Roe dan Sutherland akan digunakan untuk proyek yang bertujuan untuk meningkatkan kedua sistem, membuat hasil LMFDB tersedia dalam mathlib sebagai pernyataan yang belum dibuktikan secara formal, dan memberikan definisi formal yang tepat dari data numerik yang disimpan dalam LMFDB. Jembatan ini akan menguntungkan ahli matematika manusia dan agen AI, dan menyediakan kerangka kerja untuk menghubungkan database matematika lainnya ke sistem pembuktian teorema formal.
Hambatan utama dalam mengotomatisasi penemuan dan pembuktian matematis adalah terbatasnya jumlah pengetahuan matematika yang diformalkan, tingginya biaya untuk memformalkan hasil yang kompleks, dan kesenjangan antara apa yang dapat diakses secara komputasi dan apa yang layak untuk diformalkan.
Untuk mengatasi kendala ini, para peneliti akan menggunakan dana tersebut untuk membangun alat untuk mengakses LMFDB dari mathlib, membuat database besar pengetahuan matematika yang belum diformalkan dapat diakses oleh sistem pembuktian formal. Pendekatan ini memungkinkan asisten pembuktian untuk mengidentifikasi target spesifik untuk formalisasi tanpa perlu memformalkan seluruh korpus LMFDB terlebih dahulu.
“Membuat database besar berisi fakta-fakta teori bilangan yang belum diformalkan tersedia dalam mathlib akan memberikan teknik yang ampuh untuk penemuan matematika, karena kumpulan fakta yang mungkin ingin dipertimbangkan oleh agen saat mencari teorema atau bukti secara eksponensial lebih besar daripada kumpulan fakta yang pada akhirnya perlu diformalkan untuk membuktikan teorema tersebut,” kata Roe.
Para peneliti mencatat bahwa pembuktian teorema baru di garis depan pengetahuan matematika sering kali melibatkan langkah-langkah yang mengandalkan komputasi nontrivial. Misalnya, pembuktian Teorema Terakhir Fermat oleh Andrew Wiles menggunakan apa yang dikenal sebagai “trik 3-5” pada titik penting dalam pembuktian.
“Trik ini bergantung pada fakta bahwa kurva modular X_0(15) hanya memiliki banyak titik rasional, dan tidak satu pun titik rasional tersebut sesuai dengan kurva elips semi-stabil,” menurut Sutherland. “Fakta ini telah diketahui jauh sebelum karya Wiles, dan mudah diverifikasi menggunakan alat komputasi yang tersedia dalam sistem aljabar komputer modern, namun hal ini bukanlah sesuatu yang dapat dibuktikan secara realistis menggunakan pensil dan kertas, juga tidak mudah untuk diformalkan.”
Meskipun pembukti teorema formal dihubungkan ke sistem aljabar komputer untuk verifikasi yang lebih efisien, memanfaatkan keluaran komputasi dalam database matematika yang ada menawarkan beberapa manfaat lain.
Menggunakan hasil yang disimpan akan memanfaatkan waktu komputasi ribuan tahun CPU yang telah dihabiskan dalam pembuatan LMFDB, sehingga menghemat uang yang diperlukan untuk mengulangi komputasi ini. Memiliki informasi yang telah dihitung sebelumnya juga memungkinkan pencarian contoh atau contoh tandingan tanpa mengetahui sebelumnya seberapa luas pencarian tersebut. Selain itu, database matematika adalah gudang yang dikurasi, bukan sekadar kumpulan fakta acak.
“Fakta bahwa para ahli teori bilangan menekankan peran konduktor dalam database kurva elips telah terbukti penting bagi satu penemuan matematika penting yang dibuat menggunakan alat pembelajaran mesin: gumamankata Sutherland.
“Langkah kami selanjutnya adalah membangun tim, terlibat dengan komunitas LMFDB dan mathlib, mulai memformalkan definisi yang mendasari kurva elips, bidang bilangan, dan bagian bentuk modular LMFDB, dan memungkinkan untuk menjalankan pencarian LMFDB dari dalam mathlib,” kata Roe. “Jika Anda seorang mahasiswa MIT yang tertarik untuk terlibat, silakan menghubungi kami!”
