ทันเอไอ

ทีมนักวิจัยฮาร์วาร์ดเปิดตัว Choir โปรโตคอลกระจายศูนย์ระดม AI พิสูจน์ทฤษฎีคณิตศาสตร์

นักวิจัยจากมหาวิทยาลัยฮาร์วาร์ดนำเสนอ Choir โปรโตคอลเปิดที่ช่วยให้ตัวแทน AI หลายตัวจากผู้ใช้ที่หลากหลายมาร่วมกันแปลงทฤษฎีคณิตศาสตร์ให้เป็นภาษาทางการผ่าน GitHub ได้อย่างเป็นระบบ

วงการวิจัยปัญญาประดิษฐ์และคณิตศาสตร์กำลังก้าวไปอีกขั้น เมื่อนักวิจัยจากมหาวิทยาลัยฮาร์วาร์ด นำโดย Yidi Qi และ Melanie Weber ได้เผยแพร่งานวิจัยบนแพลตฟอร์ม arXiv เมื่อวันที่ 25 กันยายน 2026 โดยแนะนำ "Choir" โปรโตคอลแบบเปิดที่ออกแบบมาเพื่อการทำ Autoformalization หรือการแปลงข้อความคณิตศาสตร์จากภาษาธรรมชาติให้เป็นภาษาทางการที่คอมพิวเตอร์ตรวจสอบความถูกต้องได้ โดยใช้ระบบตัวแทน AI หลายตัว (Multi-Agent) ทำงานร่วมกันแบบกระจายศูนย์

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

สำหรับการประสานงานและการบริหารจัดการโครงการ Choir จะใช้ระบบของ GitHub เป็นศูนย์กลาง ตั้งแต่การจัดการงานไปจนถึงการส่ง Pull Requests โดยจะมีระบบตัวจัดการ (Orchestrator) คอยวางแผนและแบ่งงานให้ตัวแทนย่อย (Workers) นำไปดำเนินการ นอกจากนี้ เพื่อให้มั่นใจในคุณภาพและความถูกต้องของงานที่ส่งเข้ามา โปรโตคอลนี้จึงได้ติดตั้ง "Deterministic Gate" หรือระบบตรวจสอบแบบกำหนดผลลัพธ์แน่นอน ทำหน้าที่คัดกรองและตรวจสอบความถูกต้องของชิ้นงานทุกชิ้นก่อนที่จะทำการรวมเข้าสู่ระบบ (Merge)

ในแง่ของการใช้งานจริง Choir ถูกออกแบบมาให้มีความเป็นโอเพนซอร์สและมีโครงสร้างแบบโมดูลาร์ ทำให้ผู้ใช้งานสามารถปรับเปลี่ยนหรือขยายส่วนประกอบต่างๆ ได้ตามต้องการ โดยในเบื้องต้นระบบนี้รองรับระบบพิสูจน์ทฤษฎีหลักๆ ถึง 3 ระบบ ได้แก่ Lean 4, Isabelle และ Rocq ช่วยเปิดโอกาสให้ชุมชนนักพัฒนาและนักวิจัยสามารถร่วมมือกันผลักดันงานพิสูจน์ทางคณิตศาสตร์ที่ซับซ้อนได้อย่างมีประสิทธิภาพและประหยัดต้นทุนกว่าเดิม