Trong bối cảnh AI ngày càng sản sinh ra vô số bài toán toán học mới, Axiom Math đang đặt cược vào việc xác thực nghiêm ngặt để ngăn chặn những kết quả không đáng tin cậy. Startup này vừa công bố đã formal verification hoàn tất toàn bộ thư viện Stacks Project – một trong những tác phẩm toán học lớn nhất từng được viết bởi con người.
Stacks Project, được khởi xuất năm 2005 bởi nhà toán học Johan de Jong tại Columbia, là tài liệu tham khảo mở bao gồm hơn 7.654 trang về đại số cơ bản đến các lý thuyết nâng cao nhất. Axiom đã chuyển đổi nội dung này thành khoảng 16 triệu dòng code Lean, trong khi các AI agent của công ty phải duy trì mọi liên kết logic giữa các định lý một cách nhất quán.
- Formal verification giúp chắc chắn các bằng chứng logic không lỗi, tương tự cách xác thực thiết kế chip hay phần mềm.
- Hệ thống agent của Axiom hoạt động song song, tự động phát hiện và chia sẻ công việc để xử lý quy mô khổng lồ.
Nhà sáng lập tuổi 25, Carina Hong – chủ bị mất PhD Toán học tại Stanford – cho biết đây là bước đệm đầu tiên để xây dựng nền tảng toán học được AI tin cậy, từ đó có thể mở rộng sang ứng dụng trong khoa học và phần mềm.
Thành công của Axiom không chỉ là thể hiện tiềm năng của AI trong lĩnh vực trí tuệ nhân tạo, mà còn mở ra kỷ nguyên mới cho toán học học máy – nơi các kết quả được kiểm chứng chặt chẽ trước khi được công bố. Cộng đồng AI Việt Nam đang quan tâm đến các công cụ này để phát triển hệ thống an toàn và đáng tin cậy hơn.
Nguồn: TechCrunch — Biên dịch & tổng hợp: danhbaai.com