Có cảm giác như AI đang giải một bài toán mới mỗi tuần. Tháng trước, riêng OpenAI đã phát hành 719 bản thảo khẳng định giải pháp cho một số vấn đề khó khăn nhất của lĩnh vực này. Ngay cả việc kiểm tra máy tính cũng có thể bị trượt. Sau nhiều năm AI sa sút, thật công bằng khi tự hỏi liệu toán học có phải là lĩnh vực tiếp theo hay không.
AxiomMath đang đặt cược toán học có thể tránh được số phận đó, không phải bằng cách chậm lại mà bằng cách đứng trên nền tảng vững chắc hơn. Công ty khởi nghiệp trị giá 1,6 tỷ USD muốn xây dựng một nền tảng đã được xác minh mà các tác nhân AI có thể dựa vào để viết phần mềm và cuối cùng là nghiên cứu khoa học.
Vào thứ Tư, công ty thông báo họ đã chính thức xác minh Dự án Stacks, một trong những dự án toán học lớn nhất từng được con người viết ra. Các nhà toán học thường đánh giá cao Stacks—Nhà toán học người Columbia, Peter Woit đã tuyên bố rằng “không có gì khác thực sự có thể so sánh được”, so sánh dự án với “những cuốn sách Bourbaki nổi tiếng”, một bộ sách xây dựng lại toán học từ nền tảng của nó vào thế kỷ 20.
Đồng nghiệp của Woit ở Columbia, Johan de Jong, đã bắt đầu Dự án Stacks vào năm 2005 dưới dạng tài liệu tham khảo nguồn mở. Kể từ đó, các nhà toán học đã đóng góp cho nó, xây dựng các kết quả từ đại số cấp đại học cho đến những ý tưởng tiên tiến nhất trong lĩnh vực đại số, hình học và lý thuyết số.
Đội ngũ nhân viên AI của công ty dịch khoảng 7.654 trang của thư viện thành khoảng 16 triệu dòng mã được máy tính kiểm tra.
Công thức hóa toán học là một cách đảm bảo cấu trúc bên dưới nó vững chắc. Các nhà toán học viết lại bằng chứng dưới dạng mã bằng ngôn ngữ lập trình có tên Lean và một chương trình được gọi là trợ lý chứng minh sẽ kiểm tra từng dòng mã. Nếu bằng chứng được thông qua, các nhà toán học có thể tin tưởng rằng nó hợp lý về mặt logic.
Các kỹ sư sử dụng ý tưởng tương tự, được gọi là xác minh chính thức, để xác nhận thiết kế chip của họ hoạt động, trong khi các nhà nghiên cứu ở Pháp đã sử dụng nó để phát hiện lỗi trong phần mềm tính toán lợi ích gia đình.
Đối với một thư viện như Dự án Stacks, 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 Ngăn xếp được kết nối với nhau và mỗi định lý được xây dựng dựa trên các định lý trước đó. Giống như một cây phả hệ, nhiều kết quả trong Stacks có nguồn gốc từ những kết quả trước đó.
Sự liên kết đó khiến Axiom không chắc chắn rằng dự án ban đầu sẽ hoạt động. Nhóm phải giữ nguyên mọi kết nối trong khoảng 16 triệu dòng mã Lean.
Giám đốc điều hành Axiom Carina Hong nói với TechCrunch: “Những điều to lớn và những điều tế nhị trong cuộc sống không đi đôi với nhau”. “(Stacks) là tập hợp các kết quả toán học làm nền tảng của toán học. Bạn muốn (các định lý) nhất quán và không giống như nghịch lý. Bạn muốn các định nghĩa không xung đột với nhau.”
Vị CEO 25 tuổi đã bỏ học Tiến sĩ toán học Stanford. chương trình thứ đã thành lập công ty vào tháng 3 năm 2025. Vào tháng 3, Axiom đã huy động được Series A trị giá 200 triệu đô la do Menlo Ventures dẫn đầu.
Hong nói: “Chúng tôi không chắc liệu mã hóa rung cảm có thể giữ được vẻ đẹp của Stacks hay không.
Để thực hiện dự án, nhóm đã tạo cho các đại lý của mình một cấu trúc lỏng lẻo và để họ chạy song song. Ashvin Swaminathan, một thành viên đội ngũ kỹ thuật của Axiom cho biết: “Với Stacks, chúng tôi đã áp đặt một hệ thống phân cấp… (nhưng) nó không giống như một hệ thống phân cấp hoàn chỉnh để ra lệnh cho mọi tác nhân đơn lẻ đang làm gì”. “Các đặc vụ đang tìm kiếm nhiệm vụ cho chính họ và xác định những việc mà họ có thể làm song song.”
Axiom cũng đào tạo các mô hình của riêng mình để giỏi toán, một cách tiếp cận mà Hong cho biết hầu hết các công ty khởi nghiệp xác minh khác chưa thực hiện. Lúc đầu, nhóm dựa vào một trong những chuyên gia Lean nội bộ của mình để dạy cho các đại lý cảm giác về vị giác của con người. Hong cho biết, theo thời gian, các đại lý đã tự mình tiếp thu được sở thích.
Kết quả này lấp đầy một trong những lỗ hổng lớn nhất trong toán học chính thức. Swaminathan nói: “Khi bạn nhìn vào những gì đã được hình thức hóa trong toán học, có một lỗ đen khổng lồ. Và lỗ đen đó bao trùm hình học đại số”.
Swaminathan cho biết, cho đến nay, các nhà nghiên cứu muốn kiểm tra công trình mới về hình học đại số với Lean vẫn chưa có nhiều cơ sở để xây dựng. “Ồ, bây giờ họ đã làm được.”
Axiom lập luận rằng mỗi kết quả được xác minh sẽ trở thành một khối xây dựng nên các bằng chứng trong tương lai có thể dựa vào phép toán đã được kiểm tra thay vì bắt đầu lại từ đầu. Terence Tao, nhà toán học UCLA và người đoạt Huy chương Fields, đã giải thích trường hợp tổng quát một cách đơn giản hơn: “Bạn càng có nhiều bằng chứng chính thức thì bạn càng có thể tạo ra nhiều bằng chứng chính thức hơn”.
Các nhà toán học không phải là đối tượng độc giả duy nhất của Axiom. Các nhà phát triển từ lâu đã phải vật lộn để đảm bảo rằng mã của họ không có lỗi và lỗ hổng bảo mật. Vấn đề đó càng gia tăng khi các tác nhân AI viết nhiều mã hơn cho thế giới.
Axiom đang đặt cược rằng phần mềm của tương lai sẽ cần phải dựa trên nền tảng đã được xác minh, giống như cách mà Stacks hiện đang làm.
Swaminathan nói: “Chúng tôi tin rằng toán học là lĩnh vực mà 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 giao”. “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 đó. Chính thức hóa Lean của chúng tôi hiện là nền tảng mà các đại lý có thể xây dựng dựa trên đó.”
Cách các đặc vụ của Axiom xây dựng Ngăn xếp, làm việc song song và chọn nhiệm vụ của riêng họ, chính là cách Hong mong đợi phần lớn công việc trong tương lai của AI sẽ diễn ra. Cô lập luận rằng các tác nhân AI sẽ cần một khối kiến thức được xây dựng tốt, có thể tái sử dụng để tránh tạo ra sự cẩu thả.
Hong nói: “Bạn muốn (các đại lý) có một thư viện có thể tái sử dụng để họ xây dựng và tiếp tục phát triển vượt giới hạn”. “Nếu bạn thả dốc theo cách mà đó là những lựa chọn kỹ thuật tồi ngay từ đầu, thì họ sẽ rất khó phát triển ranh giới đó.”
Hong đủ tự tin vào cách tiếp cận đó để đưa ra lời thách thức. “Tôi công khai thách thức tất cả các công ty mã hóa nỗ lực chính thức hóa ở quy mô này.”
Khi bạn mua hàng thông qua các liên kết trong bài viết của chúng tôi, chúng tôi có thể kiếm được một khoản hoa hồng nhỏ. Điều này không ảnh hưởng đến tính độc lập biên tập của chúng tôi.