Cảm giác là trí tuệ nhân tạo gần như mỗi tuần đều giải quyết một bài toán toán học mới. Tháng trước, riêng OpenAI đã công bố 719 bản thảo tuyên bố đã giải quyết một số vấn đề khó nhất trong lĩnh vực này. Ngay cả việc kiểm tra bằng máy tính cũng có thể sai sót. Sau nhiều năm tràn ngập nội dung rác từ AI, người ta không khỏi tự hỏi: liệu toán học có phải là lĩnh vực tiếp theo bị ảnh hưởng?
AxiomMath có thể tránh được số phận này không phải bằng cách giảm tốc độ, mà bằng cách xây dựng một nền tảng vững chắc hơn. Công ty khởi nghiệp định giá 1,6 tỷ USD này mong muốn tạo ra một lớp nền đã được xác minh, để các đại lý AI có thể dựa vào đó để viết phần mềm và cuối cùng thực hiện các nghiên cứu khoa học.
Vào thứ Tư, công ty đã thông báo đã xác minh chính thức Stacks Project, một trong những thành tựu toán học lớn nhất do con người viết ra. Các nhà toán học thường đánh giá rất cao Stacks. Nhà toán học tại Đại học Columbia, Peter Woit, từng gọi nó là “khó có gì sánh được”, và so sánh dự án này với “bộ sách Bourbaki nổi tiếng” – bộ sách tái xây dựng toán học từ nền tảng vào thế kỷ 20.
Đồng nghiệp của Woit tại Colombia, Johan de Jong, đã khởi động Dự án Stacks vào năm 2005 như một tài liệu tham khảo mã nguồn mở. Kể từ đó, các nhà toán học đã liên tục đóng góp, mở rộng từ đại số cấp đại học đến những ý tưởng tiên tiến nhất trong các lĩnh vực như đại số, hình học và lý thuyết số.
Nhóm đại lý AI của công ty đã dịch cơ sở dữ liệu khoảng 7.654 trang này thành khoảng 16 triệu dòng mã có thể được máy tính kiểm tra.
Mục đích của toán học hình thức là đảm bảo cấu trúc nền tảng của nó là đáng tin cậy. Các nhà toán học sẽ dùng một ngôn ngữ lập trình gọi là Lean để chuyển đổi các chứng minh thành mã nguồn, sau đó một chương trình gọi là proof assistant sẽ kiểm tra từng dòng mã này. Nếu chứng minh được xác nhận, các nhà toán học có thể tin rằng nó hợp lệ về mặt logic.
Các kỹ sư cũng sử dụng cùng tư tưởng này, tức là xác minh hình thức, để xác minh xem thiết kế chip có khả thi hay không; các nhà nghiên cứu Pháp đã dùng nó để phát hiện lỗ hổng phần mềm tính trợ cấp gia đình.
Đối với các dự án như Stacks Project, việc kiểm tra từng định lý chỉ là một phần công việc. Các định lý và định nghĩa trong Stacks liên kết với nhau, mỗi định lý đều dựa trên những nội dung trước đó. Giống như gia phả, nhiều kết quả trong Stacks có thể truy ngược về các kết quả sớm hơn.
Sự liên kết này khiến Axiom ban đầu không chắc liệu dự án này có khả thi hay không. Nhóm phải đảm bảo mọi kết nối đều nguyên vẹn trong khoảng 16 triệu dòng mã Lean.
Giám đốc điều hành của Axiom, Carina Hong, cho biết với TechCrunch: “Trong thực tế, quy mô lớn và độ tinh vi thường không đi kèm với nhau. [Stacks] là một tập hợp các kết quả toán học tạo thành nền tảng toán học. Bạn mong muốn các [định lý] nhất quán với nhau, chứ không phải mâu thuẫn như các nghịch lý. Bạn cũng mong muốn các định nghĩa này không xung đột với nhau.”
Vị CEO 25 tuổi từng bỏ dở chương trình tiến sĩ toán học tại Stanford và thành lập công ty này vào tháng 3 năm 2025. Tháng 3 năm nay, Axiom đã huy động thành công vòng gọi vốn A trị giá 200 triệu đô la Mỹ do Menlo Ventures dẫn đầu.
Hong nói: “Lúc đó chúng tôi không chắc liệu vibe coding có thể giữ được vẻ đẹp của Stacks hay không.”
Để hoàn thành dự án này, đội ngũ đã thiết lập một cấu trúc linh hoạt cho các đại lý và cho phép chúng chạy song song. Ashvin Swaminathan, thành viên nhóm kỹ thuật Axiom, cho biết: “Đối với Stacks, chúng tôi đã thiết lập một cấp bậc… nhưng không phải là cấp bậc quy định chặt chẽ từng đại lý phải làm gì. Các đại lý sẽ tự tìm kiếm nhiệm vụ và nhận diện những việc có thể xử lý song song.”
Axiom cũng đã huấn luyện các mô hình của riêng mình để chúng trở nên giỏi về toán học. Hong cho biết, cách làm này là điều mà hầu hết các startup xác thực khác chưa thực hiện. Ban đầu, nhóm phụ thuộc vào một chuyên gia Lean nội bộ để dạy các đại lý hình thành các tiêu chuẩn phán đoán tương tự con người. Theo thời gian, Hong nói, các đại lý đã tự học được khả năng phán đoán này.
Thành tựu này đã lấp đầy một trong những khoảng trống lớn nhất trong toán học hình thức. Swaminathan nói: “Khi bạn xem xét những nội dung toán học đã được hình thức hóa, bạn sẽ thấy có một hố đen khổng lồ. Và hố đen đó bao trùm lên hình học đại số.”
Swaminathan cho biết, cho đến nay, các nhà nghiên cứu muốn sử dụng Lean để kiểm tra các công việc mới trong hình học đại số gần như không có sẵn nền tảng nào. “Bây giờ họ đã có.”
Axiom cho rằng mỗi kết quả đã được xác minh đều trở thành một khối xây dựng, cho phép các chứng minh tương lai được xây dựng dựa trên toán học đã được kiểm tra, thay vì phải bắt đầu từ đầu. Nhà toán học UCLA, người đoạt giải Fields Terence Tao, tóm gọn điều này một cách súc tích hơn: “Bạn càng có nhiều chứng minh hình thức, bạn càng có thể tạo ra nhiều chứng minh hình thức hơn.”
Đối tượng mục tiêu của Axiom không chỉ là các nhà toán học. Các nhà phát triển đã lâu nay nỗ lực đảm bảo mã của họ không có lỗ hổng và mối đe dọa bảo mật. Với việc các đại lý AI ngày càng viết nhiều phần mềm hơn, vấn đề này sẽ chỉ trở nên lớn hơn.
Axiom đặt cược, phần mềm tương lai cần được xây dựng trên những nền tảng đã được xác minh, giống như Stacks ngày nay.
Swaminathan nói: “Chúng tôi cho rằng, toán học là lĩnh vực bạn bắt đầu xây dựng những thứ này, và đó là một kỹ năng có thể chuyển đổi. Các đại lý có thể đọc mã của chúng tôi, hiểu nó và xây dựng cơ sở hạ tầng mới trên đó. Những gì chúng tôi đã hình thức hóa bằng Lean hiện nay chính là nền tảng cơ sở mà các đại lý có thể xây dựng lên.”
Cách Axiom xây dựng đại lý cho Stacks — làm việc song song và tự chọn nhiệm vụ — chính là cách Hong dự đoán nhiều công việc AI sẽ diễn ra trong tương lai. Cô cho rằng, các đại lý AI cần một cơ sở tri thức được cấu trúc tốt và có thể tái sử dụng để tránh tạo ra nội dung vô giá trị.
Hong nói: “Bạn muốn [đại lý] có một kho dữ liệu có thể tái sử dụng, nơi chúng có thể tiếp tục xây dựng và đẩy dần ranh giới tiến bộ. Nếu ngay từ đầu bạn nhét đầy rác vào với những lựa chọn kỹ thuật kém, thì rất khó để mở rộng ranh giới đó.”
Hong rất tự tin vào phương pháp này và thậm chí đã công khai đưa ra lời thách thức. Cô nói: “Tôi thách thức công khai tất cả các công ty lập trình hãy thực hiện công việc định dạng ở quy mô này.”