NEAR sử dụng DeepSeek để giải 600 bài toán toán học, đang làm cho việc kiểm toán mã trên chuỗi trở nên "giá rẻ như rau".

Tác giả: Trường An, Deep Tide TechFlow

Deep Tide Dẫn nhập: 672 đề toán của cuộc thi toán sinh viên hàng đầu Bắc Mỹ đã được đội ngũ NEAR AI giải toàn bộ bằng Agent. Tổng chi phí khoảng 111 đô la Mỹ, trung bình 0,17 đô la cho mỗi đề. Đội ngũ NEAR AI đã sử dụng mô hình mã nguồn mở của Trung Quốc là DeepSeek V4 để hoàn thành bài kiểm tra này. Đây không chỉ đơn giản là cuộc thi trí tuệ của các mô hình lớn, mà đằng sau hóa đơn tính toán là một ngành kinh doanh hạ tầng với tham vọng phổ cập hóa "kiểm chứng hình thức" hợp đồng thông minh vốn đắt đỏ.

Dữ liệu kiểm thử của một thư viện mã nguồn mở đã hé lộ chi phí cốt lõi của việc giải toán bằng mô hình lớn.

Gần đây, theo dữ liệu do đồng sáng lập NEAR Protocol là Alex Skidanov và trang chủ chính thức công bố, Agent của NEAR AI đã giải thành công tất cả 672 đề toán trong PutnamBench.

Để giải thích cho độc giả chưa quen thuộc, PutnamBench không phải là một bộ đề thông thường, mà là bộ kiểm thử được chuẩn hóa từ đề thi toán đại học hàng đầu Bắc Mỹ (William Lowell Putnam).

Nói một cách dễ hiểu, AI sẽ phải thực hiện suy luận logic toán học nghiêm ngặt để xem liệu có thể tự giải toán hay không. NEAR AI đã hoàn thành toàn bộ bài giải với chi phí khoảng 111,85 đô la Mỹ. Trung bình, chi phí cho mỗi đề là 0,17 đô la Mỹ.

So sánh với các phương án đạt điểm tối đa khác, hóa đơn chi phí của họ đắt hơn rất nhiều.

Theo dữ liệu do MSBIntel tổng hợp, sử dụng GPT-5.6 của OpenAI, chi phí trung bình cho mỗi câu hỏi lên tới 44,5 đô la Mỹ; còn với Claude Opus 5 của Anthropic thì mỗi câu cũng cần 3,52 đô la Mỹ.

Trong bài kiểm thử cụ thể này, NEAR đã chọn phương án DeepSeek V4, giúp giảm chi phí xuống còn 1/250 so với GPT-5.6.

Các public chain giải toán: Ý tại ngôn ngoại

Việc các team public chain nỗ lực giải toán không nhằm vào thị trường giáo dục.

Yêu cầu cốt lõi của kiểm thử PutnamBench là khả năng xác minh của máy móc: Kết quả AI tạo ra không chỉ là một đoạn văn, mà bắt buộc phải có mã chứng minh nghiêm ngặt viết bằng Lean 4 (một ngôn ngữ trợ lý chứng minh phổ biến).

Mã này không được phép có lỗi cú pháp, không được bỏ qua bước suy luận nào, phải được máy xác minh 100%. Điều này, trong lĩnh vực khoa học máy tính, gọi là kỹ thuật kiểm chứng hình thức (formal verification).

Liên hệ đến ngành crypto, hợp đồng thông minh đang quản lý khối vốn hàng tỷ, thậm chí hàng chục tỷ đô la. Cách kiểm toán truyền thống dựa vào con người dò lỗi, còn kiểm chứng hình thức thì dùng logic toán học chặt chẽ để chứng minh từng dòng mã không sai ở mọi trạng thái có thể xảy ra.

Lâu nay, nhược điểm chí tử của kiểm chứng hình thức là đắt và chậm. Nó đòi hỏi chuyên gia bảo mật hàng top và thời gian kéo dài, thường chỉ các dự án lớn nhiều vốn mới chịu nổi chi phí.

Bài kiểm thử của NEAR AI lần này đã chứng minh tính khả thi của việc sử dụng mô hình AI mã nguồn mở để tạo hàng loạt chứng minh toán học tin cậy, đồng thời xác nhận ưu thế về chi phí thấp.

Hạ tầng phổ cập cho bảo mật on-chain

Đưa ngưỡng kiểm chứng hình thức về vài nghìn đồng là bước triển khai thực tế mà NEAR đang hướng tới.

Hiện tại, bộ mã kết nối DeepSeek và Lean 4 này đã mở mã nguồn hoàn toàn. Hướng đi tiếp theo mà NEAR công bố rộng rãi là trực tiếp áp dụng công cụ giá rẻ này cho xác minh bảo mật của chính giao thức NEAR và các hợp đồng thông minh lõi.

Do đó, bạn có thể coi đây như một đợt chuyển giao công nghệ, hoặc nói đơn giản là các dự án đang thực sự làm việc, liên quan đến câu chuyện AI.

Nếu AI mã nguồn mở có thể liên tục tạo ra bằng chứng mã máy xác minh được, có nghĩa là các lập trình viên phổ thông và nhóm dự án nhỏ lẻ cũng có thể thực hiện kiểm chứng hình thức trước khi triển khai hợp đồng, chỉ tốn vài nghìn đồng để giảm nguy cơ hợp đồng thông minh gặp sự cố.

Tuy nhiên, khách quan mà nói, điều này không liên quan trực tiếp đến biến động giá ngắn hạn của token NEAR. Nhưng trong cạnh tranh hạ tầng nền tảng của hệ sinh thái public chain, việc bỏ ra vài chục xu để phòng ngừa rủi ro vẫn giá trị thương mại thực tế hơn nhiều so với tốn triệu đô la cho xử lý sự cố sau này.