Axiom Math muốn ngăn chặn nội dung AI kém chất lượng xâm nhập toán học

Trí tuệ nhân tạo (AI) dường như đang liên tục giải quyết các bài toán mới mỗi tuần. Chỉ riêng trong tháng trước, OpenAI đã công bố 719 bản thảo tuyên bố tìm ra lời giải cho một số bài toán khó nhất trong lĩnh vực này. Dù vậy, ngay cả các quy trình kiểm tra bằng máy tính vẫn có thể xảy ra sai sót. Sau nhiều năm xuất hiện những nội dung AI kém chất lượng, việc đặt câu hỏi liệu toán học có phải là lĩnh vực tiếp theo bị ảnh hưởng hay không là hoàn toàn có cơ sở. AxiomMath đặt cược rằng toán học có thể tránh được nguy cơ đó, không phải bằng cách giảm tốc độ phát triển, mà bằng việc xác lập một nền tảng vững chắc hơn. Công ty khởi nghiệp được định giá 1,6 tỷ USD này đặt mục tiêu xây dựng một hệ thống nền tảng đã qua kiểm chứng để các tác tử AI (AI agents) có thể dựa vào đó viết phần mềm và từng bước phục vụ nghiên cứu khoa học. Hôm thứ Tư, công ty thông báo đã hoàn tất việc kiểm chứng hình thức đối với Stacks Project, một trong những kho tàng công trình toán học đồ sộ nhất từng được con người xây dựng. Giới toán học luôn dành cho Stacks Project sự đánh giá đặc biệt. Nhà toán học Peter Woit thuộc Đại học Columbia từng khẳng định “hầu như không có công trình nào sánh kịp”, đồng thời so sánh dự án này với “bộ sách Bourbaki nổi tiếng” — công trình từng tái thiết toán học từ nền móng vào thế kỷ 20. Đồng nghiệp của ông Woit tại Đại học Columbia, ông Johan de Jong, đã khởi xướng Stacks Project vào năm 2005 dưới dạng tài liệu tham khảo nguồn mở. Kể từ đó, giới toán học đã liên tục đóng góp, phát triển các kết quả từ đại số bậc đại học cho tới những lý thuyết chuyên sâu nhất trong các phân ngành đại số, hình học và lý thuyết số. Hệ thống các tác tử AI của công ty đã chuyển đổi khoảng 7.654 trang tài liệu của thư viện này thành khoảng 16 triệu dòng mã nguồn được kiểm tra bằng máy tính. Hình thức hóa toán học là phương thức bảo đảm tính chuẩn xác của cấu trúc nền tảng. Các nhà toán học viết lại các phép chứng minh dưới dạng mã lệnh bằng ngôn ngữ lập trình Lean, sau đó một phần mềm hỗ trợ chứng minh (proof assistant) sẽ kiểm tra từng dòng mã. Nếu phép chứng minh được thông qua, giới toán học có thể tin cậy vào tính logic tuyệt đối của công trình. Các kỹ sư cũng áp dụng phương pháp tương tự, gọi là kiểm chứng hình thức (formal verification), để xác thực hoạt động của các thiết kế vi mạch, trong khi các nhà nghiên cứu tại Pháp từng ứng dụng phương pháp này để rà soát lỗi trong phần mềm tính toán trợ cấp gia đình. Đối với một thư viện quy mô như Stacks Project, việc kiểm tra từng định lý đơn lẻ chỉ là một phần của công việc. Các định lý và định nghĩa trong Stacks có tính liên kết chặt chẽ và kế thừa lẫn nhau. Tương tự như một cây phả hệ, nhiều kết quả trong Stacks đều bắt nguồn từ những nền tảng được xây dựng trước đó. Tính liên kết phức tạp này ban đầu khiến Axiom hoài nghi về tính khả thi của dự án. Đội ngũ kỹ thuật phải bảo đảm tính toàn vẹn của mọi mối liên kết xuyên suốt khoảng 16 triệu dòng mã Lean. “Những thứ to lớn và những cấu trúc tinh vi trong cuộc sống thường khó dung hòa với nhau”, bà Carina Hong, Giám đốc điều hành Axiom, chia sẻ với TechCrunch. “Stacks là tập hợp các kết quả toán học đóng vai trò nền tảng. Các định lý đòi hỏi tính nhất quán và không được mâu thuẫn; các định nghĩa cũng không được triệt tiêu lẫn nhau”. Nữ Giám đốc điều hành 25 tuổi này đã gác lại chương trình nghiên cứu sinh tiến sĩ toán học tại Đại học Stanford để sáng lập công ty vào tháng 3/2025. Cũng trong tháng Ba, Axiom đã huy động thành công 200 triệu USD trong vòng gọi vốn Series A do Menlo Ventures dẫn đầu. “Chúng tôi từng băn khoăn liệu phương pháp lập trình tự do (vibe coding) có thể bảo toàn được vẻ đẹp của Stacks hay không”, bà Hong nhận định. Để hiện thực hóa dự án, nhóm nghiên cứu đã thiết lập một cấu trúc phân cấp linh hoạt cho các tác tử và cho phép chúng vận hành song song. Ông Ashvin Swaminathan, thành viên đội ngũ kỹ thuật của Axiom, cho biết: “Với Stacks, chúng tôi thiết lập một cấu trúc phân tầng, song không áp đặt tuyệt đối hành vi của từng tác tử riêng lẻ. Các tác tử tự tìm kiếm nhiệm vụ và xác định những hạng mục công việc có thể phối hợp xử lý song song”. Axiom cũng tự huấn luyện các mô hình của mình để đạt hiệu quả cao trong môn toán. Bà Hong cho biết đây là hướng tiếp cận mà phần lớn các công ty khởi nghiệp trong lĩnh vực kiểm định khác chưa áp dụng. Ban đầu, đội ngũ phát triển dựa vào một chuyên gia Lean nội bộ để rèn luyện cho các tác tử (agent) khả năng thẩm định tương tự con người. Theo bà Hong, qua thời gian, các tác tử này đã tự hình thành được năng lực đánh giá độc lập. Kết quả này góp phần khỏa lấp một trong những khoảng trống lớn nhất của toán học hình thức hóa. “Khi nhìn vào những gì đã được hình thức hóa trong toán học, tồn tại một lỗ hổng rất lớn. Và lỗ hổng đó bao trùm cả hình học đại số”, ông Swaminathan nhận định. Ông Swaminathan cho biết, từ trước đến nay, các nhà nghiên cứu muốn kiểm định những công trình mới về hình học đại số bằng Lean hầu như không có cơ sở nền tảng. “Hiện tại, họ đã có thể làm được điều đó”. Axiom khẳng định mỗi kết quả được kiểm định sẽ trở thành một khối nền tảng, giúp các phép chứng minh trong tương lai có thể dựa vào những công thức toán học đã được xác minh thay vì phải bắt đầu lại từ đầu. Giáo sư Terence Tao, nhà toán học thuộc Đại học UCLA từng đoạt Huy chương Fields, đã khái quát hóa vấn đề một cách giản lược: “Càng có nhiều phép chứng minh được hình thức hóa, chúng ta càng có thể tạo ra nhiều phép chứng minh được hình thức hóa hơn”. Các nhà toán học không phải là đối tượng duy nhất mà Axiom hướng tới. Từ lâu, các nhà phát triển phần mềm đã gặp nhiều khó khăn trong việc bảo đảm mã nguồn không có lỗi (bug) và lỗ hổng bảo mật. Vấn đề này ngày càng trở nên nghiêm trọng khi các tác tử AI đang trực tiếp viết ngày càng nhiều mã nguồn trên toàn cầu. Axiom đặt cược rằng các phần mềm trong tương lai sẽ cần được xây dựng trên những nền tảng đã qua kiểm định, tương tự như cách Stacks đang vận hành. “Chúng tôi tin rằng toán học là lĩnh vực khởi đầu để xây dựng những công cụ này, đồng thời là một kỹ năng có thể chuyển giao”, ông Swaminathan phát biểu. “Các tác tử có thể đọc mã nguồn của chúng tôi, hiểu và xây dựng cơ sở hạ tầng mới dựa trên nền tảng đó. Quy trình hình thức hóa bằng Lean của chúng tôi hiện là cơ sở để các tác tử phát triển tiếp”. Cách các tác tử của Axiom xây dựng dự án Stacks—hoạt động song song và tự lựa chọn nhiệm vụ—là mô hình mà bà Hong kỳ vọng sẽ diễn ra trong phần lớn các hoạt động tương lai của AI. Bà lập luận rằng các tác tử AI sẽ cần một hệ thống tri thức hoàn chỉnh và có khả năng tái sử dụng để tránh tạo ra các sản phẩm kém chất lượng. “Cần cung cấp cho [các tác tử] một thư viện có thể tái sử dụng để phát triển và tiếp tục mở rộng các giới hạn”, bà Hong nhấn mạnh. “Nếu ban đầu đưa vào những sản phẩm kém chất lượng xuất phát từ các quyết định kỹ thuật sai lầm, các tác tử sẽ rất khó có thể mở rộng giới hạn đó”. Bà Hong hoàn toàn tự tin vào phương pháp tiếp cận này và đư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 lập trình thực hiện công tác hình thức hóa ở quy mô này”. Chủ đề agents, AI, AI, toán học, Startups, TC Khi độc giả mua hàng qua các liên kết trong bài viết, chúng tôi có thể nhận được một khoản hoa hồng nhỏ. Điều này không ảnh hưởng đến tính độc lập của hoạt động biên tập. Aditya Mehta Biên tập viên cộng tác (Editorial Fellow) Aditya Mehta là phóng viên phụ trách mảng AI tại TechCrunch. Hoạt động tác nghiệp của phóng viên nhận được sự hỗ trợ từ Tarbell