Một dự án được công bố gần đây tuyên bố cung cấp xác minh hình thức cho các mô hình học máy đã nhận được nhiều sự hoài nghi từ cộng đồng kỹ thuật. Dự án Xác minh hình thức cho mô hình học máy trong Lean tự giới thiệu là một khung làm việc để chứng minh các thuộc tính như tính mạnh mẽ, công bằng và khả năng giải thích của các mô hình ML bằng cách sử dụng trình chứng minh định lý Lean 4.
Dự án tự giới thiệu như một giải pháp toàn diện với các tính năng bao gồm thư viện Lean với các định nghĩa hình thức cho nhiều kiến trúc mạng nơ-ron khác nhau, một trình chuyển đổi mô hình để chuyển các mô hình đã được huấn luyện thành mã Lean, và một giao diện web để trực quan hóa và quản lý chứng minh. Tuy nhiên, các chuyên gia trong lĩnh vực này đã nêu lên những lo ngại đáng kể về cả tính khả thi và tính xác thực của các tuyên bố.
Hạn chế kỹ thuật và hứa hẹn quá mức
Các thành viên cộng đồng có chuyên môn về xác minh hình thức đã chỉ ra những hạn chế cơ bản trong phương pháp tiếp cận này. Xác minh hình thức các mô hình ML phức tạp phải đối mặt với những thách thức vốn có mà dự án dường như bỏ qua. Việc chứng minh các thuộc tính có ý nghĩa về mạng nơ-ron nổi tiếng là khó khăn, đặc biệt là đối với các ứng dụng thực tế.
Điều này dường như vô nghĩa... phần thực sự khó khăn tất nhiên là các chứng minh, điều mà họ dường như không giải quyết được. Các định lý kiểu mô hình X luôn làm điều mong muốn này hầu như luôn sai (vì đó là một mô hình không chính xác), và các định lý kiểu mô hình X luôn làm điều mong muốn này Y% thời gian dường như cực kỳ khó để chứng minh.
Các ví dụ trong kho lưu trữ đã bị chỉ trích vì quá đơn giản và không đại diện cho những thách thức xác minh trong thực tế. Một người bình luận lưu ý rằng ví dụ về tính công bằng chỉ chứng minh rằng một bộ phân loại luôn trả về kết quả có sẽ có tỷ lệ phần trăm phân loại giống nhau trên tất cả các nhóm dân số—một kết quả toán học tầm thường không có ý nghĩa thực tiễn.
Câu hỏi về tính xác thực
Nhiều người bình luận đã nêu lên lo ngại về tính xác thực của chính dự án. Mã Lean trong kho lưu trữ được mô tả như một sự pha trộn do AI tạo ra giữa Lean 3 và 4 mà có thể không biên dịch đúng. Việc thiếu các công trình khoa học được trích dẫn hoặc các bài báo nghiên cứu liên quan càng làm giảm độ tin cậy của dự án.
Một thành viên cộng đồng bày tỏ sự ngạc nhiên rằng dự án đã lên trang đầu của Hacker News mặc dù dường như chứa đầy các phần do AI tạo ra và những lời hứa hẹn thay vì nội dung thực chất. Sự thiếu vắng nền tảng khoa học đặc biệt đáng lo ngại khi xét đến độ phức tạp của lĩnh vực vấn đề.
Những vấn đề chính được nêu ra bởi cộng đồng:
- Lo ngại về chất lượng mã: Được mô tả là "sự pha trộn giữa Lean 3 và 4 được tạo bởi AI" có khả năng không biên dịch được
- Chứng minh hạn chế: Các ví dụ chỉ chứng minh các thuộc tính đơn giản (ví dụ: một bộ phân loại luôn trả về "có" sẽ có tỷ lệ phân loại 100% cho tất cả các nhóm)
- Thiếu nền tảng khoa học: Không trích dẫn các bài báo nghiên cứu hoặc khung lý thuyết
- Thách thức chưa được giải quyết:
- Xử lý các yếu tố ngẫu nhiên trong AI tạo sinh
- Định nghĩa các thước đo khách quan cho các khái niệm như "công bằng"
- Chứng minh các thuộc tính có ý nghĩa về mạng nơ-ron phức tạp
Các phương pháp thay thế được đề cập:
- ANSR của DARPA (Assured Neuro-Symbolic Reasoning)
- TIAMAT của DARPA (Transfer from Imprecise Models for Assured Tactical Autonomy)
Thách thức cơ bản trong xác minh ML
Cuộc thảo luận nêu bật một số thách thức cơ bản trong việc xác minh hình thức các mô hình ML mà dự án không giải quyết đầy đủ. Đối với các mô hình ngẫu nhiên—bao gồm hầu hết các hệ thống AI tạo sinh—việc xác minh trở nên phức tạp hơn. Như một người bình luận đã hỏi, Họ xử lý các mô hình có yếu tố ngẫu nhiên như thế nào? Không chắc làm thế nào để chứng minh việc lấy mẫu.
Ngay cả việc xác định những thuộc tính nào cần được xác minh cũng đặt ra những thách thức đáng kể. Các khái niệm như tính công bằng vốn mơ hồ và khó định nghĩa một cách khách quan trong các thuật ngữ toán học. Trong khi đó, việc chứng minh rằng một mô hình ngôn ngữ không đưa ra các phát biểu sai dường như là một vấn đề không thể giải quyết được.
Mặc dù có sự hoài nghi xung quanh dự án cụ thể này, cộng đồng vẫn nhận thấy tầm quan trọng của công việc theo hướng này. Các phương pháp tiếp cận thay thế được đề cập bao gồm các chương trình ANSR (Assured Neuro-Symbolic Reasoning) và TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy) của DARPA, đang giải quyết các thách thức liên quan đến xác minh AI với nền tảng khoa học nghiêm túc hơn.
Cuộc thảo luận này nhắc nhở về khoảng cách giữa những tuyên bố đầy tham vọng trong an toàn AI và thực tế kỹ thuật hiện tại. Mặc dù việc xác minh hình thức các thuộc tính đơn giản cho các mô hình ML cụ thể là khả thi, các khung xác minh toàn diện có thể xử lý các hệ thống học sâu hiện đại vẫn là một thách thức nghiên cứu mở chứ không phải là một vấn đề đã được giải quyết.
Tham khảo: Formal Verification of Machine Learning Models in Lean