Axiom Math Verifikasi 7.600 Halaman Matematika Pakai Agen AI
Startup Axiom Math berhasil memverifikasi Stacks Project ke dalam 16 juta baris kode Lean guna menekan risiko kode berkualitas rendah pada software masa depan.
Foto: TechCrunch (Dokumentasi editorial)
Poin penting
- Axiom Math memverifikasi 7.654 halaman Stacks Project menjadi 16 juta baris kode pembuktian Lean.
- Armada agen AI otonom bekerja secara paralel menentukan tugas verifikasi tanpa hierarki kerja kaku.
- Metode verifikasi formal disiapkan sebagai fondasi agar kode buatan AI lebih andal dan minim eror.
Lonjakan adopsi kecerdasan buatan memicu kekhawatiran mengenai maraknya kode program dan data berkualitas rendah atau AI slop. Menjawab tantangan tersebut, startup Axiom Math memverifikasi Stacks Project, salah satu arsip matematika terbesar di dunia, menjadi kode komputer teruji.
Sebagaimana dilaporkan TechCrunch, perusahaan bervaluasi 1,6 miliar dolar AS itu mengerahkan armada agen AI untuk menerjemahkan sekitar 7.654 halaman Stacks Project ke dalam 16 juta baris kode.
Otomasi Verifikasi Formal Skala Besar
Stacks Project dirintis matematikawan Universitas Columbia Johan de Jong sejak 2005 sebagai referensi aljabar dan geometri tingkat lanjut. Axiom mengonversi materi rumit tersebut ke dalam bahasa pemrograman Lean.
Lean bekerja bersama proof assistant, yaitu perangkat lunak pemeriksa logika yang menguji kebenaran setiap baris pembuktian secara matematis. Metode ini dikenal sebagai verifikasi formal, teknik validasi sistematis yang umum dipakai insinyur semikonduktor guna memastikan rancangan cip bekerja tepat.
"Banyak hal berukuran besar dan bernilai rumit biasanya sulit disatukan. Anda tentu menginginkan struktur fondasi yang konsisten dan tidak kontradiktif," ujar Carina Hong, CEO Axiom Math.
Agen AI milik Axiom bekerja mandiri secara paralel untuk menemukan relasi antarteorema tanpa instruksi kaku per langkah. Startup yang mengantongi pendanaan Seri A 200 juta dolar AS dari Menlo Ventures ini membuktikan agen AI sanggup membangun sistem pengetahuan terstruktur dalam skala masif.
Ambisi Menopang Keandalan Rekayasa Software
Ambisi Axiom melampaui ranah riset akademis. Mengingat kian banyaknya kode aplikasi yang ditulis oleh AI generatif, para pengembang menghadapi tantangan besar dalam memastikan software bebas dari bug dan celah keamanan.
Axiom meyakini pustaka matematika terverifikasi ini dapat menjadi landasan kokoh bagi agen perangkat lunak masa depan. Melalui pendekatan berbasis logika formal tersebut, perusahaan berharap agen AI di masa depan dapat merancang sistem komputasi yang jauh lebih aman dari risiko bug fatal.
Apa Artinya bagi Pelaku Usaha
Bagi direktur teknologi dan pengelola bisnis di Indonesia, terobosan Axiom Math menegaskan bahwa kecepatan coding AI harus diimbangi oleh validasi logika yang ketat. Ketergantungan buta pada asisten AI tanpa kontrol kualitas berlapis berisiko tinggi membengkakkan biaya perbaikan celah keamanan sistem di kemudian hari.
Pelaku usaha yang mulai memanfaatkan AI dalam pengembangan piranti lunak operasional perlu mulai mengevaluasi alat audit kode berbasis verifikasi formal. Menerapkan disiplin pengujian otomatis sejak awal jauh lebih hemat biaya daripada menanggung kerugian akibat kegagalan transaksi sistem.
Langkah mitigasi praktis yang dapat diambil adalah mewajibkan tinjauan sintaks dan logika teruji sebelum kode buatan AI masuk ke tahap produksi. Jadikan verifikasi komputasi sebagai pagar pengaman utama agar efisiensi otomasi tetap diimbangi keandalan sistem bisnis yang prima.
- TechCrunch: Axiom Math wants to keep AI slop out of mathematics
Lihat hasil pemeriksaan (9 klaim)
| Klaim | Putusan | Dasar di sumber |
|---|---|---|
| Axiom Math memverifikasi sekitar 7.600 atau 7.654 halaman Stacks Project menjadi 16 juta baris kode komputer. | Didukung | “translates the library’s roughly 7,654 pages into about 16 million lines of computer-checked code.” TechCrunch melaporkan bahwa armada agen AI Axiom menerjemahkan sekitar 7.654 halaman Stacks Project ke dalam 16 juta baris kode. |
| Axiom Math memiliki valuasi 1,6 miliar dolar AS. | Didukung | “The $1.6 billion startup wants to build a verified foundation that AI agents can rely on to write software and, eventually, do science.” TechCrunch menyebut Axiom Math sebagai startup bernilai 1,6 miliar dolar AS. |
| Stacks Project dirintis oleh matematikawan Columbia Johan de Jong sejak 2005 sebagai referensi terbuka aljabar dan geometri. | Didukung | “Johan de Jong started the Stacks Project in 2005 as an open source reference.” TechCrunch menyatakan Johan de Jong dari Universitas Columbia memulai Stacks Project pada 2005 sebagai referensi sumber terbuka. |
| Matematikawan menulis ulang pembuktian dalam bahasa Lean dan proof assistant memeriksanya baris per baris; metode verifikasi formal serupa digunakan insinyur untuk memeriksa desain cip. | Didukung | “Engineers use the same idea, called formal verification, to confirm their chip designs work” TechCrunch menjelaskan konsep verifikasi formal di Lean dan pemanfaatannya oleh para insinyur untuk memastikan rancangan cip bekerja. |
| CEO Axiom Carina Hong menyatakan bahwa hal-hal besar dan rumit biasanya sulit disatukan dan struktur matematika harus konsisten serta tidak kontradiktif. | Didukung | “Things that are big and things that are delicate in life just don’t go together” TechCrunch mengutip pernyataan CEO Axiom Carina Hong mengenai sifat proyek yang masif dan rumit. |
| Agen AI Axiom bekerja secara paralel dan menemukan tugas sendiri tanpa hierarki kaku yang mendikte setiap agen. | Didukung | “The agents were finding tasks for themselves and identified things that they could work on in parallel.” TechCrunch mengutip Ashvin Swaminathan dari Axiom mengenai cara kerja agen AI yang mencari tugas sendiri dan bekerja paralel. |
| Axiom mengantongi pendanaan Seri A senilai 200 juta dolar AS yang dipimpin oleh Menlo Ventures pada Maret 2025. | Didukung | “In March, Axiom raised a $200 million Series A led by Menlo Ventures .” TechCrunch mencatat Axiom meraih pendanaan Seri A sebesar 200 juta dolar AS dari Menlo Ventures. |
| Pengembang kesulitan memastikan kode bebas bug dan celah keamanan seiring bertambahnya kode yang ditulis oleh agen AI. | Didukung | “Developers have long struggled to guarantee that their code is free of bugs and security holes. That problem grows as AI agents write more of the world’s code.” TechCrunch menyebutkan kendala pengembang dalam menjamin kebersihan kode dari bug dan celah keamanan saat AI makin banyak menulis kode. |
| Axiom bertaruh bahwa software masa depan perlu bersandar pada fondasi terverifikasi seperti halnya Stacks Project. | Didukung | “Axiom is betting that the software of the future will need to rest on verified foundations, the way Stacks now does.” TechCrunch menulis bahwa Axiom bertaruh software masa depan akan membutuhkan landasan terverifikasi. |
Video AI terbaru
Washington, D.C. is up next. 🏛️
