Hacker News chia sẻ cuộc phỏng vấn về AI, Lean và tương lai của kiểm chứng hình thức
Một cuộc phỏng vấn với Leo de Moura, người tạo ra Lean, tập trung vào cách kết hợp mã do AI tạo với các chứng minh hình thức được máy kiểm tra. Lean vừa là ngôn ngữ lập trình vừa là công cụ chứng minh định lý: nhà phát triển có thể mô tả phần mềm phải làm gì, sau đó cung cấp một chứng minh để kernel nhỏ của Lean kiểm tra. De Moura cho rằng cách này có thể giải quyết bài toán niềm tin ngày càng lớn khi AI tạo ra nhiều mã hơn và hoạt động ngày càng tự chủ. Cuộc trò chuyện so sánh kiểm chứng hình thức với kiểm thử, vốn có thể tìm ra lỗi nhưng nhìn chung không thể chứng minh rằng không còn lỗi nào. Nội dung đề cập đến mã Rust và Lean do AI tạo, việc tự động chuyển các phát biểu toán học thành dạng hình thức, dự án Mathlib, các bộ kiểm tra chứng minh đã được xác minh, cùng một thử nghiệm chuyển thư viện nén zlib sang Lean với định lý cho biết giải nén sẽ khôi phục dữ liệu ban đầu. Hai bên cũng bàn về ngăn xếp phần mềm được xác minh, chính sách bảo mật cho tác tử AI và các ứng dụng tiềm năng trong tài chính, hóa học, kế toán, luật và vật lý lý thuyết. Trong thực tế, hướng tiếp cận này có thể đưa kỹ thuật phần mềm từ việc chủ yếu dựa vào duyệt mã và kiểm thử sang mô hình xác định trước hành vi mong muốn, rồi để AI tạo cả phần cài đặt lẫn chứng minh tương ứng.
Lập trình viên và nhóm xây dựng AI nên theo dõi Lean nếu muốn kiểm chứng chặt chẽ mã do AI tạo ra: hệ thống có thể được yêu cầu sinh cả mã nguồn lẫn chứng minh máy kiểm tra được. Tuy nhiên, cách tiếp cận này vẫn đòi hỏi viết đặc tả rõ ràng về phần mềm phải làm gì, thay vì chỉ dựa vào kiểm thử.
Đọc bài gốc