Suy luận tự động

Trong khoa học máy tính, đặc biệt là trong biểu diễn tri thức và siêu logic học, lĩnh vực suy luận tự động (automated reasoning) được dành riêng cho việc hiểu các khía cạnh khác nhau của lý trí. Nghiên cứu về suy luận tự động giúp phát triển các chương trình máy tính cho phép máy tính suy luận hoàn toàn, hoặc gần như hoàn toàn tự động. Mặc dù suy luận tự động được coi là một phân ngành của trí tuệ nhân tạo, nó cũng có sự liên kết với khoa học máy tính lý thuyết và triết học.

Các phân ngành phát triển mạnh nhất của suy luận tự động là "chứng minh định lý tự động" hay "automated theorem proving" (và phân ngành kém tự động hơn nhưng thực tế hơn là "chứng minh định lý tương tác" hay "interactive theorem proving") và "kiểm tra chứng minh tự động" hay "automated proof checking" (được coi là suy luận chính xác đảm bảo theo các giả định cố định). Rất nhiều công trình cũng đã được thực hiện trong suy luận theo loại suy bằng cách sử dụng quy nạp và giả định.^[1]

Các chủ đề quan trọng khác bao gồm suy luận trong điều kiện bất định và suy luận phi đơn điệu. Một phần quan trọng của lĩnh vực bất định là lập luận, nơi các ràng buộc về tối thiểu hóa và tính nhất quán được áp dụng bên trên các phép suy luận tự động thông thường. Hệ thống OSCAR của John Pollock^[2] là một ví dụ về hệ thống lập luận tự động cụ thể hơn so với một hệ thống chứng minh định lý thông thường.

Các công cụ và kỹ thuật của suy luận tự động bao gồm logic cổ điển và các phép tính, logic mờ, suy luận Bayes, suy luận với entropy tối đa và nhiều kỹ thuật ngẫu nhiên không chính thức khác.

Những năm đầu

Sự phát triển của logic hình thức đóng vai trò lớn trong lĩnh vực suy luận tự động, và nó cũng dẫn đến sự phát triển của trí tuệ nhân tạo. Một chứng minh hình thức là một chứng minh mà mọi suy luận logic đều được kiểm tra lại với các tiên đề cơ bản của toán học. Tất cả các bước logic trung gian đều được cung cấp mà không ngoại lệ. Không có sự nhờ cậy vào trực giác, ngay cả khi việc chuyển từ trực giác sang logic là thường xuyên. Do đó, chứng minh hình thức này ít trực giác hơn và ít dễ mắc lỗi logic hơn.^[3]

Một số người coi cuộc họp mùa hè Cornell năm 1957, quy tụ nhiều nhà logic học và nhà khoa học máy tính, là khởi đầu của suy luận tự động, hoặc suy luận tự động hóa.^[4] Những người khác cho rằng nó bắt đầu trước đó với chương trình Logic Theorist năm 1955 của Newell, Shaw và Simon, hoặc với việc Martin Davis thực hiện quy trình quyết định của Presburger năm 1954 (chứng minh rằng tổng của hai số chẵn là chẵn).^[5]

Suy luận tự động, mặc dù là một lĩnh vực nghiên cứu quan trọng và phổ biến, đã trải qua một "mùa đông AI" vào những năm tám mươi và đầu những năm chín mươi. Tuy nhiên, sau đó lĩnh vực này đã hồi sinh. Ví dụ, vào năm 2005, Microsoft đã bắt đầu sử dụng công nghệ xác minh trong nhiều dự án nội bộ của họ và dự định đưa một ngôn ngữ đặc tả logic và kiểm tra (logical specification and checking language) vào phiên bản Visual C năm 2012.^[4]

Những đóng góp đáng kể

