ทันเอไอ

ทีมนักวิจัยเปิดตัว IneqAgent ผสานสมองกล LLM และระบบคำนวณสัญลักษณ์ ช่วยพิสูจน์อสมการบน Lean4

IneqAgent กรอบงานใหม่ที่ผสานความสามารถของโมเดลภาษาขนาดใหญ่และการคำนวณเชิงสัญลักษณ์ เพื่อช่วยสร้างและตรวจสอบบทพิสูจน์อสมการทางคณิตศาสตร์บนระบบ Lean4

วงการวิจัยปัญญาประดิษฐ์และคณิตศาสตร์เชิง formal ได้มีความคืบหน้าครั้งใหม่ เมื่อนักวิจัยได้เผยแพร่งานวิจัยเกี่ยวกับ IneqAgent กรอบงาน (Framework) แบบเอเจนต์ที่ออกแบบมาเพื่อแก้ปัญหาการพิสูจน์อสมการ (Inequality Proving) บน Lean4 ซึ่งเป็นระบบพิสูจน์ทฤษฎีบทเชิงกลไก (Theorem Prover) ที่ได้รับความนิยมในหมู่นักคณิตศาสตร์และนักวิทยาศาสตร์คอมพิวเตอร์

การพิสูจน์อสมการทางคณิตศาสตร์เป็นเรื่องที่ซับซ้อน เนื่องจากต้องอาศัยการใช้เหตุผลควบคู่กับการคำนวณที่แม่นยำผ่านบทตั้ง (Lemmas) และการปรับรูปเป้าหมาย งานวิจัยนี้จึงได้นำ IneqAgent เข้ามาแก้ปัญหา โดยผสานความสามารถด้านการให้เหตุผลของโมเดลภาษาขนาดใหญ่ (LLM) เข้ากับการคำนวณเชิงสัญลักษณ์ (Symbolic Computation) เพื่อสร้างบทพิสูจน์ที่ตรวจสอบได้จริง

หัวใจสำคัญของ IneqAgent คือการใช้กระบวนการค้นหาแบบ Monte Carlo Tree Search (Monte Carlo Tree Search) ระดับบทตั้ง ในการจัดการกับการสร้างบทตั้ง การปรับรูปเป้าหมาย และการเลือกชุดคำสั่งเบื้องหลัง (Backends) นอกจากนี้ ระบบยังใช้เครื่องมือคำนวณเสริมอย่างผลบวกของกำลังสอง (Sum-of-Squares), วิธีเบิร์นสไตน์ (Bernstein) และการแทนที่ผลต่างต่อเนื่อง เพื่อสร้างใบรับรองที่ถูกต้องแม่นยำสำหรับการนำไปสร้างบทพิสูจน์บน Lean4 ต่อไป

จากรายงานในบทวิจัย ระบุว่าเมื่อใช้งานร่วมกับโมเดล DeepSeek-V4-Flash ซึ่งเป็นรุ่นที่คณะผู้วิจัยนำมาทดสอบ IneqAgent สามารถแก้ปัญหาในชุดทดสอบ 4 ชุด ได้สำเร็จถึง 175 จาก 186 ข้อ หรือคิดเป็น 94.09% ซึ่งนับว่าทำผลงานได้สูงสุดเฉพาะในกลุ่มวิธีที่งานนี้นำมาเปรียบเทียบ โดยบทความดังกล่าวได้รับการเผยแพร่บนคลังบทความวิจัย arXiv เมื่อเดือนตุลาคม 2026 ที่ผ่านมา