โปรเจกต์ชื่อ verified-3d-mesh-intersection ยกทั้งงานเขียนโค้ดและงานพิสูจน์ความถูกต้องให้ AI ทำ แล้วเหลือให้คนรีวิวอ่านเองแค่ 93 บรรทัด

โค้ดกว่า 1,000 บรรทัดกับบทพิสูจน์อีกกว่า 60,000 บรรทัดกลายเป็นส่วนที่ไม่มีใครอ่าน เพราะทั้งสองก้อนวางไว้เป็นกล่องดำตั้งแต่ต้นจนจบ บทพิสูจน์ในที่นี้คือการไล่แสดงทีละขั้นว่าโค้ดทำงานตรงตามที่สั่งไว้จริง ส่วน 93 บรรทัดนั้นไม่ใช่การกวาดตาผ่านๆ แต่เป็นการอ่านครบทุกบรรทัดที่ต้องเชื่อใจ

ถ้าใครเคยสั่ง AI เขียนฟีเจอร์ แล้วได้โค้ดกลับมาเป็นพันบรรทัดในไม่กี่นาที ก็น่าจะคุ้นเคยกับสิ่งที่เกิดขึ้นต่อจากนั้นดี คือการเลื่อนดูผ่านๆ ไม่กี่หน้าจอ พอเห็นว่ารันได้และเทสต์เขียวหมด ก็กดรวมเข้าโปรเจกต์ทันที เหตุผลไม่ใช่เพราะขี้เกียจอ่าน แต่เป็นเพราะ AI พิมพ์ออกมาเร็วกว่าที่คนจะอ่านทันมานานแล้ว

ผู้พัฒนาที่ใช้ชื่อ schildep เผยแพร่งานชิ้นนี้บน GitHub โดยตั้งใจให้เป็นการทดลองตรงๆ ว่า เราจะใช้โค้ดที่ AI เขียนโดยไม่ต้องเชื่อใจมันเลยได้ไหม

งานตัดวัตถุสามมิติ ความยากที่ซ่อนอยู่ในเคสประหลาด

งานที่ verified-3d-mesh-intersection ทำ เป็นงานเรขาคณิตพื้นฐานของโปรแกรมสามมิติ ในโลกของโมเดลสามมิติ วัตถุหนึ่งก้อนประกอบขึ้นจากผิวสามเหลี่ยมเล็กๆ จำนวนมากที่ต่อกันจนปิดสนิท เรียกกันว่า mesh ส่วน mesh intersection คือการนำวัตถุสองก้อนมาวางซ้อนกัน แล้วเก็บไว้เฉพาะเนื้อที่อยู่ในทั้งสองก้อนพร้อมกัน ที่เหลือตัดทิ้งทั้งหมด

ฟังดูเหมือนงานง่าย แต่สิ่งที่ทำให้ซับซ้อนคือเคสประหลาดที่เกิดขึ้นได้จริง เช่น มุมของก้อนหนึ่งไปวางแตะพอดีกับขอบสามเหลี่ยมของอีกก้อน หรือผิวสองชิ้นแนบสนิทกันโดยไม่ทะลุเข้าไป โปรแกรมที่ใช้งานจริงต้องเขียนโค้ดรับมือเคสเหล่านี้เป็นรายกรณี จนกลายเป็นโค้ดหลักพันบรรทัด ทั้งที่โจทย์อธิบายจบได้ในประโยคเดียว

โปรเจกต์นี้มีเดโมบนเว็บ ให้ลองตัดโมเดลในเบราว์เซอร์ได้เอง โดยเลือกใช้โมเดลตัวอย่างที่เตรียมไว้ หรือจะอิมพอร์ตไฟล์โมเดลสามมิติของตัวเองเข้าไปตัดก็ได้ โค้ดที่ผ่านการพิสูจน์แล้วจะคอมไพล์มารันอยู่ในเครื่องของผู้ใช้โดยตรง ไม่ได้ส่งข้อมูลออกไปที่เซิร์ฟเวอร์

93 บรรทัดที่ต้องอ่าน กับตัวตรวจที่ทำงานแทนสายตา

93 บรรทัดที่ว่านี้ไม่ใช่โค้ดที่ทำงานจริง แต่เป็นสเปก หรือคำอธิบายว่าผลลัพธ์ที่ถูกต้องควรมีหน้าตาอย่างไร โดยเขียนในรูปแบบที่เครื่องอ่านและตรวจได้ สเปกชุดนี้กระจายอยู่ใน 3 ไฟล์ นับเฉพาะบรรทัดที่ไม่ใช่คอมเมนต์รวมกันได้ 93 บรรทัดพอดี

