ProofOfThought: การให้เหตุผลบนพื้นฐาน LLM โดยใช้การพิสูจน์ทฤษฎีบท Z3

• ProofOfThought ผสาน โมเดลภาษาขนาดใหญ่ (LLM) เข้ากับ ตัวพิสูจน์ทฤษฎีบท Z3 เพื่อรองรับ การให้เหตุผลที่ทรงพลังและตีความได้
• โปรเจ็กต์นี้ให้ ผลลัพธ์การให้เหตุผลที่แม่นยำและเชื่อถือได้ สำหรับ คำถามภาษาธรรมชาติ
• ผ่าน Python API ระดับสูง นักพัฒนาสามารถสร้างและทดลอง งานให้เหตุผลที่ซับซ้อน ได้อย่างสะดวก
• ผ่าน Z3DSL ยังมีการเข้าถึง DSL ระดับล่างที่อิง JSON ทำให้ปรับแต่งได้อย่างยืดหยุ่น
• การได้รับการตีพิมพ์ใน Sys2Reasoning Workshop NeurIPS 2024 แสดงให้เห็นถึงข้อดีด้านการนำผลงานวิจัยล่าสุดไปใช้จริง

---

แนะนำโปรเจ็กต์โอเพนซอร์ส ProofOfThought

ProofOfThought เป็นไลบรารีโอเพนซอร์สสำหรับการให้เหตุผลที่ใช้แนวทาง การสังเคราะห์โปรแกรมแบบ neuro-symbolic (ประสาท-สัญลักษณ์) โดยผสานโมเดลภาษาขนาดใหญ่ (LLM) เข้ากับตัวพิสูจน์ทฤษฎีบท Z3 จุดเด่นสำคัญคือสามารถให้ ผลลัพธ์การให้เหตุผลที่แข็งแกร่งและตีความได้ สำหรับปัญหาซับซ้อนในโลกจริง ซึ่งมีความหมายสำคัญทั้งในด้านการใช้งานจริงและงานวิจัย

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

สถาปัตยกรรมระบบและองค์ประกอบหลัก

• API ระดับสูง (z3dsl.reasoning) :

  • ดำเนินการคำถามเชิงเหตุผลจากภาษาธรรมชาติ
  • มี Python interface ที่ผู้เริ่มต้นก็ใช้งานได้ง่าย

• DSL ระดับล่าง (z3dsl) :

  • เข้าถึงตัวพิสูจน์ทฤษฎีบท Z3 ที่อิง JSON ได้
  • เหมาะสำหรับการปรับแต่งที่ซับซ้อนและการสร้างไปป์ไลน์อัตโนมัติ

ตัวอย่างความสามารถหลัก

• LLM แปลงคำถามที่ป้อนเข้ามาให้เป็นนิพจน์ตรรกะ (symbolic program)

• สร้างผลลัพธ์การตีความแบบจริง/เท็จ (yes/no) หรือแบบมีเงื่อนไขผ่านตัวพิสูจน์ Z3

• ตัวอย่าง:

  • คำถาม: "Nancy Pelosi จะประณามการทำแท้งอย่างเปิดเผยหรือไม่?"
  • ผลลัพธ์: False (ไม่ใช่)

• มีไปป์ไลน์ประเมินผล (EvaluationPipeline):

  • ประเมินผลแบบแบตช์กับชุดข้อมูลจำนวนมากได้
  • รายงานค่าความแม่นยำและผลลัพธ์อื่น ๆ โดยอัตโนมัติ

การประยุกต์ใช้และกรณีใช้งาน

• การทำระบบอัตโนมัติสำหรับ benchmark การให้เหตุผล เพื่อการวิจัย
• บริการพิสูจน์อัตโนมัติสำหรับ knowledge graph หรือปัญหาตรรกะลำดับสูงที่อิง LLM
• มีศักยภาพในการประยุกต์ใช้กับบริการ AI หลากหลายประเภท เช่น คำถามเชิงนโยบายที่ซับซ้อน หรือการตัดสินการโต้วาทีภาษาธรรมชาติโดยอัตโนมัติ

