03 · ญาณวิทยา
การไต่สวนครั้งที่สามของภาค I: ถามไปแล้วว่าโปรแกรมคืออะไร คราวนี้ศาลถามว่ามันมีสิทธิ์อ้างว่ารู้อะไรได้บ้าง
คำตอบของเครื่องจักรนับเป็นความรู้หรือไม่
ปี 1976 เคนเนธ แอปเพลกับวุลฟ์กัง ฮาเคน ที่มหาวิทยาลัยอิลลินอยส์ เออร์บานา-แชมเปญ ประกาศบทพิสูจน์ทฤษฎีบทสี่สี — ข้อกล่าวอ้างที่ค้างมาตั้งแต่ปี 1852 ว่าแผนที่ใดๆ ระบายด้วยสี่สีได้โดยไม่มีสองพื้นที่ติดกันใช้สีเดียวกัน วิธีของพวกเขาบีบแผนที่ที่เป็นไปได้ไม่รู้จบให้เหลือชุดที่เลี่ยงไม่ได้ 1,476 โครงแบบ แต่ละโครงแบบต้องให้เครื่องตรวจ "การลดรูปได้" คอมพิวเตอร์รันราว 1,200 ชั่วโมง (Robertson, Sanders, Seymour & Thomas, "The Four Color Theorem") ไม่มีนักคณิตศาสตร์คนใดเคยอ่านการตรวจนั้นทีละบรรทัด และจะไม่มีวันมีใครอ่าน งานกรณีนั้นใหญ่เกินไป และไม่มีผู้ตรวจทานวารสารคนไหนอนุมานมันซ้ำ นี่คือบทพิสูจน์แรกของทฤษฎีบทสำคัญที่ขาดคอมพิวเตอร์ไม่ได้ และมันสั่นคลอนนักคณิตศาสตร์เพราะมันหักข้อสมมติที่เก่าจนไม่เคยต้องพูดออกมา: บทพิสูจน์คือสิ่งที่มนุษย์ผู้ผ่านการฝึกฝนตามอ่านได้ตั้งแต่บรรทัดแรกถึงบรรทัดสุดท้าย ในหลักการ แล้วรับรองด้วยความเข้าใจของตัวเอง ทฤษฎีบทสี่สีแทบจะแน่นอนว่าจริง แต่ข้อโต้แย้งของแอปเพล-ฮาเคนนับเป็นบทพิสูจน์ในความหมายเก่าหรือไม่ — สิ่งที่ surveyable (ตรวจสอบได้ทั้งหมด) สิ่งที่จิตหนึ่งถือครองไว้ได้ — แวดวงคณิตศาสตร์ไม่เคยปิดคำถามนี้ลงได้จริง
ความไม่มั่นคงนั้นคือหลักฐานชิ้นเปิดของบทนี้ และมันเรียกชื่อหลักการแรกออกมาตรงๆ: surveyable ไม่มีอะไรรับประกัน และเมื่อมันหายไป สิ่งที่บทพิสูจน์ทำให้เราได้ก็เปลี่ยนไปด้วย ภาพความแน่นอนทางคณิตศาสตร์แบบคลาสสิกของเดส์การ์ตส์สมมติลูกโซ่ของขั้นตอนที่เล็กพอและชัดพอให้จิตเดียวตรวจได้ทุกข้อต่อ บทพิสูจน์ของแอปเพลกับฮาเคนสมเหตุสมผลตามมาตรฐานรูปนัยทุกข้อที่นักวิทยาการคอมพิวเตอร์ระบุได้ แต่มันขอความไว้วางใจอีกชนิดหนึ่ง — ไว้ใจว่าคอมไพเลอร์คอมไพล์ถูก ว่าฮาร์ดแวร์ไม่สะดุดสักครั้งตลอด 1,200 ชั่วโมง ว่าโปรแกรมสร้างกรณีเองไม่พลาด ทฤษฎีบทอาจแน่นอน แต่เส้นทางไปสู่การเชื่อมันกลายเป็นข้อกล่าวอ้างเชิงวิศวกรรมพอๆ กับเชิงตรรกะ
หลักการที่สองจับวิธีที่ไม่เคยอ้างว่าตรวจสอบได้ทั้งหมดมาตั้งแต่ต้น: การจำลอง (simulation) พอล ฮัมฟรีส์ และเอริก วินส์เบิร์กที่ลงรายละเอียดมากกว่า (Science in the Age of Computer Simulation, University of Chicago Press, 2010) โต้แย้งว่าการจำลองด้วยคอมพิวเตอร์ไม่ให้ทั้งหลักฐานเชิงประจักษ์คลาสสิก (คุณรันสภาพภูมิอากาศจริงของโลกซ้ำเป็นการทดลองควบคุมไม่ได้) และการนิรนัยเชิงทฤษฎีคลาสสิก (แบบจำลองภูมิอากาศปะติดปะต่อจากทฤษฎี การประมาณเชิงตัวเลข และพารามิเตอร์ที่ปรับด้วยมือโดยไม่มีสมการเดี่ยวใดรับรอง) วินส์เบิร์กเรียกมันว่าหมวดหมู่เชิงญาณวิทยาที่แยกออกมาต่างหาก: เราไว้ใจการจำลองหนึ่งเพราะไว้ใจวิธีสร้างแบบจำลองนั้น — ฟิสิกส์ที่มันเข้ารหัสไว้ กลเม็ดที่ทำให้สมการซึ่งแก้ไม่ได้กลายเป็นแก้ได้ ประวัติผลงานของแบบจำลองคล้ายกันในกรณีที่คุณตรวจสอบได้ — ไม่ใช่เพราะไว้ใจว่าวัตถุที่ถูกจำลองกับวัตถุจริงเป็น "ระบบชนิดเดียวกัน" ในความหมายของผู้ทดลอง การจำลองเส้นทางเฮอริเคนไม่ใช่การสังเกตเฮอริเคน และไม่ใช่บทพิสูจน์เกี่ยวกับมัน มันคือสิ่งที่สาม หลักฐานที่ถูกสร้างขึ้น ไม่ใช่ถูกพบเจอ
หลักการที่สามคือความทึบ (opacity) และมันผ่ากลางวงการคำนวณสมัยใหม่เป็นเส้นตรง ฮัมฟรีส์บัญญัติคำว่าความทึบเชิงญาณวิทยา (epistemic opacity) ไว้ใช้กับกระบวนการที่องค์ประกอบซึ่งเกี่ยวข้องกับการให้เหตุผลรองรับผลลัพธ์ไม่ได้เปิดให้ผู้รู้ (epistemic agent) ที่ใช้มันเข้าถึงได้ครบ แม้ในหลักการ (Extending Ourselves: Computational Science, Empiricism, and Scientific Method, Oxford University Press, 2004) โปรแกรมที่เขียนแบบดั้งเดิมโปร่งใสในความหมายเฉพาะอย่างหนึ่ง: จะยาวแค่ไหนก็ตาม ตรรกะของมันเปิดให้ผู้อ่านที่มีความสามารถตรวจทีละบรรทัดได้ในหลักการ โครงข่ายประสาทเทียมที่ผ่านการฝึกทึบคนละแบบ: "เหตุผล" ของมันกระจายอยู่ในการเชื่อมต่อถ่วงน้ำหนักเป็นล้านหรือพันล้านจุด ที่ไม่มีใครออกแบบ มีแต่ปลูกขึ้นด้วย gradient descent และไม่มีมนุษย์คนใด — ผู้สร้างมันเองก็ด้วย — ตามรอยได้ว่าทำไมเอาต์พุตนี้จึงโผล่ออกมาแทนอีกอันหนึ่ง เรื่องนี้กระทบคำให้การ (testimony) ของเครื่องจักรโดยตรง: เมื่อแบบจำลองวินิจฉัยตีธงว่าพบเนื้องอก นั่นคือรายงานจากสิ่งที่ให้เหตุผลได้ ที่ต้องชั่งน้ำหนักอย่างที่เราชั่งคำตัดสินของเพื่อนร่วมงาน หรือคือการอ่านค่า ที่ต้องชั่งอย่างที่เราชั่งตัวเลขจากเทอร์โมมิเตอร์ สองอย่างนี้แบกน้ำหนักเชิงญาณวิทยา (epistemic weight) ไม่เท่ากัน และระบบทึบทำให้บอกได้ยากอย่างอึดอัดว่าคุณกำลังได้อันไหน
หลักการที่สี่คือสงครามกลางเมืองเก่าที่เล่นซ้ำภายใต้ชื่อใหม่: การพิสูจน์ความถูกต้องของโปรแกรม (program verification) กับการทดสอบ เหตุผลนิยม (rationalism) กับประสบการณ์นิยม (empiricism) เดือนพฤษภาคม 1979 ริชาร์ด เดอมิลโล ริชาร์ด ลิปตัน และอลัน เพอร์ลิส ตีพิมพ์ "Social Processes and Proofs of Theorems and Programs" (Communications of the ACM 22, no. 5: 271–280) ข้อโต้แย้งของพวกเขาคือความแน่นอนทางคณิตศาสตร์วางอยู่บนกระบวนการทางสังคม — เพื่อนร่วมวงการตรวจ อนุมานซ้ำ แล้วในที่สุดก็เชื่อบทพิสูจน์นั้น — และการพิสูจน์ความถูกต้องของโปรแกรมทำซ้ำกระบวนการนี้ในระดับใหญ่ไม่ได้เลย เพราะไม่มีชุมชนเทียบเคียงใดจะมาตรวจบทพิสูจน์รูปนัยยาวล้านบรรทัดของผลิตภัณฑ์ที่ส่งมอบไปแล้วซ้ำอีกรอบ "Program Verification: The Very Idea" ของเจมส์ เฟตเซอร์ปี 1988 (Communications of the ACM 31, no. 9: 1048–1063) ลับข้อคัดค้านนั้นให้เป็นข้อกล่าวอ้างเชิงปรัชญา: อัลกอริทึมในฐานะโครงสร้างเชิงตรรกะนามธรรมรับบทพิสูจน์เชิงนิรนัยได้ แต่โปรแกรมในฐานะกระบวนการทางกายภาพที่รันบนฮาร์ดแวร์จริงซึ่งบางครั้งบกพร่องนั้นรับไม่ได้ เพราะไม่มีการนิรนัยใดรับรองว่าซิลิคอนจะทำตัวอย่างที่ข้อกำหนดสมมติไว้ อุดมคติเหตุผลนิยมของฝ่ายพิสูจน์ความถูกต้อง — พิสูจน์ครั้งเดียว รู้ตลอดไป — มาชนคำตอบโต้แบบประสบการณ์นิยมของฝ่ายทดสอบ ที่เอ็ดสเกอร์ ไดก์สตราสรุปไว้ก่อนหน้านั้นหนึ่งทศวรรษว่า "การทดสอบโปรแกรมใช้แสดงการมีอยู่ของบั๊กได้ แต่ไม่เคยใช้แสดงการไม่มีอยู่ของมันได้เลย" ("Program testing can be used to show the presence of bugs, but never to show their absence") ("Notes on Structured Programming," EWD249, 1970) ไม่มีฝ่ายใดชนะ ซอฟต์แวร์ทุกวันนี้ส่งมอบด้วยส่วนผสมของทั้งสอง พิสูจน์ความถูกต้องตรงที่ราคาถูกพอ ทดสอบในที่เหลือทั้งหมด
หลักการที่ห้าคือกับดักที่เก่าที่สุดในญาณวิทยา สวมเปลือกเซนเซอร์มา บทความสามหน้าของเอ็ดมันด์ เก็ตติเยร์ปี 1963 "Is Justified True Belief Knowledge?" (Analysis 23, no. 6: 121–123) แสดงว่าความเชื่อหนึ่งมีเหตุผลรองรับและเป็นจริงพร้อมกันได้ โดยยังไม่ใช่ความรู้ ถ้าเหตุผลรองรับกับความจริงบรรจบกันด้วยความบังเอิญ — ภาพคลาสสิกคือนาฬิกาหยุดเดินที่บังเอิญบอกเวลาถูก สายพานอัตโนมัติผลิตโครงสร้างแบบนี้ออกมาเป็นประจำ: ระบบจดจำใบหน้าที่มีบั๊กจริง สมมติว่าปรับเทียบผิดกับใบหน้ามุมหนึ่ง ยังให้ผลจับคู่ที่ถูกต้องบนเฟรมหนึ่งได้โดยบังเอิญ ทั้งที่แบกเหตุผลรองรับเชิงสถาบันเต็มชุด ("ระบบนี้แม่นยำ 99%") ซึ่งตามปกติจะรับรองความเชื่อหนึ่งให้เป็นความรู้ ผลลัพธ์นั้นเป็นจริง ไว้วางใจได้อย่างสมเหตุสมผล และมาจากกระบวนการที่ในโอกาสนั้นไม่ได้ทำสิ่งที่เหตุผลรองรับของมันสมมติว่ามันทำ นาฬิกาหยุดเดินของเก็ตติเยร์ตอนนี้มีกล้อง
ผู้คน โดยย่อ แอปเพลกับฮาเคนโดนวิจารณ์หนักพอสมควร สำหรับบทพิสูจน์ที่หลายคนยังเรียกว่าไม่สง่างาม มากกว่าจะเรียกว่าผิด ฮัมฟรีส์กับวินส์เบิร์กสร้างสาขาย่อยขึ้นมาทั้งสาขา — ปรัชญาแห่งการจำลองด้วยคอมพิวเตอร์ — จากการเอาจริงกับวิธีที่นักวิทยาศาสตร์หน้างานไว้ใจมาหลายสิบปีโดยไม่เคยถามว่ามันเป็นหลักฐานชนิดไหน บทความปี 1988 ของเฟตเซอร์จุดชนวนจดหมายโต้ตอบเชิงเทคนิคหลายหน้าภายในหนึ่งปี และการถกเถียงที่ยังถูกอ้างถึงทุกวันนี้ — หนึ่งในข้อขัดแย้งที่ยืนยาวที่สุดเท่าที่ Communications of the ACM เคยพิมพ์
เชื่อมโยง
บทที่ 01 วางพื้นหลังเชิงทฤษฎีบทพิสูจน์ — ความสมเหตุสมผลเชิงตรรกะ ความสมบูรณ์ และขีดจำกัดของเกอเดิล — ที่ surveyability สมมติไว้เงียบๆ บทที่ 09 ถามว่าการตัดสินไม่ได้ (undecidability) อนุญาตให้อ้างอะไรได้บ้างในเชิงปรัชญา เป็นคำถามคู่กับสิ่งที่บทพิสูจน์ซึ่งตรวจสอบทั้งหมดไม่ได้อนุญาตให้อ้างในบทนี้ บทที่ 13 กลับมาที่ความทึบจากฝั่งการเรียนรู้: งานวิจัย interpretability ในฐานะห้องทดลองที่ไว้ค้นว่ามีอะไรอยู่ในกล่องดำ ถ้ามี
คำถามที่ยังเปิดอยู่
ถ้าบทพิสูจน์หนึ่งแน่นอนได้โดยตรวจสอบทั้งหมดไม่ได้ คำว่า "บทพิสูจน์" เปลี่ยนความหมายไปเงียบๆ ตั้งแต่ยุคยูคลิดหรือไม่ หรือมันแปลว่า "ได้รับการรับรองตามมาตรฐานของยุคนั้น" มาตลอด และมาตรฐานของยูคลิดก็แค่เข้มกว่าของเราด้วยความบังเอิญทางประวัติศาสตร์ และความทึบของเครื่องจักรเป็นข้อจำกัดเชิงวิศวกรรมชั่วคราวที่งานวิจัย interpretability จะสลายมันได้ในที่สุด หรือเป็นคุณลักษณะเชิงโครงสร้างถาวรของระบบใดๆ ที่ "ความรู้" ของมันกระจายอยู่เชิงสถิติ แทนที่จะถูกเขียนไว้เป็นกฎ
อ่านต่อ
- Eric Winsberg, Science in the Age of Computer Simulation, University of Chicago Press, 2010 — ข้อเสนอก่อตั้งสำหรับการจำลองในฐานะหมวดหมู่เชิงญาณวิทยาของตัวมันเอง
- Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis, "Social Processes and Proofs of Theorems and Programs," Communications of the ACM 22, no. 5 (1979): 271–280; James H. Fetzer, "Program Verification: The Very Idea," Communications of the ACM 31, no. 9 (1988): 1048–1063
- Computer Simulations in Science, สารานุกรมปรัชญาสแตนฟอร์ด (SEP)