ทีมศิษย์เก่า Tsinghua ประสบความสำเร็จในการพัฒนาทางคณิตศาสตร์อย่างน่าประทับใจด้วยความช่วยเหลือของ AI! LeanAgent ที่พวกเขาพัฒนาขึ้น ซึ่งเป็นผู้ช่วย AI ที่มีความสามารถในการเรียนรู้ตลอดชีวิต ประสบความสำเร็จในการพิสูจน์ทฤษฎีบททางคณิตศาสตร์ที่ยังไม่ได้แก้ 162 ทฤษฎีก่อนหน้านี้ และยังแก้ปัญหาอย่างเป็นทางการของการคาดเดาพหุนาม Freiman-Ruzsa ที่เสนอโดย Terence Tao ได้ด้วย สิ่งนี้ไม่เพียงแสดงให้เห็นถึงศักยภาพมหาศาลของ AI ในการวิจัยทางวิทยาศาสตร์ขั้นพื้นฐาน แต่ยังถือเป็นนวัตกรรมในวิธีการวิจัยทางคณิตศาสตร์อีกด้วย เครื่องมือแก้ไข Downcodes จะทำให้คุณมีความเข้าใจเชิงลึกเกี่ยวกับการพัฒนาที่น่าตื่นเต้นนี้และนวัตกรรมทางเทคโนโลยีที่อยู่เบื้องหลัง LeanAgent
ในข่าวล่าสุดที่น่าตื่นเต้นในโลกคณิตศาสตร์ กลุ่มศิษย์เก่าจากมหาวิทยาลัย Tsinghua ใช้พลังของ AI เพื่อพิสูจน์ทฤษฎีบททางคณิตศาสตร์ 162 ทฤษฎีที่ไม่มีใครแก้มาก่อนได้สำเร็จ สิ่งที่น่าทึ่งยิ่งกว่านั้นคือเจ้าหน้าที่ชื่อ LeanAgent สามารถเอาชนะปัญหาการคาดเดาแบบพหุนาม Freiman-Ruzsa ของ Terence Tero ได้จริง นี่ทำให้เราเสียใจที่วิธีการวิจัยทางวิทยาศาสตร์ขั้นพื้นฐานได้รับการเปลี่ยนแปลงอย่างสมบูรณ์โดย AI
ดังที่เราทุกคนทราบกันดี แม้ว่าโมเดลภาษาในปัจจุบัน (LLM) จะเจ๋ง แต่โมเดลส่วนใหญ่ยังคงไม่เปลี่ยนแปลงและไม่สามารถเรียนรู้ความรู้ใหม่ทางออนไลน์ได้ การพิสูจน์ทฤษฎีบททางคณิตศาสตร์ขั้นสูงนั้นยากยิ่งกว่า อย่างไรก็ตาม LeanAgent ซึ่งพัฒนาโดยทีมวิจัยจาก Caltech, Stanford University และ University of Washington นั้นเป็นผู้ช่วย AI ที่มีความสามารถในการเรียนรู้ตลอดชีวิตที่สามารถเรียนรู้และพิสูจน์ทฤษฎีบทได้อย่างต่อเนื่อง
LeanAgent ตอบสนองต่อความยากลำบากทางคณิตศาสตร์ต่างๆ ผ่านเส้นทางการเรียนรู้ที่ออกแบบมาอย่างระมัดระวัง และใช้ฐานข้อมูลแบบไดนามิกเพื่อจัดการกระแสความรู้ทางคณิตศาสตร์อย่างต่อเนื่องเพื่อให้แน่ใจว่าจะไม่ลืมทักษะที่ได้เรียนรู้แล้วเมื่อเรียนรู้ความรู้ใหม่ การทดลองแสดงให้เห็นว่าประสบความสำเร็จในการพิสูจน์ทฤษฎีบททางคณิตศาสตร์ 162 ทฤษฎีที่ไม่มีใครสามารถแก้ได้มาก่อนจากไลบรารีโค้ดแบบ Lean 23 แห่ง และประสิทธิภาพของมันนั้นสูงกว่าโมเดลขนาดใหญ่แบบดั้งเดิมถึง 11 เท่า มันน่าทึ่งมาก!
ทฤษฎีบทเหล่านี้ครอบคลุมเนื้อหาทางคณิตศาสตร์ระดับสูงหลายด้าน รวมถึงปัญหาที่ยาก เช่น พีชคณิตนามธรรมและโทโพโลยีพีชคณิต LeanAgent ไม่เพียงแต่สามารถเริ่มต้นด้วยแนวคิดง่ายๆ และค่อยๆ จัดการกับหัวข้อที่ซับซ้อนเท่านั้น แต่ยังแสดงให้เห็นถึงประสิทธิภาพที่ยอดเยี่ยมในแง่ของความเสถียรและการโยกย้ายแบบย้อนกลับ
อย่างไรก็ตาม ความท้าทายของ Terence Tao ยังคงทำให้ AI รู้สึกหมดหนทาง แม้ว่าผู้พิสูจน์ทฤษฎีบทเชิงโต้ตอบ (ITP) เช่น ลีน จะมีบทบาทสำคัญในการทำให้เป็นทางการและการตรวจสอบการพิสูจน์ทางคณิตศาสตร์ แต่กระบวนการสร้างการพิสูจน์ดังกล่าวมักจะซับซ้อนและใช้เวลานาน โดยต้องใช้ขั้นตอนที่พิถีพิถันและไลบรารีรหัสทางคณิตศาสตร์ที่กว้างขวาง โมเดลขนาดใหญ่ขั้นสูง เช่น o1 และ Claude ยังมีแนวโน้มที่จะเกิดข้อผิดพลาดเมื่อต้องเผชิญกับการพิสูจน์แบบไม่เป็นทางการ ซึ่งเน้นย้ำถึงข้อบกพร่องของ LLM ในด้านความแม่นยำและความน่าเชื่อถือของการพิสูจน์ทางคณิตศาสตร์
การวิจัยที่ผ่านมาได้พยายามใช้ LLM เพื่อสร้างขั้นตอนการพิสูจน์ที่สมบูรณ์ เช่น LeanDojo ซึ่งเป็นเครื่องพิสูจน์ทฤษฎีที่สร้างขึ้นโดยการฝึกแบบจำลองขนาดใหญ่บนชุดข้อมูลเฉพาะ อย่างไรก็ตาม ข้อมูลสำหรับการพิสูจน์ทฤษฎีบทที่เป็นทางการนั้นมีน้อยมาก ซึ่งเป็นการจำกัดการนำไปประยุกต์ใช้วิธีนี้ในวงกว้าง อีกโครงการหนึ่งคือ ReProver เป็นแบบจำลองที่ได้รับการปรับให้เหมาะสมสำหรับไลบรารีโค้ดพิสูจน์ทฤษฎีบทแบบลีน Mathlib4 แม้ว่าจะครอบคลุมทฤษฎีบทและคำจำกัดความทางคณิตศาสตร์อย่างเป็นทางการมากกว่า 100,000 รายการ แต่มันถูกจำกัดอยู่เพียงขอบเขตของคณิตศาสตร์ระดับปริญญาตรี ดังนั้นจึงทำงานได้ไม่ดีเมื่อต้องเผชิญกับความซับซ้อนมากขึ้น ปัญหาที่ดี
เป็นที่น่าสังเกตว่าลักษณะแบบไดนามิกของการวิจัยทางคณิตศาสตร์นำมาซึ่งความท้าทายที่มากขึ้นมาสู่ AI นักคณิตศาสตร์มักจะทำงานหลายโครงการในเวลาเดียวกันหรือสลับกัน ตัวอย่างเช่น Terence Tao กำลังพัฒนางานวิจัยหลายสาขาในเวลาเดียวกัน รวมถึงการคาดเดา PFR และค่าเฉลี่ยสมมาตรของจำนวนจริง ตัวอย่างเหล่านี้แสดงให้เห็นถึงข้อบกพร่องที่สำคัญของวิธีการพิสูจน์ทฤษฎีบท AI ในปัจจุบัน นั่นคือ การขาดระบบ AI ที่สามารถเรียนรู้แบบปรับตัวและปรับปรุงในสาขาคณิตศาสตร์ต่างๆ โดยเฉพาะอย่างยิ่งเมื่อข้อมูลแบบ Lean มีจำกัด
นั่นคือเหตุผลที่ทีมงานของ LeanDojo ได้สร้าง LeanAgent ซึ่งเป็นกรอบการเรียนรู้ตลอดชีวิตใหม่ที่ออกแบบมาเพื่อแก้ปัญหาความท้าทายข้างต้น ขั้นตอนการทำงานของ LeanAgent รวมถึงการได้มาซึ่งความซับซ้อนของทฤษฎีบทเพื่อกำหนดหลักสูตรการเรียนรู้ การสร้างสมดุลระหว่างความมั่นคงและความยืดหยุ่นในกระบวนการเรียนรู้ผ่านการฝึกอบรมแบบก้าวหน้า และใช้การค้นหาแบบต้นไม้อันดับแรกที่ดีที่สุดเพื่อค้นหาทฤษฎีบทที่ยังไม่ผ่านการพิสูจน์
LeanAgent ทำงานร่วมกับโมเดลขนาดใหญ่ใดๆ เพื่อปรับปรุงความสามารถในการวางลักษณะทั่วไปผ่านการ "ดึงข้อมูล" นวัตกรรมอยู่ที่การใช้ฐานข้อมูลไดนามิกแบบกำหนดเองเพื่อจัดการความรู้ทางคณิตศาสตร์ที่เพิ่มมากขึ้น และกลยุทธ์การเรียนรู้หลักสูตรตามโครงสร้างการพิสูจน์แบบ Lean เพื่อช่วยเรียนรู้เนื้อหาทางคณิตศาสตร์ที่ซับซ้อนมากขึ้น
เพื่อจัดการกับปัญหาการลืมอันหายนะของ AI นักวิจัยได้นำวิธีการฝึกอบรมแบบก้าวหน้ามาใช้เพื่อช่วยให้ LeanAgent สามารถปรับเข้ากับความรู้ทางคณิตศาสตร์ใหม่ ๆ ได้อย่างต่อเนื่องโดยไม่ลืมการเรียนรู้ก่อนหน้านี้ กระบวนการนี้เกี่ยวข้องกับการฝึกอบรมเพิ่มเติมเกี่ยวกับชุดข้อมูลใหม่แต่ละชุด เพื่อให้มั่นใจถึงความสมดุลที่เหมาะสมที่สุดของความเสถียรและความยืดหยุ่น
ด้วยการฝึกอบรมแบบก้าวหน้านี้ LeanAgent มีประสิทธิภาพที่ยอดเยี่ยมในการพิสูจน์ทฤษฎีบท โดยประสบความสำเร็จในการพิสูจน์ปัญหายากๆ 162 ข้อที่มนุษย์ไม่สามารถแก้ไขได้ โดยเฉพาะอย่างยิ่งในทฤษฎีบทที่ท้าทายของพีชคณิตนามธรรมและโทโพโลยีพีชคณิต ความสามารถในการพิสูจน์ทฤษฎีบทใหม่นั้นสูงกว่า ReProver แบบคงที่ถึง 11 เท่า ในขณะที่ยังคงความสามารถในการพิสูจน์ทฤษฎีบทที่รู้จัก
LeanAgent แสดงลักษณะของการเรียนรู้แบบก้าวหน้าในระหว่างกระบวนการพิสูจน์ทฤษฎีบท โดยค่อยๆ เปลี่ยนจากทฤษฎีบทที่เรียบง่ายไปเป็นทฤษฎีบทที่ซับซ้อนมากขึ้น เพื่อพิสูจน์ความลึกในการเรียนรู้ความรู้ทางคณิตศาสตร์ ตัวอย่างเช่น แสดงให้เห็นถึงความเข้าใจอย่างลึกซึ้งเกี่ยวกับคณิตศาสตร์โดยการพิสูจน์ทฤษฎีบทโครงสร้างพีชคณิตพื้นฐานที่เกี่ยวข้องกับทฤษฎีกลุ่มและทฤษฎีวงแหวน โดยรวมแล้ว LeanAgent นำโอกาสที่น่าตื่นเต้นมาสู่ชุมชนคณิตศาสตร์ด้วยความสามารถในการเรียนรู้และปรับปรุงอย่างต่อเนื่องอันทรงพลัง!
ที่อยู่กระดาษ: https://arxiv.org/pdf/2410.06209
การเกิดขึ้นของ LeanAgent บ่งชี้ว่า AI จะมีบทบาทสำคัญมากขึ้นในด้านการวิจัยทางคณิตศาสตร์ และอาจมีกรณีอื่นๆ ในอนาคตที่ใช้พลังของ AI เพื่อแก้ปัญหาทางคณิตศาสตร์ที่ซับซ้อน ไม่ต้องสงสัยเลยว่าสิ่งนี้เป็นการเปิดทิศทางใหม่สำหรับการวิจัยทางคณิตศาสตร์ และยังให้แนวคิดและวิธีการใหม่ๆ สำหรับการสำรวจในสาขาวิทยาศาสตร์อื่นๆ รอคอยผลลัพธ์ที่น่าอัศจรรย์มากขึ้นในอนาคต!