ใจความหลักของสเปกสั้นกว่าที่คิด ผลลัพธ์ต้องมีเนื้อเท่ากับส่วนที่วัตถุสองก้อนซ้อนทับกันพอดีโดยไม่ขาดไม่เกิน พร้อมเงื่อนไขว่าผลลัพธ์ต้องเป็นโมเดลที่นำไปใช้ต่อได้ คือผิวต้องปิดสนิท ไม่มีรูรั่ว ไม่มีสามเหลี่ยมแบนจนไม่เหลือเนื้อที่ และไม่มีผิวที่ทะลุตัวเอง

ส่วนเครื่องมืออีกฝั่งคือ Lean 4 ภาษาโปรแกรมที่เขียนบทพิสูจน์ทางคณิตศาสตร์ลงไปพร้อมกับโค้ดได้ ภาษานี้มีตัวตรวจที่คอยไล่เช็กบทพิสูจน์ทีละขั้น หากพิสูจน์ไม่ครบ โปรแกรมจะคอมไพล์ไม่ผ่านตั้งแต่แรก ดังนั้น เมื่อโปรเจกต์นี้คอมไพล์ผ่าน จึงไม่ได้บอกแค่ว่าโค้ดรันได้ แต่ยืนยันว่ามีบทพิสูจน์ครบถ้วนแล้วว่าโค้ดทำงานตรงตามสเปกที่คนอ่านไปแล้ว

ผู้รีวิวจึงเหลืองานเพียงสองอย่าง คืออ่านสเปก 93 บรรทัดว่าตรงตามต้องการหรือยัง จากนั้นจึงกดรันตัวตรวจของ Lean จนจบ ส่วนโค้ดกว่า 1,000 บรรทัดใน CSG/Impl/ และบทพิสูจน์อีกกว่า 60,000 บรรทัดใน CSG/Proof/ สามารถข้ามได้ทั้งหมด เพราะไม่มีจุดไหนที่ต้องยอมเชื่อคำพูดของโมเดลตัวไหนอีกเลย

สเปกเดียวกัน เขียนแบบปกติ เหลือบั๊ก 3 จุด

สิ่งที่ทำให้เรื่องนี้ต่างจากการเปลี่ยนภาษาโปรแกรมทั่วไป คือความครอบคลุม การเขียนเทสต์บอกได้เพียงว่าฟังก์ชันทำงานถูกต้องกับอินพุตที่เราหยิบมาลอง แต่บทพิสูจน์ยืนยันได้ว่าโค้ดทำงานถูกต้องกับอินพุตทุกแบบที่เป็นไปได้ รวมถึงเคสที่นึกไม่ออกตอนนั่งเขียนเทสต์

ผู้พัฒนาจึงทำเวอร์ชันเปรียบเทียบขึ้นมาเพื่อแสดงให้เห็นว่าส่วนต่างตรงนี้สำคัญแค่ไหน โดยนำสเปกชุดเดิมมาเขียนใหม่เป็นภาษาคนธรรมดา แล้วส่งให้โมเดล Claude Opus 4.8 ลงมือทำเวอร์ชัน C++ ขึ้นมา ผลลัพธ์ที่ได้คือโค้ดยาวกว่า 1,000 บรรทัดพอๆ กัน โดย AI ตัวนั้นเขียนยูนิตเทสต์ของตัวเอง และไล่แก้โค้ดจนเทสต์ผ่านทั้งหมด

จากนั้น ผู้พัฒนาส่ง agent อีกตัวมาไล่เทียบโค้ด C++ ก้อนนั้นกับเวอร์ชัน Lean ที่พิสูจน์แล้ว โดย agent ในที่นี้หมายถึง AI ที่รับโจทย์ไปทำงานต่อเนื่องได้หลายขั้น คนไม่ต้องคอยสั่งทีละคำสั่ง ผลลัพธ์คือ agent เจอบั๊กคนละจุดกันรวม 3 จุด และสามารถสร้างอินพุตเฉพาะชุดมาทำซ้ำให้เห็นบั๊กจริงได้ด้วย

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

ผู้พัฒนาระบุเองว่า ทั้งสามจุดนี้แทบเป็นไปไม่ได้เลยที่จะจับได้ด้วยการทดสอบแบบมองผลลัพธ์จากข้างนอก และต่อให้ใช้ agent หลายตัวผลัดกันรีวิวโค้ดจนเจอ ก็ไม่มีทางรู้ได้อยู่ดีว่ายังมีบั๊กตัวที่ 4 หลงเหลืออยู่หรือไม่

