Nhóm mạng lưới Ethereum đã xuất bản một loạt bài viết khách mời từ nhà phát triển chính của Vyper dưới bút danh big_tech_sux, tập trung vào vai trò của xác minh hình thức trong thời đại trí tuệ nhân tạo phát triển mạnh mẽ.
Tác giả khẳng định rằng sự tiến bộ của LLM đang khiến việc chứng minh tính đúng đắn của chương trình bằng toán học trở nên dễ tiếp cận hơn, và đối với các hợp đồng thông minh quản lý hàng tỷ đô la, xác minh hình thức đang dần trở thành một yêu cầu cần thiết.
AI thay đổi phương pháp kiểm tra phần mềm
Trong loạt bài viết, tác giả giải thích rằng xác minh hình thức là một phương pháp toán học cho phép chứng minh tính đúng đắn của một chương trình trong mọi tình huống thực thi có thể xảy ra, không chỉ giới hạn ở các trường hợp được bao phủ bởi kiểm thử.
Ví dụ, tác giả đưa ra hàm f(x) = x/2, mà người ta có thể chứng minh bằng toán học rằng kết quả sẽ không bao giờ vượt quá giá trị đầu vào.
Theo ông, phương pháp này có khả năng phát hiện những lỗi cực kỳ hiếm, hầu như không thể tìm thấy bằng kiểm thử thông thường.
"Xác minh hình thức có thể phát hiện một trường hợp trong một triệu tỷ, trường hợp đó sẽ không bao giờ xuất hiện trong quá trình kiểm thử, nhưng chính nó có thể dẫn đến một sự cố thảm khốc", tác giả nhấn mạnh.
Tuy nhiên, ông cũng thừa nhận rằng cho đến gần đây, việc áp dụng phương pháp này đòi hỏi làm việc với các nhóm chuyên gia lớn, những người tạo ra các mô hình toán học của chương trình và thực hiện các phép chứng minh phức tạp.
Theo nhận định của nhà phát triển, các LLM hiện đại đang đơn giản hóa đáng kể quá trình này khi tiến gần hơn đến AGI.
Đồng thời, tác giả nhấn mạnh rằng ngay cả với sự hỗ trợ của AI, xác minh hình thức vẫn là một quá trình phức tạp và tiêu tốn nhiều tài nguyên. Cụ thể, việc chuyển đổi mã nguồn sang mô hình hình thức có thể chứa những sai sót ảnh hưởng đến độ tin cậy của kết quả.
Sự phát triển của AI làm thay đổi sự cân bằng giữa tấn công và phòng thủ
Trong bài viết, tác giả lưu ý rằng sự phát triển của trí tuệ nhân tạo đồng thời nâng cao hiệu quả của cả những người bảo vệ lẫn kẻ tấn công.
Tác giả nhắc lại một trường hợp khi một mô hình OpenAI chưa được phát hành đã có thể tìm thấy các lỗ hổng zero-day cho phép vượt qua nhiều lớp bảo vệ.
Trong bối cảnh đó, xác minh hình thức, theo tác giả, cho phép chuyển lợi thế sang phía những người bảo vệ.
"Trong khi kẻ tấn công chỉ cần tìm một chuỗi dữ liệu đầu vào để xâm phạm hệ thống, những người bảo vệ có thể sử dụng xác minh hình thức để chứng minh khả năng chống chịu của nó trước mọi dữ liệu đầu vào có thể xảy ra", ông nhấn mạnh.
Chính vì lý do này, đối với phần mềm quan trọng, đặc biệt là các hợp đồng thông minh quản lý hàng tỷ đô la tài sản của người dùng, xác minh hình thức đang trở thành "không phải là một lựa chọn, mà là một tiền đề cần thiết".
Điều đáng lưu ý là điều này tiếp tục cuộc thảo luận mà đồng sáng lập Ethereum, Vitalik Buterin, đã khởi xướng trước đó về việc sử dụng AI để xác minh hình thức mã nguồn.
