"พิสูจน์" Collatz ที่ AI ช่วยเขียน กลายเป็นบั๊ก soundness ใน Lean kernel — Leo de Moura เผยแพร่ postmortem #14576

เมื่อวานนี้เราเขียนถึง เปเปอร์ ten-proofs ของ OpenAI ที่จุดขายหลักคือ “ทุกผลลัพธ์แนบ Lean 4 certificate มาให้ตรวจเอง” — ตรรกะคือ ต่อให้ไม่เชื่อแล็บ ก็ยังเชื่อ kernel ได้ วันที่ 1 สิงหาคม 2026 Leonardo de Moura ผู้สร้าง Lean และ Chief Architect ของ Lean FRO เผยแพร่ postmortem ที่เป็นอีกด้านของเหรียญเดียวกัน: kernel เองก็มีบั๊กได้ และ AI เก่งเรื่องหามันเจอ

เรื่องเริ่มวันที่ 25 กรกฎาคม เมื่อ Ramana Kumar เผยแพร่รีโปที่มี “disproof” ของ Collatz conjecture — ปราศจาก sorry ทั้งไฟล์ ผ่าน type checker เรียบร้อย และเขียนขึ้นด้วยความช่วยเหลือของ AI ปัญหาคือมันไม่ได้พิสูจน์อะไรเลย มันไป เจาะบั๊กในการจัดการ nested inductive types ของ kernel ต่างหาก

บั๊กคืออะไร และทำไมมันร้ายแรง

de Moura อธิบายไว้ตรง ๆ: เมื่อ kernel ทำ elimination บน nested occurrence ภายใต้ inductive type T ที่มีพารามิเตอร์ Ds และพารามิเตอร์เหล่านั้นเป็น phantom (ไม่ถูกอ้างถึงในฟิลด์ของ constructor เลย) พารามิเตอร์พวกนี้จะหายไปจาก auxiliary type ที่ถูก generate ขึ้นมา — และเมื่อหายไป มันก็เลย หลุดจากการตรวจ type ผลคือสามารถยัด argument ที่ ill-typed เข้าไปตำแหน่งนั้น แล้วทำให้ kernel ยอมรับ proof of False ได้ ซึ่งใน logic แปลว่าพิสูจน์อะไรก็ได้

สองข้อจำกัดสำคัญที่ postmortem ย้ำ:

• เข้าถึงได้ผ่าน metaprogramming เท่านั้น — ต้องส่ง inductive declaration เข้า kernel ตรง ๆ เพราะ frontend ตรวจ argument แล้วดักเทอมที่ ill-typed ได้อยู่
• เป็นบั๊กระดับ implementation ไม่ใช่ช่องโหว่ใน meta-theory ของ Lean — ทฤษฎีไม่พัง โค้ดพัง

ไทม์ไลน์การแก้เร็วมาก: 28 กรกฎาคม Kiran Gopinathan ย่อเคสให้เหลือ proof of False ขนาดเล็กแล้วเปิด issue #14576 (ชื่อ issue: “Kernel accepts wrong-structure projections, allowing an axiom-free proof of False”) — de Moura push แพตช์ #14577 หลังรายงานหนึ่งชั่วโมง Joachim Breitner รีวิวและเสนอปรับปรุง แล้วเมิร์จเข้าในวันเดียวกัน patch release ออกตามมาเป็น v4.32.2 เย็นวันที่ 28 กรกฎาคม

จุดที่น่ากลัวกว่า: สองบั๊กในสองระบบพร้อมกัน

วิธีปฏิบัติมาตรฐานของสาย formal verification คือ ตรวจซ้ำด้วย kernel อิสระ — ตัวหลักคือ nanoda ซึ่ง Chris Bailey เขียนใหม่ด้วย Rust แยกจาก implementation ทางการโดยสิ้นเชิง

แต่รีโป Collatz ต้นฉบับ ผ่าน nanoda เวอร์ชันเก่าอายุหนึ่งสัปดาห์ด้วย — และเหตุผลคือสิ่งที่ de Moura เรียกว่า “the surprising part”: มันคือ บั๊กสองตัวที่ไม่เกี่ยวกันเลย kernel ทางการพลาดการตรวจใน nested inductive type ส่วน nanoda ตรวจจุดนั้นได้ แต่ไม่ได้ตรวจชื่อ type ใน projection node — และ proof ถูกประกอบขึ้นมาให้เทอมที่ kernel ทางการไม่เคยมองเข้าไป เป็นเทอมเดียวกับที่ nanoda เวอร์ชันเก่ายอมรับพอดี

บั๊กของ nanoda ถูก Jeremy Chen รายงานและแก้ไปแล้ว หนึ่งสัปดาห์ก่อนบั๊กของ Lean จะถูกรายงาน Ramana เชื่อว่าจังหวะเวลานี้เป็นเรื่องบังเอิญ แต่ก็ยอมรับว่าตัดความเป็นไปได้ที่โมเดลเคยเห็นรายงานของ nanoda ไม่ได้ ขณะที่ Breitner เสนออีกสมมติฐาน: จังหวะที่พ้องกันเกิดจากการที่โมเดลแรง ๆ พร้อมใช้งานแล้วต่างหาก