จุดนี้เองที่ทำให้คำพูดว่า 'เดี๋ยวอ่านเองก็ได้' เริ่มฟังไม่ขึ้น และในระดับองค์กรก็เริ่มมีคำถามคล้ายกันเกิดขึ้น เช่นข้อเสนอที่มองว่าปัญหาอยู่ที่องค์กรไม่มีระบบตัดสินใจ ไม่ใช่ที่ตัว AI

คุมแค่สเปก แล้วปล่อยที่เหลือให้ agent

ขั้นตอนการทำงานระหว่างพัฒนาเป็นส่วนที่เรานำไปปรับใช้กับงานอื่นได้แม้จะไม่เคยแตะ Lean เลย โดยมีหลักการง่ายๆ คือ คนถือสเปกไว้เพียงชิ้นเดียว แล้วปล่อยให้ agent รับผิดชอบทั้งตัวโค้ดและบทพิสูจน์ทั้งหมด

การพัฒนาเริ่มจากสเปกเวอร์ชันง่ายที่ประเมินว่าน่าจะพิสูจน์ได้ไม่ยาก แล้วปล่อยให้ agent ทำงานจนผ่าน จากนั้นค่อยๆ เพิ่มเงื่อนไขทีละขั้น ขั้นแรกสั่งให้ agent แปลงกรอบคณิตศาสตร์จากงานวิจัยปี 1998 ให้อยู่ในรูปแบบที่เครื่องตรวจได้ ขั้นถัดมาจึงขอโค้ดที่ทำงานได้จริงพร้อมบทพิสูจน์ แล้วไล่เพิ่มข้อกำหนดเรื่องคุณภาพของผลลัพธ์ สุดท้ายจึงถอดข้อผ่อนปรนที่ยอมให้อินพุตวางในท่าง่ายๆ ออก เพื่อบังคับให้ agent รับมือเคสประหลาดทุกแบบด้วยตัวเอง

อีกขั้นตอนที่แสดงประโยชน์ของวิธีนี้ได้ชัดเจนคือตอนสั่งให้ agent ปรับโค้ดให้ทำงานเร็วขึ้น เนื่องจากสเปกเดิมไม่ได้เปลี่ยน เมื่อ Lean ตรวจผ่านอีกรอบ ก็ยืนยันได้ทันทีว่าโค้ดเวอร์ชันใหม่ยังคงถูกต้องตามสเปกเดิม คนรีวิวจึงไม่ต้องกลับไปตรวจความถูกต้องซ้ำอีก ทั้งที่โค้ดข้างในเปลี่ยนไปเยอะมาก

อีกขั้นตอนที่ขาดไม่ได้เมื่อปล่อยให้ agent เขียนบทพิสูจน์เอง คือการเช็กว่ามันไม่ได้แอบเปิดทางลัดไว้ เพราะ agent อาจใส่ข้อตั้งต้นใหม่ที่ยอมรับกันโดยไม่ต้องพิสูจน์เข้ามาเอง หรือสั่งให้ตอนคอมไพล์ไปเรียกฟังก์ชันอื่นแทนตัวที่พิสูจน์แล้ว โดยคำสั่งที่ใช้ปิดช่องโหว่นี้มีสองคำสั่งคือ

lake build
rg -n 'implemented_by|extern|csimp|skipKernelTC|unsafe|partial|opaque' CSG/

คำสั่งแรกให้ตัวตรวจไล่เช็กบทพิสูจน์ทั้งชุด ส่วนคำสั่งค้นหาคีย์เวิร์ดต้องได้ผลลัพธ์ว่าไม่พบเลยสักบรรทัด จึงจะมั่นใจได้ว่าไม่มีการแอบสลับโค้ดตอนคอมไพล์ นอกจากนี้ เรายังตรวจสอบได้ว่าทฤษฎีบทที่สนใจพึ่งพาข้อตั้งต้นตัวไหนบ้าง ซึ่งในโปรเจกต์นี้ระบุว่าพึ่งพาเพียงข้อตั้งต้นมาตรฐาน 3 ตัวของ Lean เท่านั้น ได้แก่ propext · Classical.choice · Quot.sound

ราคาที่ต้องจ่าย มีทั้งความช้าและเวลา