Principia Mathematica là một tác phẩm mang tính cột mốc trong logic hình thức được viết bởi Alfred North Whitehead và Bertrand Russell. Principia Mathematica - có nghĩa là Nguyên lý của Toán học - được viết với mục đích suy diễn tất cả hoặc một số biểu thức toán học bằng logic ký hiệu. Principia Mathematica ban đầu được xuất bản trong ba tập vào các năm 1910, 1912 và 1913.^[6]

Logic Theorist (LT) là chương trình đầu tiên được phát triển vào năm 1956 bởi Allen Newell, Cliff Shaw và Herbert A. Simon nhằm "mô phỏng suy luận của con người" trong việc chứng minh các định lý, và đã được thử nghiệm trên năm mươi hai định lý từ chương hai của Principia Mathematica, chứng minh được ba mươi tám trong số đó.^[7] Ngoài việc chứng minh các định lý, chương trình đã tìm ra một chứng minh cho một trong những định lý mà còn thanh thoát hơn so với chứng minh của Whitehead và Russell. Sau một lần không thành công trong việc xuất bản kết quả, Newell, Shaw và Herbert đã báo cáo trong ấn phẩm của họ năm 1958, The Next Advance in Operation Research:

"Hiện nay trên thế giới có những cỗ máy biết suy nghĩ, học hỏi và sáng tạo. Hơn nữa, khả năng làm những điều này của chúng sẽ tăng nhanh chóng cho đến khi (trong một tương lai có thể nhìn thấy) phạm vi các vấn đề chúng có thể xử lý sẽ rộng giống với phạm vi mà tâm trí con người đã áp dụng."^[8]

Ví dụ về các chứng minh hình thức

Năm	Định lý	Hệ thống chứng minh	Người chính thức hóa	Chứng minh truyền thống
1986	Định lý bất toàn thứ nhất	Boyer-Moore	Shankar[9]	Gödel
1990	Luật tương hỗ bậc hai	Boyer-Moore	Russinoff[10]	Eisenstein
1996	Định lý cơ bản của giải tích	HOL Light	Harrison	Henstock
2000	Định lý cơ bản của đại số	Mizar	Milewski	Brynski
2000	Định lý cơ bản của đại số	Coq	Geuvers et al.	Kneser
2004	Định lý bốn màu	Coq	Gonthier	Robertson et al.
2004	Định lý số nguyên tố	Isabelle	Avigad et al.	Selberg-Erdős
2005	Định lý đường cong Jordan	HOL Light	Hales	Thomassen
2005	Nguyên lý điểm bất động Brouwer	HOL Light	Harrison	Kuhn
2006	Flyspeck 1	Isabelle	Bauer- Nipkow	Hales
2007	Cauchy Residue	HOL Light	Harrison	Classical
2008	Định lý số nguyên tố	HOL Light	Harrison	Chứng minh giải tích
2012	Feit-Thompson	Coq	Gonthier et al.[11]	Bender, Glauberman và Peterfalvi
2016	Vấn đề bộ ba Pythagoras Boolean	Được chính thức hóa là SAT	Heule et al.[12]	None

Hệ thống chứng minh

Boyer-Moore Theorem Prover (NQTHM)

Thiết kế của NQTHM chịu ảnh hưởng bởi John McCarthy và Woody Bledsoe. Được khởi đầu vào năm 1971 tại Edinburgh, Scotland, đây là hệ thống chứng minh định lý hoàn toàn tự động, được xây dựng bằng Pure Lisp. Các điểm chính của NQTHM bao gồm:

1. sử dụng Lisp làm logic làm việc.
2. dựa vào nguyên lý định nghĩa cho các hàm đệ quy toàn phần.
3. sử dụng rộng rãi việc viết lại và "đánh giá biểu tượng".
4. một phương pháp suy diễn dựa trên việc thất bại của đánh giá biểu tượng.^[13][14]

HOL Light

Được viết bằng OCaml, HOL Light được thiết kế để có nền tảng logic đơn giản và gọn gàng cùng với một cách triển khai không phức tạp. Đây là một trợ lý chứng minh khác cho logic bậc cao cổ điển.^[15]