บทเรียนเชิงปฏิบัติที่ postmortem สรุปไว้: การตรวจด้วย kernel อิสระ ยังใช้ได้อยู่ เพราะการเจาะสำเร็จต้องอาศัยบั๊กคนละตัวใน implementation สองตัวพร้อมกัน — แต่คนที่พึ่งวิธีนี้ต้อง อัปเดตทั้งสองฝั่งให้เป็นเวอร์ชันล่าสุด ส่วน lean4lean ของ Mario Carneiro ได้รับผลกระทบด้วย เพราะการจัดการ inductive ของมันเป็น port มาจาก reference implementation โดยตรง (งานพิสูจน์ consistency ของ lean4lean ยังไม่ครอบคลุมส่วน inductive types — de Moura บอกว่าบั๊กนี้จะถูกเจอเองอยู่ดีตอนทำส่วนนั้นให้จบ)

“เอา metaprogramming ออกสิ” — de Moura บอกว่าคิดผิด

ข้อเสนอที่โผล่ในวงถกเถียงคือ ถ้าช่องโหว่นี้เข้าถึงได้ผ่าน metaprogramming เท่านั้น ก็ตัดหรือจำกัด metaprogramming ทิ้งไปเลยสิ de Moura ตอบว่านี่ misguided และเหตุผลของเขาน่าจดไว้:

elaborator ถูกออกแบบมาให้ untrusted อยู่แล้ว — soundness จะไปขึ้นกับการที่ component ที่ไม่น่าเชื่อถือ “ยอมปฏิเสธ” เทอมแย่ ๆ ให้ไม่ได้

คนที่ตั้งใจจะส่ง proof ปลอมเข้ามา เขียนไฟล์ .olean เองตรง ๆ ก็ได้ หรือแก้หน่วยความจำก็ได้ ทั้งสองทางข้าม elaborator ไปเลย kernel ต้องปฏิเสธ declaration ที่ ill-typed ได้ด้วยตัวเอง ใน process ของตัวเอง — และการแยกหน้าที่แบบนี้คือข้อได้เปรียบหลักข้อหนึ่งของสถาปัตยกรรมแบบ proof term

Lean FRO ทำอะไรต่อ — และท่อนที่เชื่อมกลับไปหา OpenAI

มาตรการที่ประกาศในโพสต์:

• Regression test ของ exploit นี้ และของเคส non-uniform parameter ที่ Arthur Adjedj ยกขึ้นมา ถูกใส่ไว้ใน Kernel Arena แล้ว
• PR #14582 ทำให้ kernel ตรวจว่าพารามิเตอร์ของ nested occurrence ทำตัวเป็นพารามิเตอร์จริง ๆ ไม่ใช่แค่ type-check ซ้ำเฉย ๆ
• hardening invariant ของ kernel เพิ่มอีกชุด: PR #14621, #14631, #14632
• Comparator ตอนนี้ รัน nanoda เป็นค่าเริ่มต้น และ nanoda ถูก track รายวัน เพื่อให้ lean-eval กับ comparator ตามแพตช์ upstream ทัน

และท่อนที่น่าสนใจที่สุดสำหรับคนอ่านข่าว AI: Daniel Selsam จาก OpenAI เข้ามาช่วย Lean FRO ด้วย AI เฉพาะทางด้าน cybersecurity แล้วเจอบั๊กเพิ่มอีกหลายตัวใน kernel — แก้หมดแล้วทุกตัวผ่าน PR #14607, #14608, #14609, #14613, #14615, #14616 ทุกตัวเข้าถึงได้ผ่าน metaprogramming เหมือนกัน และ nanoda จับได้ทุกตัว

ปิดท้าย de Moura บอกว่ากำลังติดต่อและสนับสนุนผู้เชี่ยวชาญที่จะมาหาบั๊กเพิ่ม สร้าง kernel ตัวใหม่ และทำงานฝั่งทฤษฎีหรือ verified kernel ต่อ

มุมมอง AI Curator

สองข่าวนี้ต้องอ่านคู่กัน และมันไม่ได้ขัดกันอย่างที่ดูเผิน ๆ

