Agen AI rancang algoritma evolusioner dan buktikan batas waktunya di Lean

Sebuah pracetak di arXiv memperkenalkan sistem agen AI yang tidak hanya mengusulkan algoritma optimisasi, tetapi juga membuktikan secara formal berapa lama algoritma itu berjalan. Makalah berjudul Agentic Algorithm Design ditulis oleh Per Kristian Lehre. Menurut halaman arXiv, versi pertamanya terbit 26 Oktober 2026 dan versi keduanya 27 Oktober 2026. Makalah ini belum ditelaah sejawat.

Pertanyaan yang diajukan penulis sederhana tetapi berat: apakah model bahasa besar (LLM) bisa merancang algoritma sekaligus memastikan efisiensinya dengan bukti matematis? Menurut abstraknya, bukti bahwa LLM mampu melakukan keduanya masih sangat sedikit.

Dari uji empiris ke bukti formal

Abstrak menyebut pendekatan seperti AlphaEvolve sebagai contoh desain heuristik berbasis LLM yang murni empiris. Dalam pendekatan semacam itu, kandidat algoritma dievaluasi pada sekumpulan fungsi uji, lalu yang berkinerja baik divariasikan lewat perintah ke LLM untuk menghasilkan versi lebih baik. Menurut makalah, cara ini sudah berhasil di banyak domain, tetapi tidak memberi jaminan tentang kebenaran atau kinerja algoritma yang dihasilkan.

Lean adalah bahasa pemrograman sekaligus asisten pembuktian formal: setiap langkah bukti diperiksa mesin. Batas waktu jalan (runtime bound) adalah batas atas jumlah langkah yang dibutuhkan algoritma untuk mencapai solusi, dalam makalah ini diukur dengan jumlah kueri ke fungsi yang dioptimalkan. Batas itu biasanya ditulis dengan notasi O besar, yang menunjukkan bagaimana kebutuhan waktu tumbuh seiring ukuran masalah.

Lehre mengutip argumen bahwa pembuktian teorema otomatis sulit bagi AI karena sebuah bukti hanya benar atau salah, dan ruang kemungkinan bukti sangat besar. Desain algoritma formal, menurut makalah, melangkah lebih jauh karena sistem harus menjelajahi ruang desain sekaligus membuktikan sifat-sifatnya.

Cara kerja pipeline

Pipeline dibangun bertahap dengan meniru metode riset dalam desain dan analisis algoritma evolusioner. Pada tahap informal, model menulis deskripsi desain dalam bentuk prosa. Pada tahap formal, agen harus menyusun definisi atau bukti yang kemudian diperiksa Lean. Jika Lean melaporkan kegagalan, tahap itu diulang sampai lolos atau sampai agen mundur, dengan waktu mundur ditentukan oleh urutan Luby, yaitu jadwal baku untuk memutuskan kapan sebuah percobaan diulang dari awal.

Salah satu komponen kuncinya adalah penjaga (guard) Lean yang menyaring desain cacat. Algoritma hanya diterima jika mampu menjangkau seluruh bagian ruang pencarian, memakai keacakan, dan memperhitungkan nilai fungsi yang dikembalikan oracle, yakni pihak yang mengetahui fungsi yang dioptimalkan. Pembatasan ini perlu karena model black-box membuka peluang bagi banyak algoritma yang sebagian besar tidak berguna.

Untuk membuktikan batas waktu, agen mendefinisikan fungsi potensial, alat bantu analisis yang bukan bagian dari algoritma itu sendiri. Dari perubahan potensial per kueri, yang dikenal sebagai analisis drift, dapat diturunkan batas waktu jalan. Algoritma awal dalam semua percobaan adalah pencarian acak seragam dengan waktu jalan yang diharapkan O(2^n). Menurut abstrak, tidak ada perbandingan empiris antaralgoritma pada tahap mana pun.

Hasil yang diklaim

Menurut abstrak, agen menghasilkan algoritma dengan waktu jalan yang diharapkan O(n^2) pada masalah CycleUncover, sedangkan algoritma klasik (1+1) EA membutuhkan waktu eksponensial. Untuk minimisasi submodular bernilai bulat, pipeline menghasilkan algoritma dengan waktu jalan yang diharapkan O(n^(2+2c)). Pada masalah LeadingOnes, hasilnya setara dengan batas klasik O(n^2).

Dari 8 kelas masalah, 12 dari 15 run dengan model frontier menyelesaikan seluruh pipeline dengan batas waktu jalan yang diperiksa mesin. Penulis juga melaporkan studi ablasi: ketika tahap-tahap dihilangkan dan agen diminta langsung merancang algoritma beserta jaminan waktunya, hasilnya adalah salinan algoritma awal berupa pencarian acak, atau bukti yang tidak lengkap. Sepengetahuan penulis, ini contoh pertama pipeline otomatis yang merancang algoritma optimisasi black-box efisien dengan batas waktu yang diperiksa Lean.

Keterbatasan

Klaim ini perlu dibaca dengan cermat. Pembuktian formal menjamin bahwa bukti sahih terhadap pernyataan yang dirumuskan, bukan bahwa pernyataan itu menangkap setiap detail masalah nyata. Makalah menyebut agen mampu memanfaatkan struktur pada kelas masalah yang dianonimkan, dan pengujian dilakukan pada kelas-kelas masalah teori optimisasi, bukan pada beban kerja praktis.

Tiga dari 15 run tidak menyelesaikan pipeline, dan abstrak tidak menjelaskan penyebabnya. Menurut catatan di halaman arXiv, kode sumber baru akan dipublikasikan kemudian, sehingga pihak luar belum bisa memeriksa implementasinya. Makalah ini juga belum melewati penelaahan sejawat.

Meski begitu, arah risetnya relevan bagi keandalan algoritma buatan AI. Pengujian empiris hanya menunjukkan kinerja pada fungsi uji tertentu, sedangkan bukti formal memberi jaminan yang lebih umum, sejauh model dan definisi yang dipakai sesuai dengan masalah sebenarnya.

Apa berikutnya

Penulis menyatakan repositori kode akan dipublikasikan kemudian. Pipeline juga dapat diulang: pada sebagian besar percobaan hanya satu iterasi dijalankan, sementara dua run diulang hingga tiga dan lima generasi. Penulis menyimpulkan bahwa spesifikasi yang diperiksa mesin di Lean dapat menggantikan evaluasi empiris dalam penemuan algoritma terbuka, sebuah dugaan yang masih perlu diuji pada masalah yang lebih beragam.