Coq

Phát triển ở Pháp, Coq là một trợ lý chứng minh tự động khác, có thể tự động trích xuất chương trình thực thi từ các đặc tả, dưới dạng mã nguồn của Objective CAML hoặc Haskell. Các thuộc tính, chương trình và chứng minh được chính thức hóa trong cùng một ngôn ngữ gọi là Tính toán của Các Cấu trúc Cảm ứng (Calculus of Inductive Constructions - CIC).^[16]

Ứng dụng

Suy luận tự động đã được sử dụng phổ biến nhất để xây dựng các hệ thống chứng minh định lý tự động. Tuy nhiên, hệ thống chứng minh định lý thường yêu cầu một số hướng dẫn của con người để hoạt động hiệu quả, vì vậy nó thường được coi là trợ lý chứng minh. Trong một số trường hợp, các hệ thống chứng minh định lý đã đưa ra các cách tiếp cận mới để chứng minh một định lý. Một ví dụ điển hình là chương trình Logic Theorist, chương trình này đã đưa ra một chứng minh cho một trong các định lý trong cuốn *Principia Mathematica* mà ít bước hơn so với chứng minh của Whitehead và Russell. Các chương trình suy luận tự động đang được áp dụng để giải quyết ngày càng nhiều vấn đề trong logic hình thức, toán học và khoa học máy tính, lập trình logic, xác minh phần mềm và phần cứng, thiết kế mạch và nhiều lĩnh vực khác. Thư viện TPTP (Sutcliffe và Suttner 1998) là một thư viện chứa các vấn đề như vậy, được cập nhật thường xuyên. Ngoài ra còn có một cuộc thi giữa các hệ thống chứng minh định lý tự động được tổ chức thường xuyên tại hội nghị CADE (Pelletier, Sutcliffe và Suttner 2002); các vấn đề cho cuộc thi được chọn từ thư viện TPTP.^[17]

Tham khảo

1. Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
2. John L. Pollock^{[cần chú thích đầy đủ]}
3. C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
4. ^ "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
5. Martin Davis (1983). “The Prehistory and Early History of Automated Deduction”. Trong Jörg Siekmann; G. Wrightson (biên tập). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. tr. 1–28. ISBN 978-3-642-81954-4. Here: p.15
6. "Principia Mathematica", tại Đại học Stanford. Retrieved 2010-10-19
7. "The Logic Theorist and its Children". Retrieved 2010-10-18
8. Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
9. Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, ISBN 9780521585330
10. Russinoff, David M. (1992), “A Mechanical Proof of Quadratic Reciprocity”, J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446, S2CID 14824949
11. Gonthier, G.; và đồng nghiệp (2013), “A Machine-Checked Proof of the Odd Order Theorem” (PDF), trong Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (biên tập), Interactive Theorem Proving, Lecture Notes in Computer Science, 7998, tr. 163–179, CiteSeerX 10.1.1.651.7964, doi:10.1007/978-3-642-39634-2_14, ISBN 978-3-642-39633-5, S2CID 1855636
12. Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). “Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer”. Theory and Applications of Satisfiability Testing – SAT 2016. Lecture Notes in Computer Science. 9710. tr. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6. S2CID 7912943.
13. The Boyer-Moore Theorem Prover Truy cập ngày 2010-10-23
14. Boyer, Robert S. và Moore, J Strother và Passmore, Grant Olney The PLTP Archive. Truy cập ngày 2023-07-27
15. Harrison, John HOL Light: an overview. Truy cập ngày 2010-10-23
16. Introduction to Coq. Truy cập ngày 2010-10-23
17. Automated Reasoning, Stanford Encyclopedia. Truy cập ngày 2010-10-10

Liên kết ngoài

• Hội thảo quốc tế về việc triển khai logic
• Chuỗi hội thảo về các chủ đề thành công thực nghiệm trong Suy luận Tự động