Việc phát hành ProofOfThought , một hệ thống kết hợp các mô hình ngôn ngữ lớn với chứng minh định lý Z3 cho lý luận hình thức, đã châm ngòi cho một cuộc thảo luận sôi nổi trong cộng đồng AI về bản chất của lý luận máy móc và hiệu quả của các phương pháp tiếp cận lai trong trí tuệ nhân tạo.
ProofOfThought đại diện cho một nỗ lực nhằm thu hẹp khoảng cách giữa bản chất mờ nhạt, xác suất của LLM và độ chính xác cứng nhắc của các hệ thống logic hình thức. Dự án cho phép các nhà phát triển truy vấn các mô hình ngôn ngữ cho các tác vụ lý luận phức tạp trong khi sử dụng các công cụ chứng minh định lý toán học để xác minh tính nhất quán logic của kết quả.
Triển vọng và cạm bẫy của các hệ thống AI lai
Các cuộc thảo luận trong cộng đồng cho thấy cả sự phấn khích và hoài nghi về việc kết hợp các mô hình ngôn ngữ thống kê với các công cụ xác minh hình thức. Một số nhà phát triển đã chia sẻ những trải nghiệm tích cực với các phương pháp tương tự, đặc biệt khi sử dụng LLM để tạo mã cho các gói tính toán ký hiệu như SymPy hoặc Prolog . Những hệ thống lai này tận dụng khả năng hiểu ngôn ngữ tự nhiên của LLM trong khi dựa vào các công cụ toán học xác định cho tính toán thực tế.
Tuy nhiên, kết quả đánh giá của chính dự án làm nổi bật những thách thức đáng kể. Hệ thống cho thấy tỷ lệ dương tính giả đáng lo ngại là 51% trên các bài kiểm tra logic, cho thấy rằng LLM gặp khó khăn trong việc dịch chính xác các truy vấn ngôn ngữ tự nhiên thành các biểu diễn logic hình thức. Khoảng cách tự động hóa hình thức này đại diện cho một thách thức cơ bản trong việc kết nối lý luận của con người và logic máy móc.
SymPy: Một thư viện Python cho toán học ký hiệu có thể thực hiện các thao tác đại số, tính toán vi tích phân và giải phương trình Z3: Một công cụ chứng minh định lý được phát triển bởi Microsoft Research có thể giải quyết các ràng buộc logic và toán học phức tạp
Chỉ số Hiệu suất ProofOfThought
| Chỉ số | Giá trị | Ghi chú |
|---|---|---|
| Tỷ lệ Dương tính Giả | 51% | Trên các bài kiểm tra logic với GPT-4o |
| Đảm bảo Tính chính xác | 99%+ | Trong triển khai thương mại AWS |
| Lớp Kiến trúc | 2 | API cấp cao và DSL cấp thấp |
Yêu cầu Cài đặt
- z3-solver
- openai
- scikit-learn
- numpy
- Môi trường Python
Câu hỏi cơ bản về lý luận máy móc
Dự án đã làm bùng phát lại các cuộc tranh luận triết học về việc liệu LLM có thể thực sự lý luận hay chỉ mô phỏng lý luận thông qua việc khớp mẫu. Những người chỉ trích cho rằng các mô hình ngôn ngữ thống kê thiếu các ràng buộc logic thực sự trong quá trình tạo sinh của chúng, khiến chúng về cơ bản không phù hợp cho các tác vụ lý luận hình thức.
LLM là các mô hình ngôn ngữ thống kê chứ không phải công cụ lý luận. Tôi thấy việc tạo các chương trình logic, và cụ thể là mã nguồn Prolog , hoạt động cực kỳ tốt, có thể vì Prolog được giới thiệu cho xử lý ngôn ngữ tự nhiên ký hiệu.
Quan điểm này cho rằng trong khi LLM có thể xuất sắc trong việc tạo mã trong các ngôn ngữ lập trình logic do sự trùng lặp dữ liệu huấn luyện, chúng không tham gia vào lý luận logic thực tế. Bước xác minh hình thức trở nên ít liên quan đến việc đảm bảo tính chính xác và nhiều hơn về việc phân loại liệu đầu ra của LLM có tình cờ hợp lý về mặt logic hay không.
Thách thức triển khai kỹ thuật
Các nhà phát triển đã lưu ý những vấn đề thực tế với việc triển khai hiện tại, bao gồm khó khăn trong việc phân tích các đầu ra ngôn ngữ chuyên dụng phức tạp và nhu cầu giám sát thủ công các biểu diễn hình thức được tạo ra. Việc hệ thống dựa vào các phương pháp API cũ thay vì các tính năng đầu ra có cấu trúc hiện đại cũng đã thu hút sự chỉ trích từ các chuyên gia quen thuộc với khả năng LLM hiện tại.
Sự phát triển của dự án hướng tới việc sử dụng cú pháp SMT (Satisfiability Modulo Theories) trong nghiên cứu tiếp theo cho thấy những nỗ lực đang diễn ra để giải quyết những hạn chế kỹ thuật này. Tuy nhiên, thách thức cốt lõi vẫn còn: đảm bảo rằng LLM có thể dịch một cách đáng tin cậy lý luận ngôn ngữ tự nhiên thành các câu logic hình thức.
SMT: Một khung làm việc để kiểm tra tính thỏa mãn của các công thức logic đối với các kết hợp của các lý thuyết nền
Ứng dụng thực tế và hướng phát triển tương lai
Bất chấp những thách thức, một số tổ chức đang khám phá các phương pháp tương tự cho các ứng dụng thực tế. Các công ty đang thử nghiệm việc sử dụng xác minh hình thức để xác thực nội dung do AI tạo ra so với các tài liệu chính sách và yêu cầu tuân thủ, với một số tuyên bố đảm bảo độ chính xác trên 99% trong các lĩnh vực cụ thể.
Cuộc thảo luận cho thấy sự nhận thức ngày càng tăng rằng các phương pháp lai có thể cần thiết cho các hệ thống AI đáng tin cậy, ngay cả khi các triển khai hiện tại đối mặt với những hạn chế đáng kể. Khi các mô hình ngôn ngữ tiếp tục cải thiện, khoảng cách giữa lý luận ngôn ngữ tự nhiên và biểu diễn logic hình thức có thể thu hẹp, làm cho các hệ thống như vậy trở nên thực tế hơn cho việc triển khai trong thế giới thực.
Dự án ProofOfThought , trong khi làm nổi bật những hạn chế hiện tại, đại diện cho một bước quan trọng hướng tới các hệ thống lý luận AI đáng tin cậy hơn. Sự tiếp nhận trái chiều của cộng đồng nhấn mạnh cả tiềm năng và những thách thức đáng kể vẫn còn trong việc tạo ra trí tuệ nhân tạo thực sự đáng tin cậy.
Tham khảo: ProofOfThought