Vitalik Buterin đề xuất ngôn ngữ lập trình giúp con người đọc được bằng chứng AI

Vitalik đề xuất ngôn ngữ mới cho kỷ nguyên bằng chứng AI

Đồng sáng lập Ethereum Vitalik Buterin vừa đề xuất một ngôn ngữ lập trình bậc cao mới, được thiết kế riêng để biên dịch sang Lean hoặc HOL — hai công cụ hỗ trợ chứng minh hình thức (proof assistant) phổ biến. Mục tiêu cốt lõi là giúp con người có thể đọc và hiểu các định nghĩa, định lý một cách thuận tiện nhất, trong bối cảnh AI ngày càng tạo ra nhiều khối bằng chứng toán học tự động với tốc độ vượt xa khả năng viết tay của con người.

Trên mạng xã hội X, Buterin viết: "Một loại ngôn ngữ lập trình bậc cao mới thực sự đáng để thử nghiệm — đó là ngôn ngữ được biên dịch sang Lean (hoặc HOL...) với mục tiêu tối thượng là giúp con người đọc các định nghĩa và định lý dễ dàng nhất có thể. Không phải bản thân các bước chứng minh."

Tách biệt bước chứng minh và tuyên bố có thể đọc được

Buterin lập luận rằng các bước nội tại bên trong một bằng chứng chỉ cần đáp ứng một yêu cầu duy nhất: tính đúng đắn toán học. Người đọc không cần trực tiếp kiểm tra từng bước máy móc đó. Trong khi đó, định nghĩa và định lý lại khác — đây là phần mà con người đọc để hiểu một phần mềm thực sự đảm bảo điều gì.

Logic này đã được Buterin khai thác trong một bài blog hồi tháng 5/2026, nơi ông mô tả cách một bằng chứng toán học có thể chứng minh rằng đoạn mã cấp thấp hiệu quả khớp với một đặc tả riêng biệt, dễ đọc — từ đó một lần kiểm toán duy nhất có thể bao phủ cả hai phiên bản.

Kết nối với lộ trình Lean Ethereum và ZK-EVM

Thời điểm Buterin đưa ra đề xuất cũng trùng với lộ trình Lean Ethereum — nỗ lực tái kiến trúc Ethereum bằng các phương pháp xác minh hình thức. Song song đó, các nhà nghiên cứu đang xây dựng một ZK-EVM được xác minh hình thức, tức phiên bản máy ảo EVM có khả năng chứng minh zero-knowledge, sử dụng các phương pháp tương tự.

Một dự án ví dụ được nhắc đến là evm-asm — một triển khai EVM được xác minh đối chiếu với một tài liệu tham chiếu dễ đọc.

AI viết bằng chứng, con người kiểm tra tuyên bố

Các mô hình ngôn ngữ lớn hiện đã có khả năng viết các bằng chứng Lean có thể sử dụng được. Buterin đề cập đến Claude, DeepSeek R1 Pro và Leanstral — một mô hình nhỏ hơn được tinh chỉnh riêng cho Lean — như những công cụ đang hoạt động hiệu quả trong lĩnh vực này.

Khả năng này cũng gợi nhớ đến thử thách AI mà Buterin đặt ra gần đây, khi các người kiểm tra đã giải quyết xong trong vòng vài giờ.

Trong bối cảnh các nhà nghiên cứu bảo mật ghi nhận sự gia tăng mạnh của các cuộc tấn công khai thác có hỗ trợ AI trong năm nay, mã được xác minh hình thức nổi lên như một lớp phòng thủ tiềm năng. Một ngôn ngữ đặc tả thân thiện hơn sẽ cho phép các nhà phát triển kiểm toán các tuyên bố mà không cần lội qua toàn bộ bằng chứng bên dưới.

Chưa có nguyên mẫu, cộng đồng chờ đợi

Hiện tại, chưa có nguyên mẫu nào của ngôn ngữ mới được công bố, và Buterin cũng để ngỏ cú pháp cụ thể. Cộng đồng nhà phát triển có thể hội tụ về một tiêu chuẩn chung, hoặc phân tán thành nhiều phương ngữ không tương thích — lựa chọn đó sẽ ảnh hưởng đáng kể đến tốc độ triển khai mã được xác minh bằng AI vào các hệ thống thực tế.