Việc giải quyết mọi vấn đề trong một trong những bài kiểm tra khó nhất của toán học thường tốn hàng chục nghìn đô la. NEAR AI vừa thực hiện điều đó với chi phí chỉ 111 đô la.
Vào ngày 6 tháng 9 năm 2026, đồng sáng lập NEAR Protocol, Alex Skidanov, thông báo rằng tác nhân Lean mã nguồn mở của dự án đã giải quyết tất cả 672 bài toán trong bộ tiêu chuẩn PutnamBench, được lấy từ Cuộc thi Toán học William Lowell Putnam. Tổng chi phí: 111 USD. Bản nộp rẻ thứ hai được biết đến tốn gấp 250 lần.
PutnamBench thực sự là gì và tại sao nó quan trọng
Cuộc thi Putnam là kỳ thi toán học đại học danh giá nhất ở Bắc Mỹ. Việc đạt điểm zero không phải là điều hiếm gặp, ngay cả với những sinh viên xuất sắc. Bài thi được thiết kế để khiến bạn gục ngã.
PutnamBench, được giới thiệu vào năm 2024, tiếp nối truyền thống khó khăn này và biến nó thành một bộ đánh giá chính thức cho các trình chứng minh định lý AI. Bộ chuẩn này chứa 672 bài toán được mã hóa bằng Lean 4, một ngôn ngữ trợ lý chứng minh yêu cầu các lập luận toán học phải được viết với độ chính xác có thể xác minh bằng máy móc. Một chứng minh thiếu chặt chẽ về mặt logic sẽ bị từ chối ngay lập tức, không có điểm bán phần.
Trước kết quả của NEAR AI, các tác nhân khi thử thách PutnamBench thường cần hàng ngàn lần gọi suy luận cho mỗi bài toán. Chi phí tính toán tăng nhanh, khiến tổng chi phí cho các lần chạy toàn bộ bộ kiểm tra nằm trong khoảng từ 10.000 đến 25.000 đô la Mỹ đối với các hệ thống hàng đầu.
Agent Lean của NEAR AI đã hoàn thành toàn bộ bộ 672 bài toán với chi phí 111 đô la.
Tại sao khoảng cách chi phí mới là câu chuyện thực sự
Với chi phí từ 10.000 đến 25.000 USD cho mỗi lần chạy đầy đủ, chỉ một số ít tổ chức mới có thể chi trả để lặp lại, thử nghiệm và cải thiện các đường ống chứng minh định lý của họ. Với chi phí 111 USD, tính toán này hoàn toàn đảo ngược.
Sự tiến bộ nhanh chóng trong kết quả PutnamBench giữa năm 2025 và 2026 đã được thúc đẩy bởi các quy trình agentic kết hợp các mô hình ngôn ngữ lớn với động cơ kiểm tra chứng minh của Lean. Cách tiếp cận của NEAR AI mở rộng mô hình này, đồng thời bổ sung một lớp hiệu quả mà cộng đồng benchmark chưa từng thấy trước đây.
NEAR AI đã đặt thành tựu này trong một tầm nhìn cơ sở hạ tầng rộng lớn hơn, tập trung vào cái mà họ gọi là IronClaw, một khung khổ hướng đến AI bảo mật và có thể xác minh. Khả năng xác minh hình thức phù hợp trực tiếp với khung này: nếu bạn có thể chứng minh một lập luận toán học là chính xác ở cấp độ máy, bạn đã có nền tảng cho các hệ thống AI mà đầu ra của chúng có thể được kiểm toán độc lập thay vì chỉ dựa vào niềm tin.
Quyết định của NEAR Protocol để mở nguồn agent Lean làm tăng thêm ý nghĩa. Các công cụ sở hữu độc quyền mang lại lợi thế chi phí 250x thường giữ nguyên tính độc quyền. Việc mở nguồn agent có nghĩa là phương pháp này có sẵn để kiểm tra, mở rộng và sử dụng bởi bất kỳ ai.