การให้เหตุผลอัตโนมัติคืออะไร
การให้เหตุผลอัตโนมัติเป็นสาขาวิชาวิทยาการคอมพิวเตอร์ที่พยายามรับประกันว่าระบบหรือโปรแกรมจะทำอะไรหรือจะไม่ทำอะไร การรับประกันนี้ขึ้นอยู่กับการพิสูจน์ทางคณิตศาสตร์ ผู้คนแก้ปัญหาเชิงตรรกะมากมายในคณิตศาสตร์ วิทยาศาสตร์ และการคำนวณโดยใช้กลยุทธ์เชิงตรรกะ เช่น ทฤษฎีบทและการนิรนัย การให้เหตุผลอัตโนมัติใช้คอมพิวเตอร์ที่ใช้เครื่องมือเดียวกันเพื่อแก้ปัญหาที่ซับซ้อน การให้เหตุผลอัตโนมัติพยายามตอบคำถามเกี่ยวกับโปรแกรม (หรือสูตรตรรกะ) โดยใช้เทคนิคที่ทราบจากคณิตศาสตร์ เครื่องมือต่างๆ ช่วยให้คุณตรวจสอบว่าข้อความหรือนิพจน์ใดเป็นจริง
การให้เหตุผลอัตโนมัติสามารถแก้ปัญหาอะไรได้บ้าง
นักวิทยาศาสตร์และนักพัฒนาซอฟต์แวร์ใช้การให้เหตุผลอัตโนมัติเพื่อพิสูจน์สองอย่างนี้ อย่างแรก พวกเขาพิสูจน์ว่าการออกแบบระบบหรือการดำเนินการปฏิบัติตามข้อกำหนดของมัน อย่างที่สอง พวกเขาพิสูจน์ว่ามันได้ผล ตามที่มันตั้งใจไว้
การให้เหตุผลอัตโนมัติทำเช่นนี้โดยการผลิตข้อพิสูจน์ในตรรกะทางการที่สนับสนุนโดยทฤษฎีบททางคณิตศาสตร์ หรือความจริงที่เป็นที่รู้จัก การให้เหตุผลอัตโนมัติใช้วิธีการตรวจสอบอัลกอริทึมเชิงตรรกะทางคณิตศาสตร์เพื่อสร้างข้อพิสูจน์ความปลอดภัยหรือความถูกต้องสำหรับพฤติกรรมที่เป็นไปได้ทั้งหมด
อีกทั้งการให้เหตุผลอัตโนมัติยังสามารถใช้เพื่อพิสูจน์ว่าระบบที่ใช้ในการกำหนดค่าเครือข่าย อนุญาตให้เข้าถึงเครือข่ายหรือให้สิทธิ หรือเพื่อให้ข้อมูลมีความเป็นส่วนตัวและปลอดภัยในการทำงานตามที่ตั้งใจไว้
เมื่อคุณใช้การให้เหตุผลอัตโนมัติ ครั้งแรกคุณต้องเสนอคำชี้แจงปัญหากับระบบ จากนั้นระบบการให้เหตุผลอัตโนมัติจะคำนวณและตรวจสอบสมมติฐานตามคำชี้แจงปัญหา ซอฟต์แวร์จะทำเช่นนี้จนกว่าจะหมดตัวเลือกทั้งหมด
ตัวอย่างปัญหาสำหรับการให้เหตุผลอัตโนมัติ
เพื่อให้เข้าใจการให้เหตุผลอัตโนมัติให้ดีขึ้น โปรดพิจารณาคำชี้แจงปัญหา แมวอาศัยอยู่บนบกหรือไม่ และการยืนยันต่อไปนี้
- แมวเป็นสัตว์เลี้ยงลูกด้วยนม
- สัตว์เลี้ยงลูกด้วยนมอาศัยอยู่บนบก
ระบบการให้เหตุผลอัตโนมัติจะประเมินว่าคำชี้แจงปัญหาเป็นความจริงหรือไม่ กล่าวโดยเจาะจง มันใช้การนิรนัยเชิงตรรกะ ในกรณีนี้ แมวเป็นสัตว์เลี้ยงลูกด้วยนม และสัตว์เลี้ยงลูกด้วยนมอาศัยอยู่บนบก ดังนั้นมันจะยืนยันว่าแมวอาศัยอยู่บนบก
ข้อจำกัดของการให้เหตุผลอัตโนมัติ
การให้เหตุผลอัตโนมัติไม่ได้ทำการคาดการณ์หรือการทำให้ครอบคลุมทั่วไป ยกตัวอย่างเช่น เราสามารถใช้การให้เหตุผลอัตโนมัติเพื่อสร้างการโต้แย้งเช่นนี้
- แมวมีขน
- ขนปุยเป็นแมวตัวหนึ่ง
- ดังนั้นขนปุยมจึงมีขน
เราไม่สามารถใช้การให้เหตุผลอัตโนมัติเพื่อสร้างการโต้แย้งเช่นนี้
- แมวเป็นสัตว์เลี้ยงลูกด้วยนม
- แมวอาศัยอยู่บนบก
- ดังนั้นสัตว์เลี้ยงลูกด้วยนมทั้งหมดจึงอาศัยอยู่บนบก
การใช้งานดังกล่าวเป็นเรื่องทั่วไปในการพิสูจน์ทฤษฎีบท ซึ่งต้องใช้คำแนะนำของมนุษย์เมื่อปฏิบัติงานให้เหตุผลเชิงอนุมาน
การใช้การให้เหตุผลอัตโนมัติมีอะไรบ้าง
ความสามารถการให้เหตุผลอัตโนมัติที่จะทำการอนุมานตรรกะทีละขั้นตอนมีประโยชน์ในหลากหลายด้าน ด้วยการใช้การให้เหตุผลอัตโนมัติ คุณจะสามารถพิสูจน์ความปลอดภัย การปฏิบัติตามข้อกำหนด ความพร้อมใช้งาน ความทนทาน และคุณสมบัติด้านความปลอดภัยของสถาปัตยกรรมขนาดใหญ่ได้
ต่อไปนี้คือการใช้การให้เหตุผลอัตโนมัติในกรณีอื่นๆ
โมเดลทางคณิตศาสตร์
นักวิทยาศาสตร์ วิศวกร และนักคณิตศาสตร์ แก้ปัญหาและตรวจสอบการพิสูจน์ทางคณิตศาสตร์ โดยการนำสูตรพีชคณิตมาประยุกต์ใช้ในการประยุกต์ทางวิทยาศาสตร์ ในการปฏิบัติเช่นนั้น พวกเขาใช้โมเดลทางคณิตศาสตร์ที่พึ่งพาตัวแปรหลากหลายเพื่ออนุมานวิธีแก้ปัญหาที่น่าจะเป็นไปได้
การตรวจสอบฮาร์ดแวร์
การให้เหตุผลอัตโนมัติช่วยให้วิศวกรฮาร์ดแวร์สร้างผลิตภัณฑ์ที่เชื่อถือได้ มันช่วยให้พวกเขาค้นพบข้อบกพร่องที่อาจถูกมองข้ามไปจากวิธีการทดสอบแบบดั้งเดิม
ยกตัวอย่างเช่น วิศวกรออกแบบอิเล็กทรอนิกส์ใช้การวิเคราะห์การให้เหตุผลอัตโนมัติทางคณิตศาสตร์อย่างเข้มงวดเพื่อให้ได้ข้อพิสูจน์ที่แน่นอน ว่าการออกแบบฮาร์ดแวร์เฉพาะนั้นตรงตามข้อกำหนดของมัน เช่น พฤติกรรมของระบบหรือการดำเนินการ
การตรวจสอบแสดงให้เห็นว่าพฤติกรรมที่เป็นไปได้ทั้งหมดของระบบทำตามลักษณะชั่วคราวซึ่งประกอบข้อกำหนดได้ นอกจากนี้ยังอาจแสดงให้เห็นว่าแต่ละพฤติกรรมที่เป็นไปได้ของการดำเนินงานของระบบนั้นสอดคล้องกับพฤติกรรมของข้อกำหนดระดับสูงบางอย่างของมัน
การตรวจสอบซอฟต์แวร์
นักพัฒนาซอฟต์แวร์ใช้การให้เหตุผลอัตโนมัติเพื่อช่วยให้มั่นใจว่าแอปพลิเคชันมีประสิทธิภาพต่อปัญหาด้านความปลอดภัยที่ไม่พึงประสงค์ และซอฟต์แวร์นั้นทำงานตามที่ตั้งใจไว้หรือตามที่ได้รับการออกแบบ เช่นเดียวกับการตรวจสอบฮาร์ดแวร์ การให้เหตุผลอัตโนมัติช่วยให้นักพัฒนาตรวจสอบมาตรการรักษาความปลอดภัยซอฟต์แวร์ต่อนโยบายต่างๆ ได้
ตัวอย่างเช่น วิศวกรที่ Amazon Web Services (AWS) พิสูจน์ว่ารหัสบูตมีความปลอดภัยสำหรับทุกการกำหนดค่าการบูตด้วยการให้เหตุผลอัตโนมัติ อีกตัวอย่างหนึ่งคือพวกเขาพิสูจน์ว่าข้อมูลที่จัดเก็บและประมวลผลใน Amazon Simple Storage Service (Amazon S3) ได้รับการป้องกัน ในตัวอย่างนี้ พวกเขาใช้การให้เหตุผลอัตโนมัติสำหรับการจำลองแบบ ความสอดคล้อง การปรับขนาดอัตโนมัติ การปรับสมดุลโหลด และการประสานงานอื่นๆ
การจำลองเหตุผลของมนุษย์
นักวิทยาศาสตร์คอมพิวเตอร์ใช้เทคโนโลยีการให้เหตุผลอัตโนมัติเพื่อกำหนดค่าการเข้าถึง เพื่อทำเช่นนี้ พวกเขาเขียนนโยบายที่อธิบายจะอนุญาตและปฏิเสธคำขอของผู้ใช้เพื่อเข้าถึงทรัพยากรเมื่อไหร่ สิ่งนี้จะตรวจสอบว่าเฉพาะผู้ใช้ที่ตั้งใจเท่านั้นที่สามารถเข้าถึงทรัพยากร ซึ่งเป็นสิ่งสำคัญสำหรับความปลอดภัยและความเป็นส่วนตัวของทรัพยากร
ยกตัวอย่างเช่น นักวิทยาศาสตร์คอมพิวเตอร์ใช้สูตร Satisfiability Modulo Theories (SMT) และตัวแก้ปัญหา SMT เพื่อพิสูจน์คุณสมบัติด้านความปลอดภัย
เครื่องมือและเทคนิคการให้เหตุผลอัตโนมัติมีอะไรบ้าง
ถัดไป เราจะแบ่งปันวิธีการนิรนัยอัตโนมัติอันหลากหลายที่ช่วยให้ระบบคอมพิวเตอร์สามารถดำเนินการนิรนัยอย่างมนุษย์ได้
ตรรกะดั้งเดิม
ตรรกะดั้งเดิมเป็นปรัชญาทางคณิตศาสตร์ที่ให้โมเดลการให้เหตุผลพื้นฐานสำหรับโปรแกรมการให้เหตุผลเชิงตรรกะอัตโนมัติ ตรรกะนี้ขึ้นอยู่กับหลักการที่แต่ละข้อเสนอมีค่าความจริงที่เป็นจริงหรือเท็จ แต่ไม่ใช่ทั้งสองอย่าง
โดยจะมุ่งเน้นไปที่ตรรกะลำดับแรกเป็นหลัก ซึ่งช่วยให้นักคณิตศาสตร์สามารถแสดงตัวแปรที่ไม่รู้จัก เช่น x ด้วยตัวบ่งปริมาณเหมือนที่มีอยู่ใน ประโยค ตัวอย่างเช่น นักวิทยาศาสตร์ใช้ตรรกะดั้งเดิมในการเขียนโปรแกรมตรรกะเพื่อหา x ในประโยคนี้ โดยที่ x ที่มีอยู่ x อาศัยอยู่บนบก และ x นั้นเป็นสัตว์เลี้ยงลูกด้วยนม
ตรรกะที่มีคุณค่า
ตรรกะที่มีคุณค่าเป็นระบบตรรกะที่มีคุณค่าที่สามารถเป็นได้ทั้งจริงหรือเท็จและโครงสร้างความสัมพันธ์ระหว่างพวกมันที่เรียกว่าการโต้แย้ง
คำสั่งดั้งเดิมของการโต้แย้งในตรรกะที่มีคุณค่าคือ หาก P เช่นนั้น Q ตัวอย่างเช่น หากเป็นวันเสาร์ เช่นนั้นมันก็เป็นวันหยุดสุดสัปดาห์
การให้เหตุผลอัตโนมัติใช้เทคนิคที่เรียกว่า SAT Solving มันใช้เครื่องมือที่เรียกว่า SAT Solvers เพื่อค้นหาการกำหนดที่น่าพึงพอใจในการโต้แย้งตรรกะที่มีคุณค่า ซึ่งหมายความว่ามันเป็นตัวแปรที่ทำให้การโต้แย้งเป็นจริง
อะไรคือข้อแตกต่างระหว่างการให้เหตุผลอัตโนมัติกับปัญญาประดิษฐ์
การให้เหตุผลอัตโนมัติเป็นสายวิชาเฉพาะของปัญญาประดิษฐ์ (AI) ที่ใช้การนิรนัยเชิงตรรกะกับระบบคอมพิวเตอร์
AI เป็นวิทยาศาสตร์ที่สอนคอมพิวเตอร์ให้คิดเหมือนผู้คนเมื่อคอมพิวเตอร์แก้ปัญหา การพัฒนาล่าสุดของ AI ได้นำไปสู่ความก้าวหน้าของสายวิชาย่อยต่างๆ รวมถึงดีปเลิร์นนิง การวิเคราะห์ข้อมูล และแมชชีนเลิร์นนิง
การให้เหตุผลอัตโนมัติแตกต่างจากเทคโนโลยี AI อื่นๆ เช่น การประมวลผลภาษาธรรมชาติ (NLP) ซึ่งเน้นการฝึกฝนคอมพิวเตอร์ให้เข้าใจคำพูดที่เป็นลายลักษณ์อักษรหรือวาจา แต่การให้เหตุผลอัตโนมัติจะใช้โมเดลทางตรรกะและการพิสูจน์เพื่อให้เหตุผลเกี่ยวกับพฤติกรรมที่เป็นไปได้ของระบบหรือโปรแกรม รวมไปถึงระบุว่ามันสามารถไปหรือไปไม่ถึงหรือไม่
อะไรคือข้อแตกต่างระหว่างการให้เหตุผลอัตโนมัติกับดีปเลิร์นนิง
การให้เหตุผลอัตโนมัติเป็นการพิสูจน์คุณสมบัติของโปรแกรมหรือระบบ มันใช้โปรแกรมหรือระบบของตัวเองเช่นเดียวกับโมเดลหรือข้อกำหนดของระบบในตรรกะอย่างเป็นทางการ
ดีปเลิร์นนิงคาดการณ์โดยขึ้นอยู่กับการนำโมเดลทางสถิติไปใช้กับชุดข้อมูลขนาดใหญ่
ดีปเลิร์นนิงเป็นเทคโนโลยีแมชชีนเลิร์นนิงขั้นสูง ที่จำลองการทำงานของสมองมนุษย์ โดยจะใช้โมเดลนิวรัลเน็ตเวิร์กต่างๆ ที่ประกอบด้วยนิวรอนหลายเลเยอร์ที่ทำการแยก เปรียบเทียบ และวิเคราะห์ข้อมูลที่เกี่ยวข้อง นักวิทยาศาสตร์ข้อมูลใช้ดีปเลิร์นนิงสำหรับการใช้งานที่ซับซ้อน เช่น การประมวลผลกล้อง และข้อมูลเซนเซอร์ในรถยนต์ที่ขับเคลื่อนด้วยตนเอง
การให้เหตุผลโดยอัตโนมัติเป็นแมชชีนเลิร์นนิงหรือไม่
การให้เหตุผลอัตโนมัติและแมชชีนเลิร์นนิงนั้นไม่เหมือนกัน สรุปง่ายๆ ว่าแมชชีนเลิร์นนิงทำการคาดการณ์และการอนุมาน การให้เหตุผลอัตโนมัติมีการพิสูจน์
ส่วนแมชชีนเลิร์นนิงนั้นเป็นส่วนย่อยของ AI ที่ฝึกฝนคอมพิวเตอร์ให้ตัดสินใจด้วยตัวอย่างข้อมูลขนาดใหญ่ ยกตัวอย่างเช่น นักวิทยาศาสตร์ข้อมูลใช้แมชชีนเลิร์นนิงในการฝึกฝนซอฟต์แวร์ธนาคารเพื่อระบุกิจกรรมฉ้อโกง พวกเขาใช้ตัวอย่างขนาดใหญ่ของข้อมูลทางการเงินเพื่อให้แน่ใจว่าซอฟต์แวร์ระบุรูปแบบที่ผิดปกติได้อย่างง่ายดายขึ้นอยู่กับผลการเรียนรู้ก่อนหน้านี้
แทนที่จะฝึกฝนโมเดลด้วยข้อมูล การให้เหตุผลอัตโนมัติช่วยให้โมเดลสามารถอนุมานผลลัพธ์ตามความจริงทางคณิตศาสตร์และการพิสูจน์ได้
AWS ใช้การให้เหตุผลอัตโนมัติเพื่อปรับปรุงการให้บริการอย่างไร
AWS ใช้เหตุผลอัตโนมัติเพื่อปรับปรุงการให้บริการที่หลากหลาย ตัวอย่างมีดังนี้
- Amazon CodeGuru Reviewer ใช้เหตุผลอัตโนมัติและแมชชีนเลิร์นนิงเพื่อช่วยผู้ พัฒนาในการระบุช่องโหว่ของซอฟต์แวร์
- Amazon Inspector Classic มี คุณลักษณะ การเข้าถึงเครือข่ายที่วิเคราะห์อินสแตนซ์ EC2 ของคุณโดยอัตโนมัติสำหรับช่องโหว่ด้านความปลอดภัยและการกำหนดค่าผิดพลาดที่อาจเกิดขึ้น
- AWS Identity and Access Management (IAM) Access Analyzer จัดการสิทธิ์เข้าถึงบัญชีด้วยการให้เหตุผลอัตโนมัติ
- Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer ใช้การให้เหตุผลอัตโนมัติเพื่อช่วยให้คุณเข้าใจและแสดงภาพเครือข่าย AWS ของคุณ
ไปที่ การรักษาความปลอดภัยที่พิสูจน์ได้ สำหรับข้อมูลเพิ่มเติมเกี่ยวกับการให้เหตุผลอัตโนมัติทั่วทั้งบริการของ AWS เราใช้การให้เหตุผลทางคณิตศาสตร์เพื่อรับรองความปลอดภัยที่แข็งแกร่งสำหรับเวิร์กโหลดด้านความปลอดภัยของคุณ
เริ่มต้นใช้งานความปลอดภัยบน AWS ด้วยการสร้างบัญชีวันนี้
ขั้นตอนถัดไปบน AWS
