🔬Vượt qua AI không chính thức - Carina Hong, Axiom Math

Năm 2025, công ty khởi nghiệp Axiom, mới thành lập được 7 tháng, đã giải quyết thành công toàn bộ 12 bài toán của kỳ thi Putnam (đạt 8/12 điểm trong thời gian quy định), một kỳ thi toán học danh giá dành cho sinh viên đại học. Thành tích 12/12 điểm này vượt trội so với các sinh viên đại học hàng đầu (110/120) và hệ thống AI gần nhất từng công bố kết quả (DeepSeek 103/120), mặc dù chưa rõ điểm số của con người và các hệ thống khác sẽ ra sao nếu có thêm thời gian. Tuy nhiên, kỳ thi Putnam nổi tiếng về độ khó, với điểm trung bình thường là 0 hoặc 1 điểm. Xét riêng, đây có vẻ là một thành tựu nhỏ của AI; một trong chuỗi dài các thành tích của hệ thống AI trong các cuộc thi cấp cao với con người, bắt đầu từ việc Deep Blue đánh bại Kasparov. Đến giữa năm 2026, Claude Code và Codex đang tạo ra tiếng vang lớn trên toàn cầu. Năm 2024, việc Anthropic đặt cược vào mã nguồn và doanh nghiệp dường như là một chiến lược thích hợp thực dụng hơn so với các mô hình tốt hơn và quy mô tiêu dùng khổng lồ của OpenAI. Ngày nay, quyết định dồn toàn lực của Amodei vào việc tăng tốc thông qua mã nguồn (bỏ qua hình ảnh và video) dường như là một tầm nhìn xa. Tuy nhiên, bất chấp đà phát triển của Anthropic, Giám đốc điều hành Axiom Carina Hong coi khả năng viết mã là một cột mốc cần thiết nhưng chưa đủ trên con đường đạt được AGI (Trí tuệ nhân tạo tổng quát). Mã nguồn có thể đẩy ranh giới không đồng đều đến mức siêu trí tuệ trong một số lĩnh vực ngoài mã hóa, nhưng có những khoảng trống đáng ngạc nhiên mà Carina tin rằng sẽ cản trở sự tiến bộ của AI. (Thống kê về các tiêu chuẩn toán học). Nút thắt không chính thức "AI đã được xác minh" nghe có vẻ giống như việc ăn bông cải xanh và nộp thuế, nhưng đối với Axiom, nó mang một ý nghĩa rất khác. Carina chia sẻ với chúng tôi: "Đối với tôi, việc xác minh là về việc mở rộng sự xuất sắc, tích lũy sự xuất sắc." Phải mất một thời gian để hiểu ý nghĩa của điều này (nghe giống như lời quảng cáo cho đến khi tôi hiểu ra). Carina đã đề cập đến nhà toán học huyền thoại Srinivasa Ramanujan (“Người đàn ông biết vô cực”) để minh họa cho luận điểm này. Khi G.H. Hardy cuối cùng đã thuyết phục Ramanujan chính thức chứng minh các định lý thay vì dựa vào trực giác (phi thường) của mình, điều đó được cho là đã cải thiện khả năng của ông. Điều này có lẽ là do việc chính thức chứng minh mọi thứ đã buộc Ramanujan phải trình bày chi tiết theo cách mở ra những hướng tư duy mới, v.v. Đây là cách “tổng hợp” trong toán học – xây dựng trên nền tảng vững chắc thay vì lung lay… còn được gọi là Tiên đề. Nhưng việc chính thức chứng minh mọi thứ cũng cho phép những người khác hưởng lợi từ trực giác của ông: các bằng chứng là cách truyền đạt một trực giác và thuyết phục người khác rằng trực giác đó là đúng. Đây là sự mở rộng (nhiều người sử dụng kết quả) và tổng hợp (mọi người có thể học hỏi và xây dựng dựa trên công việc của ông). Đây là nhận định cốt lõi giúp chúng ta hiểu được cách tiếp cận mà Axiom đang thực hiện. **Tạo ra đã được xác minh** Có hai cách mà AI đã được xác minh xuất hiện: trong quá trình đào tạo và trong quá trình suy luận. Nhưng một đoạn đi đường vòng nhanh: theo một cách gần đúng, “Xác minh hình thức” có nghĩa là sử dụng các trình kiểm tra kiểu (như đối với TypeScript, C++ hoặc Rust, nhưng có khả năng hơn) để xác minh các bằng chứng toán học được chỉ định tỉ mỉ bằng một ngôn ngữ như Lean2. Cần rất nhiều công sức để dịch một bằng chứng “không chính thức” (mặc dù hầu hết mọi người sẽ không gọi đó là “không chính thức”) thành một bằng chứng Lean3. Bản thân Axiom đã công bố công trình đột phá với AXLE – bộ công cụ ứng dụng Lean tương tác của họ để khám phá, xác thực và thao tác các bằng chứng toán học. Bạn có thể hình dung điều này sẽ hữu ích (rất nhiều) như thế nào trong Học tăng cường: thay vì dựa vào những phỏng đoán tốt nhất dựa trên thống kê (GRPO, RLHF, v.v.), bạn có thể chỉ cần xác minh bằng chứng là đúng bằng cách sử dụng trình xác minh Lean. Đây rõ ràng là một tín hiệu phần thưởng mạnh mẽ hơn nhiều, tương tự như việc biên dịch mã và kiểm tra nó (điều thường được thực hiện với RL trong mã hóa). Vấn đề: LLM (hiện tại) không giỏi trong việc chứng minh mọi thứ bằng Lean. Axiom xuất hiện: Mặc dù họ chưa chính thức báo cáo các con số chuẩn ngoài kết quả Putnam 12/12, Carina báo cáo rằng họ đã đạt được 99% (187/189) ProofGen rất ấn tượng trên chuẩn codegen của Verina. Chuẩn này là để tạo mã và bằng chứng về tính đúng đắn cho một loạt các vấn đề. Để so sánh, OpenAI o3 (lần chạy OpenAI cuối cùng được biết đến) đạt 4,9% trên chuẩn này. Dựa trên các số liệu chuẩn thưa thớt, khó có thể nói các phòng thí nghiệm tiên phong hiện đang hoạt động như thế nào ngoài các cột mốc IMO hàng năm, nhưng Carina gợi ý rằng họ vẫn chưa đào tạo để tạo ra các bằng chứng Lean trực tiếp, mà thay vào đó dựa vào các bằng chứng không chính thức. Thời gian sẽ trả lời liệu các phương pháp tiếp cận hiện tại của các phòng thí nghiệm tiên phong có thu hẹp được khoảng cách này hay không. Mở rộng quy mô và tích lũy Phép loại suy Ramanujan của Carina khá trực tiếp. Các chứng minh tốt hơn dẫn đến việc tạo Lean tốt hơn, từ đó dẫn đến RL tốt hơn. Tín hiệu mạnh hơn có nghĩa là hiệu quả lấy mẫu cao hơn và hiệu suất tối đa cao hơn. Tuyệt vời! Việc mở rộng quy mô cũng khá rõ ràng: một khi tôi đã chứng minh điều gì đó trong Lean, chất lượng đầu ra về cơ bản cao như thể nó đến từ con người, vì vậy tập dữ liệu huấn luyện chất lượng cao của tôi đã tăng lên theo cách mà một kho ngữ liệu triển khai không chính thức không thể làm được. Tôi có thể tin tưởng vào các chứng minh Lean của mình. Việc tích lũy cũng rõ ràng: giờ đây, tất cả các suy luận và huấn luyện trong tương lai đều có thể xây dựng dựa trên những chứng minh đó. Mặt khác, một mô hình chỉ được huấn luyện bằng các tín hiệu thống kê như GRPO trong quá trình RL thiếu hiệu quả lấy mẫu, hiệu suất tối đa và kho ngữ liệu tích lũy mà một hệ thống sử dụng xác minh hình thức được hưởng lợi. Mọi con đường đều dẫn đến xác minh Bỏ qua Broccoli và thuế, xác minh đã xuất hiện trong nhiều cuộc trò chuyện của chúng ta. Trong lĩnh vực hệ thống vật lý, hãy nhớ lại Applied Intuition: "Tôi nghĩ [khả năng xác minh] có lẽ là vấn đề khó khăn nhất hiện nay, bởi vì khi các mô hình ngày càng tốt hơn, việc tìm ra lỗi trên hệ thống có thể ngày càng khó hơn. Và vì vậy, vấn đề thực hiện đánh giá phù hợp để tìm ra những lỗi đó, vấn đề đó cũng ngày càng khó hơn khi các mô hình ngày càng tốt hơn." Trong vật lý lý thuyết, chúng ta nhớ lại Alex Lupsasca: "...bây giờ chúng ta đang ở trong chế độ mà bạn có thể chỉ cần có ChatGP