เมื่อวาน OpenAI ขายไอเดียว่า Lean certificate = ไม่ต้องเชื่อใจแล็บ วันนี้ผู้สร้าง Lean บอกว่า kernel ที่คุณเชื่อนั้นเพิ่งมีบั๊กที่ทำให้พิสูจน์ False ได้ คนจะรีบสรุปว่า “เห็นไหม formal verification ก็เชื่อไม่ได้” — ซึ่งเป็นข้อสรุปที่ผิด สิ่งที่เกิดขึ้นจริงคือ ระบบทำงานถูกตามที่ออกแบบไว้: มีคนเจอ มีคนย่อเป็นเคสเล็ก เปิด issue ได้แพตช์ในหนึ่งชั่วโมง ออก patch release ในวันเดียวกัน แล้วเผยแพร่ postmortem ที่บอกทุกอย่างรวมถึงส่วนที่น่าอาย ลองเทียบกับสิ่งที่เกิดขึ้นเวลาโมเดล LLM ตอบผิด — ไม่มี issue tracker ไม่มีเลข PR ไม่มี patch release ที่บอกได้ว่า “เวอร์ชันนี้แก้แล้ว” trust base ของ Lean เล็กพอที่จะแก้ได้ในหนึ่งชั่วโมง นั่นแหละคือคุณค่าทั้งหมดของมัน

แต่ประเด็นที่ผมคิดว่าสำคัญกว่าและถูกพูดถึงน้อยเกินไปคือ ราคาของ “เชื่อได้” เพิ่งขึ้น เดิมทีธรรมเนียม “ตรวจซ้ำด้วย kernel อิสระ” ถือเป็นเกราะที่แข็งพอ เพราะสมมติฐานเงียบ ๆ ของมันคือ ไม่มีใครหาบั๊กที่ตรงกันในสอง implementation พร้อมกันได้ เคสนี้ไม่ได้ล้มสมมติฐานนั้นเสียทีเดียว (มันไม่ใช่บั๊กเดียวที่ทะลุทั้งสอง แต่เป็นสองบั๊กที่บังเอิญประกบกันพอดี) แต่มันแสดงให้เห็นว่า search process ที่มีโมเดลแรง ๆ อยู่เบื้องหลัง เดินไปในมุมของ input space ที่มนุษย์ไม่เคยเดินเข้าไป สมมติฐานของ Breitner ที่ว่า “จังหวะที่พ้องกันเกิดจากการมีโมเดลที่หาบั๊กนี้เจอ” คือคำอธิบายที่ประหยัดที่สุด และเป็นคำเตือนที่ตรงที่สุด — พร้อมกับข้อเท็จจริงที่ว่า OpenAI ต้องส่ง AI ด้าน cybersecurity มาช่วยกวาดบั๊กที่เหลือ

สำหรับนักพัฒนาไทยที่กำลังคิดจะเอา proof assistant มาใช้จริง — ในงาน smart contract, ระบบการเงิน, หรือ safety-critical — บทเรียนปฏิบัติมีสามข้อ: (1) pin เวอร์ชัน toolchain แล้วอัปเดตเมื่อมี patch release เพราะ v4.32.2 คือเส้นแบ่งของเคสนี้ (2) ถ้าใช้ external checker เป็นเกราะ ต้องอัปเดตทั้งสองฝั่ง ไม่ใช่แค่ฝั่งเดียว — รีโป Collatz ผ่าน nanoda ได้เพราะ nanoda ที่ใช้เก่าไปหนึ่งสัปดาห์เท่านั้น และ (3) เวลาเห็น “AI พิสูจน์ทฤษฎีบทได้” ให้ถามต่อว่า ตรวจด้วย kernel เวอร์ชันไหน ไม่ใช่แค่ “ตรวจแล้วหรือยัง”

และข้อสังเกตสุดท้ายที่กลืนยากหน่อย: สิ่งที่ทำให้เรื่องนี้เป็นข่าว ไม่ใช่ว่า Lean มีบั๊ก ซอฟต์แวร์ทุกตัวมีบั๊ก แต่คือ เครื่องมือที่เราตั้งใจใช้เป็น “ผู้ตัดสินความจริง” ในยุคที่ AI ผลิตข้ออ้างเร็วกว่ามนุษย์ตรวจไหว กำลังกลายเป็นเป้าโจมตีที่มีมูลค่า ตราบใดที่การมี Lean certificate แปลว่าได้รับความเชื่อถือฟรี ๆ ก็จะมีคน (และโมเดล) ที่หาทางได้ certificate โดยไม่ต้องพิสูจน์อะไรจริง ๆ Lean FRO เพิ่งเจอเวอร์ชันแรกของแรงกดดันนั้น และรับมือได้ดีมาก คำถามคือทีมงานขนาดไม่กี่สิบคนจะรับแรงกดดันแบบนี้ไหวไปอีกนานแค่ไหน

แหล่งข่าว

• Postmortem for Kernel Soundness Bug #14576 — Leonardo de Moura, 1 ส.ค. 2026
• leanprover/lean4 issue #14576 — Kernel accepts wrong-structure projections, allowing an axiom-free proof of False
• leanprover/lean4 PR #14577 — fix: missing check at kernel inductive declaration
• Lean 4 releases — v4.32.2 (28 ก.ค. 2026)
• Why is it all in the kernel? — Lawrence Paulson, 30 ก.ค. 2026