ในแวดวงคณิตศาสตร์ การพิสูจน์ว่าสิ่งที่ถูกต้องนั้นจริง (Proof Construction) และการหาตัวอย่างค้านสำหรับสิ่งที่ผิด (Counterexample Generation) มีความสำคัญเท่าเทียมกัน แต่งานวิจัยด้าน AI ส่วนใหญ่มักมุ่งเน้นไปที่การสร้างบทพิสูจน์เพียงอย่างเดียว งานวิจัยชิ้นนี้จึงนำเสนอแนวทางใหม่ในการฝึกฝน LLM ให้สามารถหาตัวอย่างค้านได้อย่างเป็นระบบ
ทีมวิจัยได้ใช้วิธี 'Symbolic Mutation' เพื่อสร้างข้อมูลฝึกสอนจำนวนมากจากการปรับเปลี่ยนทฤษฎีบทเดิมที่มีอยู่ และพัฒนาเฟรมเวิร์กการฝึกแบบ Multi-reward Expert Iteration ซึ่งผลลัพธ์ที่ได้คือโมเดลไม่เพียงแต่เสนอตัวอย่างค้านได้ แต่ยังสามารถเขียนโค้ดในภาษา Lean 4 เพื่อให้ระบบตรวจสอบความถูกต้องได้โดยอัตโนมัติ ช่วยเพิ่มประสิทธิภาพในการตรวจสอบความสมเหตุสมผลของทฤษฎีบทต่างๆ ได้อย่างก้าวกระโดด
