03 · Epistemology
03 · ญาณวิทยา
Part I's third hearing: having asked what a program is, the court now asks what it is entitled to claim it knows.
การไต่สวนครั้งที่สามของภาค I: ถามไปแล้วว่าโปรแกรมคืออะไร คราวนี้ศาลถามว่ามันมีสิทธิ์อ้างว่ารู้อะไรได้บ้าง
Does a machine's answer count as knowledge?
คำตอบของเครื่องจักรนับเป็นความรู้หรือไม่
In 1976, Kenneth Appel and Wolfgang Haken, at the University of Illinois at Urbana–Champaign, announced a proof of the four-color theorem — the claim, open since 1852, that any map can be colored with four colors so that no two adjacent regions share one. Their method reduced the infinite variety of possible maps to an unavoidable set of 1,476 configurations, each of which had to be checked for "reducibility" by machine; the computer ran roughly 1,200 hours (Robertson, Sanders, Seymour & Thomas, "The Four Color Theorem"). No mathematician has ever read that check line by line, and none ever will; the case-work is too vast, and no journal referee re-derives it. The result was the first proof of a major theorem that essentially required a computer, and it unsettled mathematicians precisely because it broke an assumption so old it had never needed stating: that a proof is something a trained human being can, in principle, follow from first line to last and certify with their own understanding. The four-color theorem is almost certainly true. Whether the Appel–Haken argument counts as a proof in the older sense — something surveyable, something a mind can hold — is a question the mathematical community has never fully closed.
ปี 1976 เคนเนธ แอปเพลกับวุลฟ์กัง ฮาเคน ที่มหาวิทยาลัยอิลลินอยส์ เออร์บานา-แชมเปญ ประกาศบทพิสูจน์ทฤษฎีบทสี่สี — ข้อกล่าวอ้างที่ค้างมาตั้งแต่ปี 1852 ว่าแผนที่ใดๆ ระบายด้วยสี่สีได้โดยไม่มีสองพื้นที่ติดกันใช้สีเดียวกัน วิธีของพวกเขาบีบแผนที่ที่เป็นไปได้ไม่รู้จบให้เหลือชุดที่เลี่ยงไม่ได้ 1,476 โครงแบบ แต่ละโครงแบบต้องให้เครื่องตรวจ "การลดรูปได้" คอมพิวเตอร์รันราว 1,200 ชั่วโมง (Robertson, Sanders, Seymour & Thomas, "The Four Color Theorem") ไม่มีนักคณิตศาสตร์คนใดเคยอ่านการตรวจนั้นทีละบรรทัด และจะไม่มีวันมีใครอ่าน งานกรณีนั้นใหญ่เกินไป และไม่มีผู้ตรวจทานวารสารคนไหนอนุมานมันซ้ำ นี่คือบทพิสูจน์แรกของทฤษฎีบทสำคัญที่ขาดคอมพิวเตอร์ไม่ได้ และมันสั่นคลอนนักคณิตศาสตร์เพราะมันหักข้อสมมติที่เก่าจนไม่เคยต้องพูดออกมา: บทพิสูจน์คือสิ่งที่มนุษย์ผู้ผ่านการฝึกฝนตามอ่านได้ตั้งแต่บรรทัดแรกถึงบรรทัดสุดท้าย ในหลักการ แล้วรับรองด้วยความเข้าใจของตัวเอง ทฤษฎีบทสี่สีแทบจะแน่นอนว่าจริง แต่ข้อโต้แย้งของแอปเพล-ฮาเคนนับเป็นบทพิสูจน์ในความหมายเก่าหรือไม่ — สิ่งที่ surveyable (ตรวจสอบได้ทั้งหมด) สิ่งที่จิตหนึ่งถือครองไว้ได้ — แวดวงคณิตศาสตร์ไม่เคยปิดคำถามนี้ลงได้จริง
That unease is this chapter's opening exhibit, and it names the first principle directly: surveyability is not guaranteed, and its loss changes what proof can do for us. Descartes's classical picture of mathematical certainty assumed a chain of steps small enough, and clear enough, for one mind to inspect every link. Appel and Haken's proof is sound by every formal standard computer scientists can specify, yet it asks for a different kind of trust — trust that the compiler compiled correctly, that the hardware did not glitch across 1,200 hours, that the case-generating program itself contained no error. The theorem may be certain; the route to believing it has become an engineering claim as much as a logical one.
ความไม่มั่นคงนั้นคือหลักฐานชิ้นเปิดของบทนี้ และมันเรียกชื่อหลักการแรกออกมาตรงๆ: surveyable ไม่มีอะไรรับประกัน และเมื่อมันหายไป สิ่งที่บทพิสูจน์ทำให้เราได้ก็เปลี่ยนไปด้วย ภาพความแน่นอนทางคณิตศาสตร์แบบคลาสสิกของเดส์การ์ตส์สมมติลูกโซ่ของขั้นตอนที่เล็กพอและชัดพอให้จิตเดียวตรวจได้ทุกข้อต่อ บทพิสูจน์ของแอปเพลกับฮาเคนสมเหตุสมผลตามมาตรฐานรูปนัยทุกข้อที่นักวิทยาการคอมพิวเตอร์ระบุได้ แต่มันขอความไว้วางใจอีกชนิดหนึ่ง — ไว้ใจว่าคอมไพเลอร์คอมไพล์ถูก ว่าฮาร์ดแวร์ไม่สะดุดสักครั้งตลอด 1,200 ชั่วโมง ว่าโปรแกรมสร้างกรณีเองไม่พลาด ทฤษฎีบทอาจแน่นอน แต่เส้นทางไปสู่การเชื่อมันกลายเป็นข้อกล่าวอ้างเชิงวิศวกรรมพอๆ กับเชิงตรรกะ
The second principle addresses a method that never pretended to surveyability in the first place: simulation. Paul Humphreys and, at greater length, Eric Winsberg (Science in the Age of Computer Simulation, University of Chicago Press, 2010) have argued that computer simulation supplies neither classical empirical evidence (you cannot rerun Earth's actual climate as a controlled experiment) nor classical theoretical deduction (a climate model is stitched from theory, numerical approximations, and hand-tuned parameters no single equation justifies). Winsberg calls this a distinct epistemic category: trust in a simulation rests on trust in the model's construction — the physics it encodes, the tricks it uses to make intractable equations tractable, the track record of similar models on cases you can check — rather than on trust that the modeled object and the real object are, in the experimenter's sense, "the same kind of system." A hurricane-track simulation is neither an observation of a hurricane nor a proof about one; it is a third thing, evidence built rather than found.
หลักการที่สองจับวิธีที่ไม่เคยอ้างว่าตรวจสอบได้ทั้งหมดมาตั้งแต่ต้น: การจำลอง (simulation) พอล ฮัมฟรีส์ และเอริก วินส์เบิร์กที่ลงรายละเอียดมากกว่า (Science in the Age of Computer Simulation, University of Chicago Press, 2010) โต้แย้งว่าการจำลองด้วยคอมพิวเตอร์ไม่ให้ทั้งหลักฐานเชิงประจักษ์คลาสสิก (คุณรันสภาพภูมิอากาศจริงของโลกซ้ำเป็นการทดลองควบคุมไม่ได้) และการนิรนัยเชิงทฤษฎีคลาสสิก (แบบจำลองภูมิอากาศปะติดปะต่อจากทฤษฎี การประมาณเชิงตัวเลข และพารามิเตอร์ที่ปรับด้วยมือโดยไม่มีสมการเดี่ยวใดรับรอง) วินส์เบิร์กเรียกมันว่าหมวดหมู่เชิงญาณวิทยาที่แยกออกมาต่างหาก: เราไว้ใจการจำลองหนึ่งเพราะไว้ใจวิธีสร้างแบบจำลองนั้น — ฟิสิกส์ที่มันเข้ารหัสไว้ กลเม็ดที่ทำให้สมการซึ่งแก้ไม่ได้กลายเป็นแก้ได้ ประวัติผลงานของแบบจำลองคล้ายกันในกรณีที่คุณตรวจสอบได้ — ไม่ใช่เพราะไว้ใจว่าวัตถุที่ถูกจำลองกับวัตถุจริงเป็น "ระบบชนิดเดียวกัน" ในความหมายของผู้ทดลอง การจำลองเส้นทางเฮอริเคนไม่ใช่การสังเกตเฮอริเคน และไม่ใช่บทพิสูจน์เกี่ยวกับมัน มันคือสิ่งที่สาม หลักฐานที่ถูกสร้างขึ้น ไม่ใช่ถูกพบเจอ
The third principle is opacity, and it cuts a line straight through modern computing. Humphreys coined "epistemic opacity" for processes in which not all the elements relevant to a result's justification are, even in principle, available to the epistemic agent making use of it (Extending Ourselves: Computational Science, Empiricism, and Scientific Method, Oxford University Press, 2004). A traditionally written program is transparent in a specific sense: however long, its logic is in principle inspectable, line by line, by a competent reader. A trained neural network is opaque in a different sense: its "reasons" are distributed across millions or billions of weighted connections that were never designed, only grown by gradient descent, and no human — not even its authors — can trace why one output rather than another emerged. This bears directly on machine testimony: when a diagnostic model flags a tumor, is that a report from a reasoning entity, to be weighed the way we weigh a colleague's judgment, or a reading, to be weighed the way we weigh a thermometer's? The two carry different epistemic weight, and opaque systems make it uncomfortably hard to tell which one you are getting.
หลักการที่สามคือความทึบ (opacity) และมันผ่ากลางวงการคำนวณสมัยใหม่เป็นเส้นตรง ฮัมฟรีส์บัญญัติคำว่าความทึบเชิงญาณวิทยา (epistemic opacity) ไว้ใช้กับกระบวนการที่องค์ประกอบซึ่งเกี่ยวข้องกับการให้เหตุผลรองรับผลลัพธ์ไม่ได้เปิดให้ผู้รู้ (epistemic agent) ที่ใช้มันเข้าถึงได้ครบ แม้ในหลักการ (Extending Ourselves: Computational Science, Empiricism, and Scientific Method, Oxford University Press, 2004) โปรแกรมที่เขียนแบบดั้งเดิมโปร่งใสในความหมายเฉพาะอย่างหนึ่ง: จะยาวแค่ไหนก็ตาม ตรรกะของมันเปิดให้ผู้อ่านที่มีความสามารถตรวจทีละบรรทัดได้ในหลักการ โครงข่ายประสาทเทียมที่ผ่านการฝึกทึบคนละแบบ: "เหตุผล" ของมันกระจายอยู่ในการเชื่อมต่อถ่วงน้ำหนักเป็นล้านหรือพันล้านจุด ที่ไม่มีใครออกแบบ มีแต่ปลูกขึ้นด้วย gradient descent และไม่มีมนุษย์คนใด — ผู้สร้างมันเองก็ด้วย — ตามรอยได้ว่าทำไมเอาต์พุตนี้จึงโผล่ออกมาแทนอีกอันหนึ่ง เรื่องนี้กระทบคำให้การ (testimony) ของเครื่องจักรโดยตรง: เมื่อแบบจำลองวินิจฉัยตีธงว่าพบเนื้องอก นั่นคือรายงานจากสิ่งที่ให้เหตุผลได้ ที่ต้องชั่งน้ำหนักอย่างที่เราชั่งคำตัดสินของเพื่อนร่วมงาน หรือคือการอ่านค่า ที่ต้องชั่งอย่างที่เราชั่งตัวเลขจากเทอร์โมมิเตอร์ สองอย่างนี้แบกน้ำหนักเชิงญาณวิทยา (epistemic weight) ไม่เท่ากัน และระบบทึบทำให้บอกได้ยากอย่างอึดอัดว่าคุณกำลังได้อันไหน
The fourth principle replays an old civil war under new names: program verification versus testing, rationalism versus empiricism. In May 1979, Richard De Millo, Richard Lipton, and Alan Perlis published "Social Processes and Proofs of Theorems and Programs" (Communications of the ACM 22, no. 5: 271–280), arguing that mathematical certainty rests on a social process — peers checking, re-deriving, and eventually trusting a proof — that program verification could never replicate at scale, because no comparable community will re-verify a million-line formal proof of a shipped product. James Fetzer's 1988 "Program Verification: The Very Idea" (Communications of the ACM 31, no. 9: 1048–1063) sharpened the objection into a philosophical claim: algorithms, as abstract logical structures, admit deductive proof; programs, as physical processes running on real, occasionally faulty hardware, do not, because no deduction can certify that silicon will behave as its specification assumes. The verificationist's rationalist ideal — prove it once, know it forever — meets the tester's empiricist reply, distilled by Edsger Dijkstra a decade earlier: "Program testing can be used to show the presence of bugs, but never to show their absence" ("Notes on Structured Programming," EWD249, 1970). Neither side has won; software ships today on some blend of both, verified where it is cheap enough, tested everywhere else.
หลักการที่สี่คือสงครามกลางเมืองเก่าที่เล่นซ้ำภายใต้ชื่อใหม่: การพิสูจน์ความถูกต้องของโปรแกรม (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) ไม่มีฝ่ายใดชนะ ซอฟต์แวร์ทุกวันนี้ส่งมอบด้วยส่วนผสมของทั้งสอง พิสูจน์ความถูกต้องตรงที่ราคาถูกพอ ทดสอบในที่เหลือทั้งหมด
The fifth principle is the oldest trap in epistemology, wearing a sensor's housing. Edmund Gettier's three-page 1963 paper, "Is Justified True Belief Knowledge?" (Analysis 23, no. 6: 121–123), showed that a belief can be justified and true and still fail to be knowledge, when the justification and the truth connect only by luck — the classic image is a stopped clock that happens to show the correct time. Automated pipelines manufacture this structure routinely: a facial-recognition system with a genuine bug — miscalibrated, say, on faces at a certain angle — can still output the correct match on a given frame, by accident, while carrying all the institutional justification ("this system is 99% accurate") that would normally certify a belief as knowledge. The output is true, and reasonably trusted, and arrived at by a process that, on that occasion, was not doing what its justification assumed it was doing. Gettier's stopped clock now has cameras.
หลักการที่ห้าคือกับดักที่เก่าที่สุดในญาณวิทยา สวมเปลือกเซนเซอร์มา บทความสามหน้าของเอ็ดมันด์ เก็ตติเยร์ปี 1963 "Is Justified True Belief Knowledge?" (Analysis 23, no. 6: 121–123) แสดงว่าความเชื่อหนึ่งมีเหตุผลรองรับและเป็นจริงพร้อมกันได้ โดยยังไม่ใช่ความรู้ ถ้าเหตุผลรองรับกับความจริงบรรจบกันด้วยความบังเอิญ — ภาพคลาสสิกคือนาฬิกาหยุดเดินที่บังเอิญบอกเวลาถูก สายพานอัตโนมัติผลิตโครงสร้างแบบนี้ออกมาเป็นประจำ: ระบบจดจำใบหน้าที่มีบั๊กจริง สมมติว่าปรับเทียบผิดกับใบหน้ามุมหนึ่ง ยังให้ผลจับคู่ที่ถูกต้องบนเฟรมหนึ่งได้โดยบังเอิญ ทั้งที่แบกเหตุผลรองรับเชิงสถาบันเต็มชุด ("ระบบนี้แม่นยำ 99%") ซึ่งตามปกติจะรับรองความเชื่อหนึ่งให้เป็นความรู้ ผลลัพธ์นั้นเป็นจริง ไว้วางใจได้อย่างสมเหตุสมผล และมาจากกระบวนการที่ในโอกาสนั้นไม่ได้ทำสิ่งที่เหตุผลรองรับของมันสมมติว่ามันทำ นาฬิกาหยุดเดินของเก็ตติเยร์ตอนนี้มีกล้อง
The people, briefly. Appel and Haken took considerable heat for a proof many still call inelegant rather than false. Humphreys and Winsberg built an entire subfield — the philosophy of computer simulation — out of taking seriously a method working scientists had already trusted for decades without asking what kind of evidence it was. Fetzer's 1988 paper triggered pages of technical correspondence within a year and a debate still cited today — one of the longest-running controversies Communications of the ACM ever printed.
ผู้คน โดยย่อ แอปเพลกับฮาเคนโดนวิจารณ์หนักพอสมควร สำหรับบทพิสูจน์ที่หลายคนยังเรียกว่าไม่สง่างาม มากกว่าจะเรียกว่าผิด ฮัมฟรีส์กับวินส์เบิร์กสร้างสาขาย่อยขึ้นมาทั้งสาขา — ปรัชญาแห่งการจำลองด้วยคอมพิวเตอร์ — จากการเอาจริงกับวิธีที่นักวิทยาศาสตร์หน้างานไว้ใจมาหลายสิบปีโดยไม่เคยถามว่ามันเป็นหลักฐานชนิดไหน บทความปี 1988 ของเฟตเซอร์จุดชนวนจดหมายโต้ตอบเชิงเทคนิคหลายหน้าภายในหนึ่งปี และการถกเถียงที่ยังถูกอ้างถึงทุกวันนี้ — หนึ่งในข้อขัดแย้งที่ยืนยาวที่สุดเท่าที่ Communications of the ACM เคยพิมพ์
Connections
เชื่อมโยง
Chapter 01 supplies the proof-theoretic background — soundness, completeness, and Gödel's limits — that surveyability quietly assumes. Chapter 09 asks what undecidability licenses philosophically, a companion question to what unsurveyable proof licenses here. Chapter 13 returns to opacity from the learning side: interpretability research as a laboratory for finding out what, if anything, is inside the black box.
บทที่ 01 วางพื้นหลังเชิงทฤษฎีบทพิสูจน์ — ความสมเหตุสมผลเชิงตรรกะ ความสมบูรณ์ และขีดจำกัดของเกอเดิล — ที่ surveyability สมมติไว้เงียบๆ บทที่ 09 ถามว่าการตัดสินไม่ได้ (undecidability) อนุญาตให้อ้างอะไรได้บ้างในเชิงปรัชญา เป็นคำถามคู่กับสิ่งที่บทพิสูจน์ซึ่งตรวจสอบทั้งหมดไม่ได้อนุญาตให้อ้างในบทนี้ บทที่ 13 กลับมาที่ความทึบจากฝั่งการเรียนรู้: งานวิจัย interpretability ในฐานะห้องทดลองที่ไว้ค้นว่ามีอะไรอยู่ในกล่องดำ ถ้ามี
Open questions
คำถามที่ยังเปิดอยู่
If a proof can be certain but not surveyable, has "proof" quietly changed meaning since Euclid, or did it always mean "warranted to the standards of the day" and Euclid's standards were simply stricter than ours by accident of history? And is machine opacity a temporary engineering limitation interpretability research will eventually dissolve, or a permanent structural feature of any system whose "knowledge" is distributed statistically rather than written down as rules?
ถ้าบทพิสูจน์หนึ่งแน่นอนได้โดยตรวจสอบทั้งหมดไม่ได้ คำว่า "บทพิสูจน์" เปลี่ยนความหมายไปเงียบๆ ตั้งแต่ยุคยูคลิดหรือไม่ หรือมันแปลว่า "ได้รับการรับรองตามมาตรฐานของยุคนั้น" มาตลอด และมาตรฐานของยูคลิดก็แค่เข้มกว่าของเราด้วยความบังเอิญทางประวัติศาสตร์ และความทึบของเครื่องจักรเป็นข้อจำกัดเชิงวิศวกรรมชั่วคราวที่งานวิจัย interpretability จะสลายมันได้ในที่สุด หรือเป็นคุณลักษณะเชิงโครงสร้างถาวรของระบบใดๆ ที่ "ความรู้" ของมันกระจายอยู่เชิงสถิติ แทนที่จะถูกเขียนไว้เป็นกฎ
Go deeper
อ่านต่อ
- Eric Winsberg, Science in the Age of Computer Simulation, University of Chicago Press, 2010 — the founding case for simulation as its own epistemic category.
- 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, Stanford Encyclopedia of Philosophy.
- 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)