แน่นอนว่าแนวทางนี้มีราคาที่ต้องจ่าย เพราะโค้ดเวอร์ชันที่ผ่านการพิสูจน์แล้วทำงานช้ากว่าโปรแกรมตัดโมเดลระดับแนวหน้ามาก ตัวเลขในโปรเจกต์ระบุว่า การตัดโมเดลกระต่าย Stanford สองตัว ตัวละ 70,000 สามเหลี่ยม ใช้เวลาถึง 24 วินาทีบนชิป M4 Pro แบบรันเธรดเดียว

ผู้พัฒนาอธิบายว่าเป็นความตั้งใจออกแบบ เพื่อยอมแลกความเร็วกับการให้คนต้องตรวจทานน้อยที่สุด และไม่ได้เป็นข้อจำกัดตายตัวของซอฟต์แวร์ที่ผ่านการพิสูจน์ อย่างไรก็ตาม หน้าโปรเจกต์ไม่ได้แนบผลการวัดประสิทธิภาพจากภายนอกไว้ ตัวเลขทั้งหมดจึงมาจากผู้พัฒนาเอง

ต้นทุนอีกส่วนคือเวลากับจำนวนโทเคน การให้ agent เขียนบทพิสูจน์อย่างเป็นทางการ กินเวลาและโทเคนมากกว่าการให้มันเขียนโค้ดแบบทั่วไปอยู่คนละระดับ โดยบางขั้นตอนในโปรเจกต์นี้ agent ต้องทำงานต่อเนื่องยาวนานเกิน 24 ชั่วโมง

หน้าโปรเจกต์ยังระบุข้อจำกัดไว้อย่างตรงไปตรงมาอีกข้อว่า งานจำนวนมากในชีวิตจริงไม่สามารถเขียนสเปกให้สั้นกระชับได้เหมือนงานเรขาคณิต นอกจากนี้ โค้ดและบทพิสูจน์ที่ AI เขียนขึ้นก็มีการสะสมหนี้ทางดีไซน์ไปเรื่อยๆ โดยไม่ได้สะอาดหรือมีโครงสร้างที่กลมกลืนเท่ากับงานที่คนเป็นผู้คุมภาพรวมทั้งหมด ดังนั้น งานชิ้นนี้จึงไม่ได้ยืนยันว่างานเขียนโค้ดของ AI ไว้ใจได้แล้ว แต่แสดงให้เห็นว่าในงานบางประเภท เราสามารถย้ายความเชื่อใจไปไว้ที่เครื่องตรวจแทนได้

เอาไปใช้ได้ตั้งแต่วันนี้ แม้ไม่แตะ Lean

ประโยคที่ผู้พัฒนาทิ้งท้ายไว้ในหน้าโปรเจกต์ ได้สรุปเหตุผลของงานชิ้นนี้ไว้อย่างชัดเจน

แม้จะยังไม่มีความจำเป็นต้องใช้ Lean แต่เราสามารถนำแนวคิด 3 อย่างไปปรับใช้ได้ทันที

• กำหนดให้ชัดเจนตั้งแต่แรกว่าผลลัพธ์ที่ยอมรับได้คืออะไร ยิ่งสั้นและตัดสินถูกผิดได้ชัดเจนเท่าไรยิ่งดี เพราะนี่คือสิ่งเดียวที่เราจะถือไว้เองตลอดการทำงาน
• ให้เครื่องเป็นคนตรวจแทนสายตาคนให้ได้มากที่สุด ทั้งการใช้เทสต์ที่รันอัตโนมัติทุกครั้งที่แก้ไขโค้ด · การกำหนดชนิดข้อมูลให้รัดกุมจนหากพิมพ์ผิดจะคอมไพล์ไม่ผ่าน · และการใช้เครื่องมือตรวจโค้ดอัตโนมัติ เพราะทุกอย่างที่เครื่องตรวจจับได้ จะช่วยประหยัดเวลาของคนอ่าน
• ลดขนาดส่วนที่คนต้องอ่านเองให้เล็กลงเรื่อยๆ เช่นการใช้ skill อย่าง ponytail ที่บังคับให้ agent เลือกแนวทางที่เขียนโค้ดน้อยที่สุดก่อน ซึ่งช่วยลดปริมาณโค้ดที่ต้องอ่านตั้งแต่ต้นทาง

ตัวเลข 93 บรรทัดนี้มาจากงานเรขาคณิตเพียงชิ้นเดียว งานของแต่ละคนย่อมมีตัวเลขที่เหมาะสมแตกต่างกันไป และการตอบให้ได้ว่างานของเราต้องใช้กี่บรรทัด ก็ยังเป็นส่วนที่คนต้องตัดสินใจเองอยู่ดี

ที่มา: โปรเจกต์ verified-3d-mesh-intersection บน GitHub