Axiom Math nỗ lực ngăn chặn ‘rác AI’ trong toán học bằng xác thực hình thức

Trong bối cảnh AI liên tục đưa ra các giải pháp cho những bài toán hóc búa, rủi ro về những kết quả sai lệch hoặc thiếu căn cứ—thường được gọi là “AI slop”—đang trở thành mối lo ngại lớn trong cộng đồng khoa học. Axiom Math, một startup được định giá 1,6 tỷ USD, đang đặt cược vào phương pháp xác thực hình thức (formal verification) để xây dựng một nền tảng toán học đáng tin cậy cho các tác nhân AI.

Mới đây, Axiom đã công bố hoàn thành việc xác thực chính thức Stacks Project, một trong những kho tàng kiến thức toán học đồ sộ nhất do con người tạo ra. Dự án này bao gồm các kết quả từ đại số cơ bản đến các lý thuyết nâng cao về hình học và lý thuyết số. Đội ngũ AI của Axiom đã chuyển đổi khoảng 7.654 trang tài liệu này thành 16 triệu dòng mã được kiểm tra bởi máy tính.

Cơ chế xác thực hình thức

Quy trình này dựa trên ngôn ngữ lập trình Lean. Các nhà toán học viết lại các chứng minh dưới dạng mã, sau đó một chương trình hỗ trợ chứng minh (proof assistant) sẽ kiểm tra từng dòng một. Nếu mã vượt qua quá trình kiểm tra, kết quả đó được coi là có tính logic chặt chẽ. Kỹ thuật này vốn đã được các kỹ sư chip sử dụng để đảm bảo thiết kế phần cứng không lỗi, hoặc dùng để phát hiện lỗ hổng trong các phần mềm tính toán phúc lợi xã hội.

Thách thức lớn nhất đối với Axiom là tính liên kết chặt chẽ của Stacks Project. Mỗi định lý đều xây dựng dựa trên các kết quả trước đó, tạo thành một hệ thống phụ thuộc lẫn nhau phức tạp. CEO Carina Hong cho biết, việc giữ cho các kết nối này nhất quán mà không tạo ra các nghịch lý là yếu tố then chốt.

Tương lai của AI và phát triển phần mềm

Axiom không chỉ nhắm đến giới toán học. Họ tin rằng khi các tác nhân AI ngày càng tham gia nhiều vào việc viết code, nhu cầu về một nền tảng được xác thực là vô cùng cấp thiết. Bằng cách cung cấp một thư viện toán học đã được kiểm chứng, Axiom tạo ra “chất nền” (substrate) để các tác nhân AI có thể xây dựng hạ tầng phần mềm mới một cách an toàn hơn, giảm thiểu các vulnerability (lỗ hổng) và lỗi logic.

Ashvin Swaminathan, thành viên đội ngũ kỹ thuật của Axiom, nhấn mạnh rằng các kết quả đã được xác thực sẽ trở thành những khối xây dựng (building block) cho các chứng minh tương lai. Thay vì bắt đầu từ con số không, AI có thể dựa trên những kiến thức đã được kiểm chứng để mở rộng biên giới tri thức mà không rơi vào tình trạng tạo ra những kết quả thiếu chính xác.

Với thành công này, Axiom đã đưa ra lời thách thức đối với các công ty phát triển phần mềm AI khác: hãy cùng tập trung vào việc xác thực hình thức ở quy mô lớn để đảm bảo sự phát triển bền vững và chính xác cho công nghệ trong tương lai.

Nguồn tham khảo: TechCrunch