ความสำคัญเชิงวิจัยและคุณลักษณะเด่น

• นำเสนอในเวิร์กช็อป Sys2Reasoning ของ NeurIPS 2024
• เสริมข้อจำกัดเดิมของ LLM (ความไม่แน่นอนในการให้เหตุผล) ด้วย ความน่าเชื่อถือบนพื้นฐานการตีความเชิงสัญลักษณ์
• ความโปร่งใสและการตีความได้ของผลลัพธ์การให้เหตุผลและหลักฐาน เป็นจุดแข็งสำคัญสำหรับการพัฒนาบริการจริง

บทสรุป

ProofOfThought ผสานจุดแข็งของ LLM และตัวพิสูจน์ทฤษฎีบท Z3 เข้าด้วยกัน เพื่อมอบคุณค่าเชิงปฏิบัติแก่ทั้งนักพัฒนาและนักวิจัยที่ต้องการสร้าง โครงสร้างพื้นฐาน AI สำหรับการให้เหตุผลที่แข็งแกร่งและตีความได้ ใบอนุญาตและโครงสร้างของโปรเจ็กต์ยังถูกออกแบบมาให้เหมาะกับระบบนิเวศโอเพนซอร์ส จึงน่าสนใจทั้งในมุมงานวิชาการและการนำไปใช้ในอุตสาหกรรม

[GN⁺]

ความคิดเห็นจาก Hacker News

• เล่าประสบการณ์ที่น่าสนใจกับ Gemini 2.5 Pro ระหว่างพยายามแก้ระบบสมการในระบบ CAS ออนไลน์ แต่ CAS ไม่ทำงานอย่างที่คาดไว้ จึงขอให้ Gemini ช่วย และ Gemini ก็ให้คำตอบโดยตรง พร้อมอธิบายว่าใช้แพ็กเกจ sympy ของ Python ทำให้รู้สึกว่าการผสาน LLM ที่คลุมเครือเข้ากับเครื่องมือที่เข้มงวดสามารถให้ผลลัพธ์ที่ทรงพลังได้
  • ให้ความรู้สึกคล้ายมนุษย์ เราไม่เก่งการคำนวณซับซ้อน แต่เราสร้างคอมพิวเตอร์ที่ยอดเยี่ยมมาทำสิ่งนี้ได้ดี และหลังจากพยายามอย่างหนัก เราก็สร้างโปรแกรมที่พอจะทำนายข้อความจากการคำนวณเชิงตัวเลขได้ แต่กลับไม่ถนัดการคำนวณยาก ๆ สุดท้ายโปรแกรมนี้ก็สามารถทำนายวิธีสร้างและใช้งานโปรแกรมที่เก่งด้านการคำนวณเชิงตัวเลขได้
  • ชอบการจับคู่ LLM กับ sympy สำหรับงานคณิตศาสตร์มาก หากให้ LLM เขียนโค้ด sympy ก็สามารถเชื่อถือได้ว่าการคำนวณเชิงสัญลักษณ์ถูกต้อง ตัวโค้ดเองยังคงเป็นผลลัพธ์ที่เก็บไว้ได้ และไม่ว่าจะเป็นมนุษย์หรือ LLM ก็สามารถค่อย ๆ แก้ไขและปรับปรุงต่อได้ รวมถึงจัดการด้วยประวัติ git ได้อีกด้วย ความเชื่อมั่นในความถูกต้องทางคณิตศาสตร์ยังรักษาไว้ได้ผ่านการทดสอบและการตรวจสอบความถูกต้อง นอกจากนี้ยังใช้ฟังก์ชันช่วยที่แปลงจากโค้ด sympy เป็น latex ได้ง่าย ๆ ด้วย ช่วงหลังยังทำงานคณิตศาสตร์เกี่ยวกับการทดลอง quantum eraser ด้วยวิธีนี้ ลิงก์ github
  • เข้าใจว่าการใช้เครื่องมือเพื่อติดตามกระบวนการแก้ปัญหาร่วมกับ LLM เป็นวิธีที่ใช้ได้จริง และในความเป็นจริงมันทำงานได้ดีกว่าที่คาดมาก แต่การไม่ใช้ CAS แล้วไปให้ LLM จัดการคณิตศาสตร์แทน ก็เปรียบเหมือนย้ายอพาร์ตเมนต์ด้วยการนั่งรถบัสไปกลับหลายรอบแทนใช้รถบรรทุก เพียงเพราะมีบัตรโดยสารรถบัสอยู่แล้ว
