- การพิสูจน์ความถูกต้องเชิงรูปแบบ (formal verification) คือวิธีการพิสูจน์ทางคณิตศาสตร์ว่าโค้ดเป็นไปตามข้อกำหนดเสมอ ซึ่งเป็นพื้นที่ที่จำกัดอยู่ในวงการวิจัยมาเป็นเวลานาน
- แม้จะมีระบบขนาดใหญ่บางส่วน เช่น ไมโครเคอร์เนล seL4 ที่พัฒนาด้วยการพิสูจน์ความถูกต้องเชิงรูปแบบ แต่ก็แทบไม่ถูกใช้ในภาคอุตสาหกรรมเนื่องจาก ความยากและต้นทุนที่สูง
- ช่วงหลังมานี้ เครื่องมือช่วยเขียนโค้ดที่อิง LLM ไม่เพียงทำผลงานได้ดีในการสร้างโค้ด แต่ยังทำได้ดีในการ เขียนสคริปต์พิสูจน์ ในหลายภาษา จึงมีแนวโน้มจะเปลี่ยนโครงสร้างต้นทุนของการตรวจพิสูจน์อย่างมาก
- หาก AI สามารถทำให้ทั้งการสร้างโค้ดและ การพิสูจน์ความถูกต้องอัตโนมัติ เกิดขึ้นได้พร้อมกัน ก็อาจนำไปสู่การพัฒนาซอฟต์แวร์ที่เชื่อถือได้ยิ่งกว่าการรีวิวโค้ดโดยมนุษย์
- การทำให้การพิสูจน์ความถูกต้องเชิงรูปแบบเป็นอัตโนมัติ คือ เทคโนโลยีหลักสำหรับการรับประกันความน่าเชื่อถือของซอฟต์แวร์ในยุค AI และปัจจัยชี้ขาดต่อการแพร่หลายสู่กระแสหลักน่าจะเป็นการเปลี่ยนผ่านทางวัฒนธรรมมากกว่าข้อจำกัดทางเทคนิค
สถานะปัจจุบันและข้อจำกัดของการพิสูจน์ความถูกต้องเชิงรูปแบบ
- ภาษาและเครื่องมือที่มุ่งเน้นการพิสูจน์ เช่น Rocq, Isabelle, Lean, F*, Agda ช่วยให้สามารถพิสูจน์ทางคณิตศาสตร์ได้ว่าโค้ดสอดคล้องกับข้อกำหนด
- ตัวอย่างเด่น ได้แก่ เคอร์เนลระบบปฏิบัติการ seL4, คอมไพเลอร์ภาษา C อย่าง CompCert และสแตกโปรโตคอลเข้ารหัส Project Everest
- อย่างไรก็ตาม ในภาคอุตสาหกรรมการพิสูจน์ความถูกต้องเชิงรูปแบบ แทบไม่ถูกใช้งาน
- ในกรณีของ seL4 การตรวจพิสูจน์โค้ด C จำนวน 8,700 บรรทัด ต้องใช้ 20 คน-ปี และโค้ด Isabelle 200,000 บรรทัด
- ต่อโค้ดที่เขียนจริง 1 บรรทัด ต้องใช้สคริปต์พิสูจน์ 23 บรรทัดและกำลังคนครึ่งวัน
- คาดว่าทั่วโลกมีผู้เชี่ยวชาญที่สามารถเขียนการพิสูจน์ลักษณะนี้ได้เพียง ระดับไม่กี่ร้อยคน
- ในทางเศรษฐศาสตร์ สำหรับระบบส่วนใหญ่ ต้นทุนการตรวจพิสูจน์สูงกว่าความเสียหายจากบั๊ก จึงทำให้การใช้งานจริงมีความคุ้มค่าน้อย
AI กำลังเปลี่ยนเศรษฐศาสตร์ของการพิสูจน์ความถูกต้องเชิงรูปแบบ
- ช่วงหลัง ผู้ช่วยเขียนโค้ดที่อิง LLM แสดงผลงานได้ดีไม่เฉพาะกับโค้ดที่ใช้จริง แต่รวมถึง การเขียนสคริปต์พิสูจน์ ด้วย
- มีรายงานจาก Nature, Galois, arXiv และแหล่งอื่น ๆ ว่า LLM สามารถสร้างบทพิสูจน์ได้ในหลายภาษา
- ปัจจุบันยังต้องอาศัยการกำกับจากผู้เชี่ยวชาญ แต่คาดว่า การทำงานอัตโนมัติเต็มรูปแบบอาจเป็นไปได้ภายในไม่กี่ปี
- หากต้นทุนการตรวจพิสูจน์ลดลงอย่างมาก ก็จะสามารถนำการพิสูจน์ความถูกต้องเชิงรูปแบบไปใช้กับซอฟต์แวร์ได้มากขึ้น
- ขณะเดียวกัน โค้ดที่ AI สร้างขึ้นก็จำเป็นต้อง รับประกันความน่าเชื่อถือด้วยการพิสูจน์เชิงรูปแบบแทนการตรวจโดยมนุษย์
- หาก AI สามารถพิสูจน์ความถูกต้องของโค้ดที่มันสร้างเองได้ ก็มีแนวโน้มที่จะได้รับความนิยมมากกว่าโค้ดที่เขียนด้วยมือ
ความเกื้อหนุนกันระหว่าง LLM และการตรวจสอบบทพิสูจน์
- เมื่อ LLM เขียนสคริปต์พิสูจน์ แม้จะสร้าง ข้อมูลเท็จหรือภาพหลอน (hallucination) ขึ้นมา แต่ ตัวตรวจสอบบทพิสูจน์ (proof checker) จะปฏิเสธสิ่งเหล่านั้น
- ตัวตรวจสอบถูกสร้างจากโค้ดขนาดเล็กที่ผ่านการตรวจพิสูจน์มาแล้ว จึง ยากที่จะปล่อยให้บทพิสูจน์ที่ผิดผ่านไปได้
- ดังนั้น ความไม่แน่นอนของ LLM จึงถูกชดเชยด้วย ความเข้มงวดของการพิสูจน์เชิงรูปแบบ
- การจับคู่เช่นนี้ทำหน้าที่เป็น เส้นทางสู่อัตโนมัติที่ปลอดภัย สำหรับการรับประกันความน่าเชื่อถือของโค้ดที่ AI สร้างขึ้น
ความท้าทายใหม่: ความถูกต้องของการนิยามข้อกำหนด
- แม้อยู่ในสภาพแวดล้อมที่ตรวจพิสูจน์แบบอัตโนมัติ การนิยาม ข้อกำหนด (specification) ให้ถูกต้องก็ยังเป็นโจทย์สำคัญ
- ต้องตรวจสอบว่าคุณสมบัติที่พิสูจน์ได้นั้นตรงกับคุณสมบัติที่นักพัฒนาตั้งใจจริงหรือไม่
- การเขียนข้อกำหนดยังคงต้องใช้ความเชี่ยวชาญและการคิดอย่างรอบคอบ แต่ ง่ายและเร็วกว่าการพิสูจน์ด้วยมือมาก
- AI อาจช่วย แปลข้อกำหนดระหว่างภาษาธรรมชาติกับภาษาทางการ ได้ด้วย
- อย่างไรก็ตาม ยังมีความเสี่ยงเรื่องการสูญเสียความหมาย แต่ถูกประเมินว่าอยู่ในระดับที่จัดการได้
แนวโน้มการเปลี่ยนแปลงของวิธีพัฒนาซอฟต์แวร์
- นักพัฒนาสามารถอธิบายคุณสมบัติของโค้ดที่ต้องการในรูปแบบ ข้อกำหนดเชิงประกาศ และให้ AI สร้างทั้ง การติดตั้งใช้งานและบทพิสูจน์ ไปพร้อมกันได้
- ในกรณีนี้ นักพัฒนาไม่จำเป็นต้องตรวจโค้ดที่ AI สร้างขึ้นโดยตรง และสามารถใช้งานมันบนพื้นฐานของความเชื่อถือได้ เช่นเดียวกับภาษาเครื่องที่คอมไพเลอร์สร้างขึ้น
- โดยสรุป คาดว่าจะเกิดการเปลี่ยนแปลง 3 ประการต่อไปนี้
- ต้นทุนของการพิสูจน์ความถูกต้องเชิงรูปแบบลดลงอย่างรวดเร็ว
- ความต้องการการตรวจพิสูจน์เพิ่มขึ้นเพื่อรับประกันความน่าเชื่อถือของโค้ดที่ AI สร้าง
- ความแม่นยำของการพิสูจน์ความถูกต้องเชิงรูปแบบเข้ามาชดเชยธรรมชาติแบบความน่าจะเป็นของ LLM
- เมื่อปัจจัยเหล่านี้รวมกัน การพิสูจน์ความถูกต้องเชิงรูปแบบก็มีแนวโน้มสูงที่จะกลายเป็น เทคโนโลยีกระแสหลักของวิศวกรรมซอฟต์แวร์
- ข้อจำกัดในอนาคตจึงมีแนวโน้มจะอยู่ที่ ความเร็วในการยอมรับการเปลี่ยนแปลงของวัฒนธรรมการพัฒนา มากกว่าประเด็นทางเทคนิค
1 ความคิดเห็น
ความเห็นจาก Hacker News
ฉันคิดว่า formal verification แสดงคุณค่าได้ชัดในงานที่ implementation ซับซ้อนกว่าสเปกมาก
เช่น การทำ optimization ระดับบิตในงานเข้ารหัส หรือขั้นตอน optimization ของคอมไพเลอร์
แต่โค้ดที่นักพัฒนาส่วนใหญ่ (หรือ AI) เขียนกันทุกวันนี้ก็ใกล้เคียงกับสเปกอยู่แล้วเพราะอาศัยภาษาระดับสูง จึงมองว่าข้อดีของ formal verification ไม่ได้มากขนาดนั้น
ก็ยังไม่แน่ใจด้วยว่าการแยกเขียนสเปกออกมาต่างหากจะอ่านง่ายกว่าจริงหรือไม่
เพราะทุกวันนี้ก็มี framework และ library มากมายที่ช่วย abstract รายละเอียดการ implementation อยู่แล้ว
formal verification อาจให้การรับประกันที่แข็งแรงกว่าได้จริง แต่คนส่วนใหญ่ไม่ได้ต้องการการรับประกันระดับนั้น และ AI ก็คงไม่ได้สร้างความจำเป็นนั้นขึ้นมาใหม่
บางคนคาดว่า AI จะทำให้ formal verification เป็นอัตโนมัติได้ทั้งหมด แต่ฉันคิดว่าตรรกะนี้มีปัญหา
ถ้า AI สามารถพิสูจน์ซอฟต์แวร์ได้อัตโนมัติ ก็คงไม่จำเป็นต้องมาคอยตรวจสอบซอฟต์แวร์ที่มนุษย์เขียนอยู่แล้ว
เพราะ AI คง คิดไอเดีย ลงมือทำ และตัดสินใจเลือกระดับการตรวจสอบ ได้เอง
สุดท้ายการเขียนโปรแกรมหรือการตรวจสอบโดยมนุษย์อาจหายไปเลยก็ได้
ในทางปฏิบัติ มนุษย์อาจออกแบบ proof assistant ได้ แต่การใช้มันเพื่อตรวจสอบโปรแกรมขนาดใหญ่นั้นยากกว่ามาก
ดังนั้นถ้ามี AI แบบนั้นเกิดขึ้น มันก็น่าจะสร้าง proof assistant แบบใหม่ขึ้นมาเองได้
แน่นอนว่าจินตนาการแบบนี้ใกล้เคียงกับ แนว SF มากกว่า และการคาดเดาว่า AI จะทำให้อะไรง่ายขึ้นหรือยากขึ้นโดยที่เรายังไม่ชัดเจน ก็ไม่ได้มีความหมายมากนัก
ลิงก์การถกเถียงที่เกี่ยวข้อง
มันน่าจะเป็น จุดเปลี่ยน ที่ทำให้มนุษยชาติก้าวเข้าสู่อีกยุคหนึ่งโดยสิ้นเชิง
หากอยากได้ผลลัพธ์ที่มีประโยชน์จาก coding agent (เช่น Claude Code, Codex CLI เป็นต้น) หัวใจสำคัญคือการมี สภาพแวดล้อมที่สามารถรันและตรวจสอบโค้ดที่มันเขียนได้ อย่างพร้อมสรรพ
ภาษาที่รันได้ง่ายอย่าง Python เหมาะที่สุด และถ้าเป็น HTML+JS ก็ควรใช้เครื่องมืออย่าง Playwright
ขั้นถัดไปคือ automated test suite และเครื่องมือคุณภาพโค้ดอย่าง formatter, linter, fuzzer
debugger ก็ดี แต่มีข้อเสียตรงที่เป็นแบบ interactive จึงจัดการได้ยากสำหรับเอเจนต์
ฉันมองว่าเครื่องมือ formal verification ก็อยู่ในสเปกตรัมนี้ด้วย — เพราะโมเดลยุคนี้จัดการกับ ภาษาโปรแกรมเฉพาะทาง ได้ดีเหมือนกัน
ถ้ารู้สึกว่า coding agent ไม่ค่อยมีประโยชน์ สาเหตุก็มักเป็นเพราะสภาพแวดล้อมสำหรับการรันและทดสอบยังไม่พร้อม
ถ้ายก Haskell เป็นตัวอย่าง พอคอมไพล์ผ่านแล้วก็มักจะทำงานได้ถูกต้องเกือบตลอด
ถ้าคุณสมบัตินี้มีประโยชน์กับมนุษย์ มันก็น่าจะมีประโยชน์กับ LLM เช่นกัน
โดยเฉพาะ property test ที่เข้ากับ LLM ได้ดี — เพราะใช้จำนวนเทสต์ไม่มากแต่ครอบคลุมพื้นที่ความผิดพลาดได้กว้าง
เมื่อเห็นว่าชุมชนคณิตศาสตร์พยายามใช้ LLM เพื่อปรับปรุงโค้ด Lean ก็พอเชื่อได้ว่าการพัฒนาซอฟต์แวร์โดยอาศัย type system ที่แข็งแรงกว่านี้ก็เป็นไปได้มากพอสมควร
เพราะการ debug ไม่ได้เป็นลำดับตรงไปตรงมา และจังหวะของสาเหตุกับผลลัพธ์ก็มักสลับปะปนกัน
ก่อนหน้านี้ฉันเคยลองใช้ ChatGPT ตอนตามแก้บั๊ก multithread ด้วย gdb แต่มันก็เอาแต่เสนอให้เพิ่ม print ง่ายๆ ซ้ำไปซ้ำมา
สุดท้ายก็ยิ่งรู้สึกว่านี่เป็นงานที่ต้องอาศัย ประสบการณ์และสัญชาตญาณ
จะให้วิศวกรจูเนียร์ทำงานโดยไม่มี debugger หรือ test runner ก็คงไม่มีเหตุผล
สุดท้ายก็คงต้องใช้ ทรัพยากรคอมพิวต์ มากขึ้น
ให้ Claude ลงมือ implement แล้วให้ Codex กับ Gemini ช่วย review
วิธีนี้แพงก็จริง แต่เป็นวิธีที่แน่นอนที่สุดที่ฉันเจอในการลด self-bias และยกระดับคุณภาพโค้ด
เครื่องมือ static analysis น่าจะช่วยเสริมได้ แต่ก็รู้สึกว่าแค่เพิ่มจำนวนเครื่องมืออย่างเดียวไม่เพียงพอ
เมื่อกระบวนการตรวจสอบเป็นอัตโนมัติแล้ว ส่วนที่ยากจริงจะย้ายไปอยู่ที่ การนิยาม specification ให้แม่นยำ
การเขียนสเปกนั้นเร็วและง่ายกว่าการพิสูจน์มาก แต่ก็ยังต้องอาศัยความเชี่ยวชาญและความรอบคอบอยู่ดี
เหตุผลที่ formal proof ไม่แพร่หลายในอดีตไม่ใช่แค่เพราะมันยาก แต่ยังเพราะ แนวทางแบบ waterfall หายไปและ การพัฒนาแบบ agile กลายเป็นกระแสหลัก
เราเปลี่ยนจากการเขียนสเปกยาวๆ มาเป็นการวนรอบเร็วให้สอดคล้องกับความต้องการของผู้ใช้แทน
ดูเหมือนว่าจะถึงเวลาต้องไปเรียน OCaml แล้ว
proof assistant และระบบ verification หลายตัวสามารถสร้างโค้ด OCaml ได้ และ ADA/Spark ก็น่าสนใจเช่นกัน
ไม่ว่าอย่างไร software engineering ในยุค AI ก็คงเปลี่ยนไป แต่เราจำเป็นต้องสร้าง ซอฟต์แวร์ที่มีคุณภาพสูงกว่าเดิม
formal verification จะช่วยเป้าหมายนั้นได้อย่างแน่นอน
ยังทำไม่เสร็จดี แต่ขอแชร์โปรเจ็กต์ทดลองของฉัน
ในโลกที่ยังมีงานเขียนเชิงโค้ดไม่มากนัก ถ้าใครกำลังหา ไอเดียแฮกกาธอนที่น่าสนใจ ก็น่าจะลองดูได้
ลิงก์โปรเจ็กต์ py-mcmas
LLM มักเก่งกับ ปัญหาที่ตรวจสอบคำตอบได้ง่าย
เพราะแบบนั้นฉันจึงแบ่งการแก้ปัญหาออกเป็นสามขั้น
1️⃣ เขียนโปรแกรมสำหรับเงื่อนไขความสำเร็จก่อน
2️⃣ ให้โปรแกรมนั้นใช้ตรวจสอบปัญหาต้นฉบับ
3️⃣ แล้วค่อยให้ฉันตรวจเองอีกครั้งในตอนท้าย
วิธีนี้เป็นแนวทางที่ฉันใช้มานานแล้ว แต่ตอนนี้โมเดลอย่าง Opus หรือ GPT-5.2 ก็ทำได้ดีแม้ใน โหมดไร้การควบคุม
บล็อกโพสต์ที่เกี่ยวข้อง
ในงานที่การตรวจสอบใช้เวลานาน ภาระการตรวจของมนุษย์อาจยิ่งเพิ่มขึ้นแทน
อาจมีคนถามว่า “แล้วใครจะตรวจโปรแกรมที่ใช้ตรวจสอบอีกที?”
ถ้า LLM เป็นคนเขียนมันด้วย ก็อาจดูเหมือน กองเต่าซ้อนกันไม่รู้จบ (turtles all the way down)
สิ่งที่ยากคือกระบวนการสร้าง proof
แน่นอนว่าใน proposition ที่ซับซ้อนมากๆ ก็มีข้อยกเว้นอยู่บ้าง แต่โดยรวมแล้วมันช่วยลดบั๊กได้มาก
ต่อให้ formal verification จะแพร่หลายขึ้น ก็ไม่ได้แปลว่าทุกคนจะต้องใช้ Lean หรือ Isabelle
ตรงกันข้าม มันน่าจะกระจายตัวในรูปแบบที่ AI กลมกลืนเข้าไปใน workflow เดิมอย่างเป็นธรรมชาติ มากกว่า
เช่น มี property verification อยู่ใน CI หรือมีปุ่ม “พิสูจน์ invariant ของโมดูลนี้” ใน IDE
วิศวกรส่วนใหญ่คงไม่จำเป็นต้องเห็น proof script ด้วยตัวเองเลย
เรื่องที่ยากจริงไม่ใช่การให้ LLM สร้าง proof แต่คือการทำให้องค์กร ยอมลงทุนกับการเขียน specification และ model
ถ้า AI ช่วยให้การเสนอและแก้ไขสเปกทำได้ง่ายขึ้น verification ก็น่าจะกลายเป็น เครื่องมือรีแฟกเตอร์ริง ที่เป็นธรรมชาติเหมือน test หรือ linter
บางคนบ่นว่า GPT‑5.2 ยังนับจำนวน r ในคำว่า “garlic” ไม่ได้เลย
ถ้าจำเป็นจริงๆ ก็แค่ให้ LLM เขียนสคริปต์ Python แล้วรันมันก็พอ
แม้จะพูดไม่ผิด แต่ก็เป็นแค่ รายละเอียดระดับ implementation ของ tokenizing และแทบไม่เกี่ยวกับความมีประโยชน์ในการใช้งานจริง
แทบไม่มีใครใช้ LLM เพื่อนับจำนวนตัวอักษรในคำอยู่แล้ว