Suốt sự nghiệp của tôi, Xác minh Hình thức (dùng các công cụ như TLA+, Coq, hoặc Lean) luôn là Chén Thánh của kỹ thuật phần mềm mà chẳng ai thực sự dùng. Trừ khi bạn đang xây dựng bộ điều khiển hàng không vũ trụ hoặc mật mã cấp thấp, sự đồng thuận của ngành luôn là việc viết các chứng minh toán học cho mã của bạn đơn giản là quá chậm và tốn kém đối với các SaaS doanh nghiệp tiêu chuẩn. Chúng ta chấp nhận các bài kiểm tra đơn vị, quy trình CI/CD, và đôi khi là phân tích sau sự cố.
Nhưng tôi đang nhìn vào sự chuyển động gần đây trong không gian cơ sở hạ tầng AI, và tôi nghĩ rằng phép tính đó sắp thay đổi một cách dữ dội.
Tin tức tuần trước là Yann LeCun đã huy động một vòng hạt giống KHỔNG LỒ trị giá $1 tỷ đô la. Số tiền đô la chỉ là con số. Điều thực sự thú vị là tiền đề kỹ thuật đằng sau công ty, Logical Intelligence. Họ hoàn toàn từ bỏ con đường LLM tự hồi quy (mà tất cả chúng ta đều biết là rất tệ trong logic chặt chẽ) và xây dựng các Mô hình Dựa trên Năng lượng (Energy-Based Models) đặc biệt để xuất ra mã đã được xác minh cho các hệ thống quan trọng.
Nếu một nền tảng thực sự quản lý để sử dụng AI để thu hẹp khoảng cách giữa các yêu cầu bằng tiếng Anh thông thường và các chứng minh toán học hình thức, vai trò của một Kỹ sư Cao cấp sẽ thay đổi hoàn toàn.
Thay vì viết chi tiết triển khai hoặc dọn dẹp ảo giác của Copilot, công việc chính của chúng ta có thể chuyển sang viết các đặc tả và ràng buộc siêu chặt chẽ. Chúng ta sẽ không xem xét mã mà AI viết; chúng ta sẽ xem xét bằng chứng rằng mã của AI đáp ứng các ràng buộc. Nó đưa chúng ta từ những người thợ thủ công phần mềm thành những nhà toán học hệ thống.
Nếu chúng ta đột nhiên có một công cụ AI tuyên bố rằng nó có thể “chứng minh toán học” một microservice sẽ không mất trạng thái trong quá trình phân vùng mạng, liệu văn hóa kỹ thuật của bạn có đủ khả năng để áp dụng nó không, hay ngành công nghiệp này quá nghiện “đi nhanh và phá vỡ mọi thứ”?
