Vitalik Buterin đề xuất ngôn ngữ giúp các bằng chứng AI dễ hiểu

Đồng sáng lập Ethereum, Vitalik Buterin, đã đề xuất một ngôn ngữ lập trình mới có thể biên dịch trực tiếp sang Lean hoặc HOL – những phần mềm dùng để kiểm chứng toán học tự động.

Ý tưởng này nhằm giải quyết một vấn đề cụ thể: cách con người đọc và hiểu kết quả do AI tạo ra. Trí tuệ nhân tạo ngày càng có khả năng sản xuất hàng loạt các chứng minh tự động, thậm chí nhanh hơn rất nhiều so với nhóm người tự viết. Tuy nhiên, rất ít người có thể xác nhận nhanh chóng các chứng minh đó thực chất chứng minh được điều gì.

Một ngôn ngữ dành riêng cho những ai đọc chứng minh do AI tạo ra

Lean là một phần mềm hỗ trợ kiểm chứng, thường được các nhà toán học và kỹ sư sử dụng để viết các chứng minh mà máy tính có thể kiểm tra từng bước. Các nhà nghiên cứu Ethereum hiện cũng dùng Lean để kiểm tra mã hóa mật mã và thuật toán đồng thuận. Dù phần mềm hỗ trợ kiểm chứng đã có mặt gần 60 năm, lĩnh vực này vẫn khá mới mẻ với phần lớn mọi người.

A new type of "high-level programming language" that seems really worth trying to make, is a language that gets compiled to Lean (or HOL, or…) that is specifically about making it as friendly as possible for a human to read definitions and theorems.Not the proofs – as all…

— vitalik.eth (@VitalikButerin) July 21, 2026

Trong bài đăng của mình, Buterin cho rằng, các bước bên trong một chứng minh thực chất chỉ có một yêu cầu duy nhất: đó là sự chính xác về mặt toán học. Người đọc sẽ không cần phải xem xét trực tiếp phần này. Riêng các định nghĩa và định lý lại khác, vì đây là phần con người đọc để hiểu về cam kết thực tế của phần mềm.

Buterin cũng bàn thêm về vấn đề này trong một bài blog vào tháng 05/2026. Tại đây, một chứng minh toán học chỉ rằng mã thấp cấp hiệu quả thực tế khớp với một bản đặc tả dễ hiểu hơn, nhờ đó mà chỉ một lần kiểm toán thôi đã đủ để xác minh cho cả hai phiên bản mã nguồn này.

Đề xuất này cũng khá phù hợp với nỗ lực làm lại Ethereum, còn gọi là lộ trình Lean Ethereum. Hiện tại, các nhà nghiên cứu cũng đang xây dựng ZK-EVM được kiểm chứng hình thức – phiên bản máy ảo Ethereum (EVM) có thể chứng minh bằng zero-knowledge, với các phương pháp tương tự.

AI tạo chứng minh, con người kiểm tra cam kết

Các mô hình ngôn ngữ lớn hiện nay đã có thể viết các chứng minh Lean usable. Buterin nêu tên Claude và Deepseek 4 Pro là các công cụ mạnh mẽ, cùng với Leanstral – một mô hình nhỏ hơn, huấn luyện riêng cho Lean. Một dự án điển hình là evm-asm, ứng dụng EVM được kiểm chứng so với bản tham khảo dễ đọc. Khả năng này tương tự kỹ năng tư duy logic của các lập trình viên từng thể hiện tại thử thách AI do Buterin khởi xướng. Đáng chú ý, các tester đã giải trong vài giờ đồng hồ.

Tuy vậy, tầm quan trọng của đề xuất còn vượt ngoài yếu tố tiện lợi. Các nhà nghiên cứu bảo mật ghi nhận số vụ tấn công mạng liên quan đến AI đang tăng mạnh trong năm nay (báo cáo). Việc mã hóa được kiểm chứng hình thức là một lớp bảo vệ tốt trước xu hướng này. Nếu có ngôn ngữ đặc tả thân thiện hơn, lập trình viên có thể kiểm toán các cam kết mà không mất thời gian kiểm tra toàn bộ chứng minh xung quanh.

Ngoài phạm vi nghiên cứu của Ethereum

Buterin vẫn đang tiếp tục thử nghiệm ý tưởng này trong thực tế, mới đây ông đã giới thiệu bảng quảng cáo ẩn danh sử dụng zero-knowledge proofs. Bản demo này cho thấy những lý thuyết kiểm chứng hình thức hoàn toàn có thể áp dụng vào sản phẩm thực tế. Đồng thời, các nhà nghiên cứu cũng dần dùng Lean để kiểm chứng khách hàng đồng thuận sớm, giúp phát hiện lỗi hiệu quả hơn.

Dù vậy, hướng đi này vẫn lặp lại một xu thế quen thuộc: tách biệt mã chạy nhanh và những cam kết dễ đọc, sau đó chứng minh hai phần này thực sự trùng khớp với nhau.

Hiện tại vẫn chưa có bản mẫu nào cho ngôn ngữ mới này và Buterin cũng chưa chốt cách viết cụ thể. Các lập trình viên có thể sẽ cùng nhau xây dựng một chuẩn chung, hoặc chấp nhận tồn tại nhiều biến thể khác nhau. Lựa chọn này sẽ ảnh hưởng trực tiếp đến tốc độ ứng dụng mã được AI kiểm chứng vào hệ thống thực tiễn.