• ย้ำว่า LLM ท้ายที่สุดก็เป็นแบบจำลองภาษาทางสถิติ จากประสบการณ์พบว่ามันทำงานได้ดีกว่าที่คาดมากในการสร้างโปรแกรมเชิงตรรกะ โดยเฉพาะซอร์สโค้ด Prolog อาจเป็นเพราะ Prolog ถูกนำมาใช้กับการประมวลผลภาษาธรรมชาติเชิงสัญลักษณ์ และในชุดข้อมูลฝึกก็มีตัวอย่างการแปลจำนวนมาก จึงน่าลองใช้ไวยากรณ์ Datalog ของ Z3 แทนไวยากรณ์ SMTLib ดูด้วย แนะนำให้อ่าน เดโมที่เกี่ยวข้อง และ ไวยากรณ์ Z3 Datalog
  • ไวยากรณ์ Datalog ใน Z3 นั้นดีมาก เราใช้ SMT ในงานวิจัยเรื่อง grammars เพราะมันเข้ากันได้กับตัวแก้ปัญหาหลายตัวมากที่สุด แต่เราได้ทดสอบในกระบวนการรีวิว NeurIPS แล้วว่าวิธีนี้ใช้กับ PROLOG ได้ดีเช่นกัน และคาดว่าน่าจะใช้กับ Datalog ได้ด้วย ลิงก์บทความ, ตัวอย่าง datalog
• มองว่าเป็นแนวทางที่น่าสนใจ ทีมของเราก็เคยสร้างต้นแบบที่คล้ายกัน โดยเข้ารหัสนโยบายการดำเนินธุรกิจด้วย LEAN ก่อนอื่นให้ LLM แปลงคลังความรู้ใน internal wiki หรือ Google Docs เป็นโค้ด LEAN แล้วจึงรันตัวแก้ปัญหาเพื่อตรวจสอบความสอดคล้องกัน เมื่อ wiki ถูกแก้ไข กระบวนการทั้งหมดก็จะรันใหม่ ทำหน้าที่คล้าย process linter อย่างไรก็ตาม การแปลงเป็น LEAN เองยังต้องให้วิศวกรตรวจทาน จึงยังอยู่ในขั้นต้นแบบ แต่เป็นแนวทางที่มีอนาคตในโดเมนที่ต้องการ compliance ด้านกฎหมายและการเงิน
  • กล่าวว่ากำแพงของการทำ formalization อัตโนมัตินั้นสูงมาก พร้อมแชร์ประสบการณ์จากบทความ NeurIPS 2025 ของพวกเขาที่วิเคราะห์โดยการหาปริมาณความไม่แน่นอนของการทำ formalization อัตโนมัติสำหรับไวยากรณ์ที่กำหนดไว้อย่างชัดเจน ลิงก์บทความ หากต้องการพูดคุยรายละเอียดเพิ่มเติมก็ยินดีเสมอ
  • สำหรับผู้ที่สงสัยว่า LEAN คืออะไร ขอแนะนำว่าเป็น Lean Theorem Prover ที่สร้างโดย Microsoft ลิงก์โครงการ
  • อยากเห็นตัวอย่างจริง ว่านโยบายแบบใดในโลกความเป็นจริงที่ถูกอธิบายไว้อย่างแม่นยำพอจะนิยามด้วย LEAN ได้
  • ดูเหมือนว่าวิธีนี้จะมีประโยชน์มากในการระบุแนวทางปฏิบัติที่ขัดแย้งกันอย่างเป็นระบบ
