Menyelesaikan setiap masalah dalam salah satu tolok ukur matematik yang paling mencabar biasanya menghabiskan puluhan ribu dolar. NEAR AI baru sahaja melakukannya dengan harga $111.
Pada 6 September 2026, rakan penubuh NEAR Protocol, Alex Skidanov, mengumumkan bahawa agen open-source Lean projek tersebut telah menyelesaikan semua 672 masalah dalam tolok PutnamBench, satu set soalan yang diambil daripada Pertandingan Matematik William Lowell Putnam. Jumlah kos: $111. Penghantaran paling murah kedua berharga 250 kali lebih banyak.
Apa itu PutnamBench, dan mengapa ia penting
Pertandingan Putnam ialah pertandingan matematik sarjana muda yang paling bergengsi di Amerika Utara. Mendapat skor sifar bukanlah perkara yang tidak biasa, walaupun di kalangan pelajar cemerlang. Peperiksaan ini direka untuk menghancurkan anda.
PutnamBench, yang diperkenalkan pada 2024, mengambil tradisi kesukaran itu dan menjadikannya satu set penilaian rasmi untuk penyelesa teorem AI. Benchmar ini mengandungi 672 masalah yang dikodkan dalam Lean 4, bahasa pembantu bukti yang memerlukan hujah matematik ditulis dengan ketepatan yang boleh disahkan mesin. Sebuah bukti yang secara logik tidak kemas akan ditolak sepenuhnya, tiada markah separuh.
Sebelum keputusan NEAR AI, agen yang mencuba PutnamBench sering memerlukan ribuan panggilan inferens setiap masalah. Kos komputasi bertambah dengan cepat, menjadikan pelaksanaan penuh benchmark berada dalam julat perbelanjaan keseluruhan $10,000 hingga $25,000 untuk sistem terkemuka.
Agen Lean NEAR AI telah menyelesaikan keseluruhan set 672 masalah sebanyak $111.
Mengapa jurang kos adalah cerita sebenar
Pada harga $10,000 hingga $25,000 setiap larian penuh, hanya sedikit organisasi yang mampu mengulang, menguji, dan memperbaiki saluran pembuktian teorem mereka. Pada harga $111, pengiraan ini berubah sepenuhnya.
Kemajuan pantas dalam keputusan PutnamBench antara 2025 dan 2026 sudah didorong oleh alur kerja agen yang menggabungkan model bahasa besar dengan enjin semak bukti Lean. Pendekatan NEAR AI memperluas corak ini, tetapi menambahkan lapisan kecekapan yang belum pernah dilihat oleh komuniti benchmark sebelum ini.
NEAR AI telah menempatkan pencapaian ini dalam visi infrastruktur yang lebih luas yang berpusat pada apa yang disebutnya IronClaw, sebuah kerangka yang berorientasi pada AI rahsia dan boleh disahkan. Kemampuan pengesahan formal sesuai dengan kerangka ini secara langsung: jika anda boleh membuktikan bahawa hujah matematik adalah betul pada peringkat mesin, anda mempunyai asas untuk sistem AI yang outputnya boleh diaudit secara bebas daripada hanya dipercayai berdasarkan keyakinan.
Keputusan NEAR Protocol untuk menjadikan agen Lean sebagai sumber terbuka memperkuat kepentingannya. Alat milik sendiri yang memberikan keuntungan kos 250x cenderung kekal sebagai milik sendiri. Membuka sumber agen bermaksud metodologi ini tersedia untuk pemeriksaan, pengembangan, dan penggunaan oleh sesiapa sahaja.