• เป็นสาขาวิจัยที่น่าสนใจมาก หลายปีก่อนเคยใช้เอนจินให้เหตุผลเชิงตรรกะและเชิงความน่าจะเป็นเพื่อตรวจสอบว่าข้อสมมติฐานนำไปสู่ข้อสรุปได้ดีหรือไม่ และยังใช้ agent เพื่อสังเคราะห์ ทำให้เป็นทางการ และวิจารณ์ความรู้เฉพาะโดเมนด้วย แม้ไม่ใช่ยาวิเศษ แต่ก็รับประกันความแม่นยำได้ระดับหนึ่ง มองว่าความเป็นเชิงสัญลักษณ์บางส่วนและแนวคิด agent-as-a-judge มีอนาคตที่ดี บทความอ้างอิง
  • ได้อ่านงานวิจัยนั้นแล้ว มันเจ๋งมาก ฉันเองก็เพิ่งมีประสบการณ์สร้างเอเจนต์ autoformalization ที่ AWS ARChecks เมื่อไม่นานนี้ แม้ยังไม่เปิดเผยต่อสาธารณะ แต่ก็มีผลิตภัณฑ์ที่ใช้งานได้ทั่วไปแล้ว จึงน่าจะเป็นประโยชน์ให้ดูไว้ AWS Blog
  • มองว่าการใช้ Agent/LLM เป็นผู้ตัดสินมีอคติ และเหมาะเพียงใช้สำหรับ bootstrapping เท่านั้น เมื่อประสิทธิภาพสูงขึ้นพอ LLM ที่ทำหน้าที่ผู้ตัดสินจะกลายเป็นข้อจำกัดแบบประดิษฐ์เอง สุดท้ายจึงต้องเปลี่ยนไปใช้ผู้ตัดสินที่เป็นมนุษย์ผู้เชี่ยวชาญหรือ oracle แบบกำหนดแน่นอน
• กล่าวถึงว่า proof of concept นี้ใช้ knife-edge rolling kernel ของ RHEL
• รู้สึกว่ารายละเอียดในรีโพซิทอรียังไม่เพียงพอ ซึ่งอาจเป็นเพราะมันทำหน้าที่เป็นผลลัพธ์ประกอบของงานวิจัย โดยแก่นแท้แล้วดูเหมือนเป็น API ที่ให้ LLM พยายามสร้างโปรแกรม Z3 โดยชี้นำให้มันแสดงคำถามจากโลกจริงในรูปแบบตรรกะ ครอบคลุมทั้งข้อเท็จจริง กฎการอนุมาน และเป้าหมาย ความสามารถในการกำกับดูแลอยู่ที่การทำให้สามารถอ่านคำอธิบายเชิงตรรกะได้โดยตรง และรัน solver เพื่อตรวจสอบว่าจริงหรือเท็จได้ จุดที่น่าสงสัยคือ ใครจะเป็นคนอ่านกฎ SMT ทีละข้อแล้วเทียบกับมุมมองของโลกจริง ใครจะตรวจสอบค่าคงที่ และ LLM จะเผลอหรือจงใจเพิ่มกฎที่ผิดเพี้ยนทั้งในเชิงตรรกะหรือเชิงความจริงเพื่อให้บรรลุเป้าหมายหรือไม่ ในบทความนี้มี false positive สูงถึง 51% ตามเกณฑ์มาตรฐานด้านตรรกะ ซึ่งเป็นตัวเลขที่สูงจนน่าตกใจ และตีความได้ว่า LLM ยังอ่อนในการสร้างแบบจำลองเชิงตรรกะหรือสร้างกฎที่ไม่สมบูรณ์ การประเมินผลเองก็ค่อนข้างบาง ทำให้ยังอธิบายไม่ชัดว่าทำไมจึงเกิดสิ่งนี้
  • บทความนี้เขียนขึ้นเมื่อปีที่แล้วด้วย GPT-4o และอ้างว่าสถานการณ์ดีขึ้นมากแล้วในโมเดลล่าสุด ตัวอย่างเช่นใน บทความล่าสุด ตาราง 1 มีการเปรียบเทียบประสิทธิภาพแบบ text-based กับแบบ SMT ซึ่ง o3-mini ทำให้ผลของ text reasoning กับ SMT สอดคล้องกันได้ดี สำหรับผลิตภัณฑ์เชิงพาณิชย์อย่าง AWS Automated Reasoning Checks จะสร้างโดเมนโมเดล ตรวจสอบมัน และในขั้นสร้างคำตอบก็ใช้การตรวจสอบอย่างเข้มงวดด้วย solver ว่าคู่ Q/A ของ LLM ปฏิบัติตามนโยบายหรือไม่ โดยเน้นว่าสามารถรับประกันความถูกต้องเชิงนโยบายของคู่ Q/A ได้มากกว่า 99% AWS Blog
• เป็นคำถามว่าความเข้าใจของตนถูกต้องหรือไม่ หากโครงสร้างคือเอาผลลัพธ์เชิงความน่าจะเป็นจาก LLM ไปส่งต่อเข้าโมเดลเชิงตรรกะ ก็อดสงสัยไม่ได้ว่านี่ไม่ใช่แค่ “ขยะเข้า ก็ขยะออก” หรือ
  • ตรรกะแบบเป็นทางการทำหน้าที่เป็นตัวกรอง กล่าวคือไม่ใช่ “ขยะเข้า ก็ขยะออก” แต่เป็น “ขยะเข้า ก็ได้ขยะที่ผ่านการกรองแล้ว” พร้อมยกอุปมาเหมือนวิวัฒนาการ ที่การกลายพันธุ์แบบ “ขยะ” แบบสุ่มถูกคัดกรองโดยสภาพแวดล้อมทางธรรมชาติ
  • ยืนยันว่าไม่ได้ออกมาเป็น “ขยะ” เสมอไป เพราะมันให้ผลลัพธ์ที่มีประโยชน์ได้ค่อนข้างบ่อย จึงมีความหมาย
  • มองว่าเป็นเรื่องการประเมินเชิงอัตวิสัย เพราะสิ่งที่มนุษยชาติสร้างมาตลอดหลายพันปีก็อาจถูกมองว่าเป็นขยะได้เหมือนกัน ถ้าจะเถียงกันจริง ๆ ชีวิตในถ้ำอาจจะเรียบง่ายกว่า
• น่าสนใจมากที่ AI ไม่ได้แค่ “คิด” แต่ยังทิ้งไดอารีที่ตรวจสอบได้ไว้ด้วย ราวกับนักปรัชญาที่มีทนายรับรองแบบคริปโตคอยอยู่ข้างตัว เป็นงานที่น่าทึ่งจริง ๆ
• แนวคิดหลักคือให้ LLM วางโครงกระบวนการให้เหตุผลในรูปแบบ JSON DSL ที่มีโครงสร้าง จากนั้นจึงแปลงแบบกำหนดแน่นอนเป็นตรรกะอันดับหนึ่งและพยายามพิสูจน์ทฤษฎีบทด้วย Z3 ดังนั้นผลลัพธ์สุดท้ายคือข้อสรุปที่พิสูจน์ได้จริง หรือไม่ก็ตัวอย่างโต้แย้ง ซึ่งต่างจากสายโซ่ข้อความที่ดูน่าเชื่อถือเฉย ๆ
• เป็นงานวิจัยที่น่าสนใจ อยากดูตัวอย่าง DSL จึงไปดูรีโป แต่หาตัวอย่างที่ชัดเจนได้ยาก คงดีถ้ามีโค้ดตัวอย่างสั้น ๆ อยู่ใน README
  • ขอบคุณที่สนใจ จะเพิ่มให้ในเร็ว ๆ นี้ ระหว่างนี้ในหน้าที่ 11 เป็นต้นไปของบทความมีคำอธิบายหลายสถานการณ์อยู่ PDF บทความ