- ปัญหา Erdős #728 เพิ่งถูก เครื่องมือ AI แก้ได้เกือบอัตโนมัติ กลายเป็นหมุดหมายใหม่ของการทำวิจัยคณิตศาสตร์แบบอัตโนมัติ
- ปัญหานี้เดิมเป็น คำถามเกี่ยวกับการแยกตัวประกอบเฉพาะของสัมประสิทธิ์ทวินาม ที่ Erdős, Graham, Ruzsa, Strauss เสนอไว้ในปี 1975 แต่เพราะเงื่อนไขกำกวมจึงไม่ถูกจัดการอย่างชัดเจนมาเป็นเวลานาน
- ChatGPT สร้างบทพิสูจน์ภายใต้ข้อจำกัดที่ปรับแล้ว และ Aristotle ทำให้เป็น Lean formal proof พร้อมแก้ข้อผิดพลาดโดยอัตโนมัติ
- หลังจากนั้นผู้เข้าร่วมหลายคนได้ ใช้ ChatGPT เขียนใหม่เป็นภาษาธรรมชาติ และปรับปรุงเวอร์ชันที่เสริมการเชื่อมโยงกับงานวิจัยและโครงสร้างการเล่าเรื่องซ้ำแล้วซ้ำอีก
- Terence Tao ประเมินว่ากระบวนการนี้แสดงให้เห็นว่า ความสามารถของ AI ในการเขียนและแก้ไขบทพิสูจน์อย่างรวดเร็ว มีศักยภาพจะเปลี่ยนวิธีการเขียนงานวิจัยเอง
ปัญหา Erdős #728 ที่ AI แก้ได้
- เมื่อไม่นานมานี้ การประยุกต์ใช้เครื่องมือ AI ทำให้การแก้ปัญหา Erdős มีความคืบหน้าใหม่ โดยปัญหา #728 ถูก AI แก้ได้เกือบอัตโนมัติ
- หลังความพยายามแรก มีการแก้ไขตามข้อเสนอแนะแล้วจึงสำเร็จ
- ผลลัพธ์นี้ไม่พบว่ามีการทำซ้ำแบบเดียวกันในวรรณกรรมเดิม และมีเพียงผลลัพธ์คล้ายกันจากวิธีที่ใกล้เคียงกันเท่านั้น
- กรณีนี้แสดงให้เห็นว่าในช่วงไม่กี่เดือนที่ผ่านมา ความสามารถของ AI ในการแก้ปัญหาคณิตศาสตร์ได้พัฒนาขึ้นจริง
- ในอดีตก็เคยมีกรณีที่ AI แก้ปัญหา Erdős ได้ แต่ส่วนใหญ่ภายหลังพบว่าเป็นคำตอบที่มีอยู่แล้วในวรรณกรรม
- ปัญหานี้เดิมทีคำบรรยายของ Erdős ถูกนำเสนอในรูปแบบที่ไม่ถูกต้อง และเพิ่งถูกประกอบสร้างใหม่ให้เป็นรูปแบบที่ตั้งใจไว้เมื่อไม่นานนี้
- จึงอธิบายได้ว่าทำไมวรรณกรรมเดิมจึงแทบไม่มีงานที่เกี่ยวข้อง
ประวัติของปัญหาและแนวทางช่วงแรก
- ในปี 1975 Erdős, Graham, Ruzsa, Strauss ศึกษาการแยกตัวประกอบเฉพาะของ สัมประสิทธิ์ทวินาม (2n choose n) และเสนอปัญหาที่เกี่ยวข้องหลายข้อ
- หนึ่งในนั้นถามถึงการมีอยู่ของ a, b, n แบบอนันต์ที่ทำให้เป็นจริงทั้งเงื่อนไข a!b! | n!(a+b−n)! และ a+b > n + C log n
- อย่างไรก็ตาม มีหลายจุดที่อธิบายไม่ชัดเจน เช่น ขนาดของ C (เล็กหรือใหญ่)
- เมื่อไม่กี่เดือนก่อน ทีม AlphaProof พบคำตอบแบบง่ายของปัญหา แต่เนื่องจากไม่สอดคล้องกับเจตนารมณ์ของปัญหา จึงเพิ่มข้อจำกัด a,b ≤ (1−ε)n
- หลังจากนั้นแม้จะใช้ AI ช่วยค้นวรรณกรรม ก็ยังแทบไม่พบงานที่เกี่ยวข้อง
ความร่วมมือระหว่าง ChatGPT และ Aristotle
- วันที่ 4 มกราคม ChatGPT สร้างบทพิสูจน์สำหรับกรณีของ C ขนาดเล็ก ภายใต้ข้อจำกัดที่ปรับแล้ว
- บทพิสูจน์นี้ถูกทำให้เป็น Lean formal proof โดย Aristotle
- ต่อมาเมื่อทบทวนต้นฉบับอีกครั้ง ก็ยืนยันได้ว่าบทความต้นฉบับได้ครอบคลุมกรณี C ขนาดเล็กไว้แล้ว
- ผู้เข้าร่วมอีกคน แปลง Lean proof เป็นภาษาธรรมชาติด้วย ChatGPT และผ่านการสนทนาเพิ่มเติมก็จัดทำ เวอร์ชันที่ปรับปรุงแล้ว
- เวอร์ชันนี้อุดช่องว่างของบทพิสูจน์บางส่วน แต่ยังคงมี สำนวนที่แข็งและแปลกแบบ AI และ การอ้างอิงวรรณกรรมที่ยังไม่เพียงพอ
- ถึงอย่างนั้นก็อ่านได้ดีพอในระดับที่ สามารถเข้าใจแนวคิดหลักได้
การเขียนใหม่ครั้งใหญ่และผลลัพธ์ที่ดีขึ้น
- ผ่านพรอมป์เพิ่มเติม ChatGPT สร้าง บทพิสูจน์ที่ขยายไปถึงกรณี C ขนาดใหญ่
- แม้จะมีข้อผิดพลาดบางส่วน แต่ Aristotle แก้ไขให้อัตโนมัติ และทำให้เสร็จเป็น บทพิสูจน์ที่ตรวจสอบด้วย Lean
- ผู้เข้าร่วมคนที่สาม บีบอัด Lean proof แล้วผู้เข้าร่วมอีกคนก็ สนทนากับ ChatGPT เป็นเวลานาน เพื่อ
- เขียนใหม่ให้อยู่ในรูปบทความที่สมบูรณ์ยิ่งขึ้น พร้อมการเชื่อมโยงวรรณกรรมและโครงสร้างการเล่าเรื่องที่แน่นขึ้น
- ผลลัพธ์ถูกประเมินว่ามี กลิ่นอายของงานที่สร้างโดย AI น้อยลง และมี คุณภาพใกล้เคียงระดับบทความวิจัย
- Tao ระบุว่าเขาได้ตรวจทานข้อความนี้ในฟอรัมปัญหา Erdős
AI กำลังเปลี่ยนวิธีเขียนบทความวิจัย
- Tao มองว่าแม้บทความฉบับสุดท้ายยังคง ต้องให้มนุษย์เขียนส่วนสำคัญเอง
- แต่ก็ประเมินว่า การผสาน AI กับ Lean ได้เพิ่ม ความเร็วในการเขียนและแก้ไขบทพิสูจน์ อย่างมาก
- แต่เดิมการทำให้บทความหนึ่งอ่านง่ายต้องใช้เวลามาก
- และการแก้ไขตามความเห็นของผู้ประเมินก็มักจำกัดอยู่ที่ การเปลี่ยนแปลงเฉพาะจุด
- แต่ตอนนี้เมื่อ ความสามารถของ AI ในการสร้างและแก้ไขข้อความ ผสานกับ ความสามารถตรวจสอบของเครื่องมือพิสูจน์เชิงรูปแบบ
- ก็สามารถ สร้างบทความเวอร์ชันใหม่ได้อย่างรวดเร็วในหลายระดับของความละเอียดและการบรรยาย
- นอกจาก “บทความทางการ” เพียงฉบับเดียวแล้ว ยังอาจมี เวอร์ชันเสริมที่ AI สร้างขึ้นจำนวนมาก
- ซึ่งเปิดความเป็นไปได้ในการมอบ มุมมองที่หลากหลายและคุณค่าเพิ่มเติม
ปฏิกิริยาจากชุมชน
- ผู้ใช้บางคนอธิบาย คุณค่าเพิ่มเติมของเอกสารที่ AI สร้าง ว่าเป็น “ความสามารถในการมองจากอีกมุมหนึ่ง”
- นักคณิตศาสตร์คนอื่น ๆ เสนอว่าจำเป็นต้องมีการวัด ความเป็นต้นฉบับของผลลัพธ์จาก AI และ การประเมินความคล้ายกับวรรณกรรมเดิม
- ตัวอย่างเช่น มีข้อเสนอให้วัดความคล้ายเชิงปริมาณผ่าน การเปรียบเทียบความยาวของ Lean formal proof
- ความเห็นอีกส่วนหนึ่งระบุว่า AI สามารถเขียนบทความใหม่ทั้งระบบได้เหมือนการ refactor โค้ด
- ทำให้นักวิจัยควรไปโฟกัสกับ การออกแบบโครงสร้างเอกสารในระดับที่สูงขึ้น
- บางคนยังคง สงสัยว่า AI จะเข้ามาแทนบทบาทของนักคณิตศาสตร์ได้หรือไม่
- แต่อีกฝ่ายมองว่านี่คือ โอกาสใหม่ของการทำงานร่วมกันและการขยายขอบเขตความคิด
1 ความคิดเห็น
ความเห็นจาก Hacker News
ฉันทำงานที่ Harmonic และอยากชี้แจงความเข้าใจผิดบางอย่างเกี่ยวกับ Aristotle ที่เราสร้างขึ้น
Aristotle ใช้ เทคนิค AI สมัยใหม่อย่างจริงจัง รวมถึงการทำ language modeling ด้วย
หากป้อนบทพิสูจน์แบบไม่เป็นทางการที่เขียนเป็นภาษาอังกฤษเข้าไป เมื่อบทพิสูจน์นั้นถูกต้อง ก็มีโอกาสสูงที่จะถูกแปลเป็น Lean ได้ นั่นจึงเป็นสัญญาณที่ชัดเจนว่าบทพิสูจน์ภาษาอังกฤษนั้นแข็งแรง
เมื่อถูกทำให้เป็นแบบรูปนัยใน Lean แล้ว ก็แทบไม่มีข้อกังขาเลยว่าบทพิสูจน์นั้นถูกต้อง นี่คือแนวทางหลักของเรา — หากค้นหาคำตอบได้ผ่านการสำรวจที่ขับเคลื่อนด้วย AI เราก็สามารถรับประกันความถูกต้องของผลลัพธ์ได้ ไม่ว่าความซับซ้อนจะมากแค่ไหนก็ตาม
Rust ใช้ชุดกฎที่ตายตัวเพื่อรับประกัน memory safety แต่กฎเหล่านี้ค่อนข้างเรียบง่ายและมีข้อจำกัด ถ้าระบบแบบ Aristotle ถูกผนวกเข้ากับคอมไพเลอร์ แล้วทำให้โค้ดที่มี บทพิสูจน์ความถูกต้อง ผ่านได้โดยอัตโนมัติ ก็คงยอดเยี่ยมมาก
สงสัยว่า Harmonic จะต้องใช้เวลาอีกนานแค่ไหนกว่าจะทำให้คณิตศาสตร์ที่มนุษย์เขียนไว้ส่วนใหญ่กลายเป็นรูปแบบทางการได้ คู่แข่งอย่าง Christian Szegedy บอกว่าน่าจะทำได้ภายในปีนี้
จากคำอธิบายของ Terence Tao ดูเหมือนว่ามนุษย์เป็นคนส่งต่อผลลัพธ์ไปมาระหว่างเครื่องมือ AI สองตัว และ AI ทำหน้าที่ เติมช่องว่าง ที่มนุษย์หาเจอ
จึงใกล้เคียงกับ ความร่วมมือ ระหว่างมนุษย์กับ AI มากกว่าการแก้ปัญหาแบบอัตโนมัติเต็มรูปแบบ กล่าวคือ ผู้เชี่ยวชาญเป็นคนนำ และ AI เป็นผู้ช่วย
การนำบทพิสูจน์เดิมมาสร้างใหม่หรือประกอบเข้าด้วยกันในรูปแบบใหม่ เป็น กระบวนการที่น่าเบื่อหรือซับซ้อน สำหรับมนุษย์ แต่ AI ทำสิ่งนี้ได้ด้วยความเร็วระดับเหนือมนุษย์
แนวทางแบบนี้จะเปิดศักยภาพมหาศาลได้แม้ก่อนจะไปถึง AGI เสียอีก ดูเหมือนว่าเรากำลังเข้าสู่ยุคที่นักคณิตศาสตร์ใช้ AI เป็นเครื่องมือเพื่อจัดการปัญหายากระดับ Millennium Problems
คุณค่าที่แท้จริงของ LLM อยู่ที่การเสนอ มุมมองใหม่ ในหัวข้อที่อธิบายออกมาเป็นภาษาได้
ถ้าอ่าน โพสต์อธิบาย ที่คนซึ่งแก้ปัญหาจริงเขียนไว้ จุดที่น่าประทับใจคือได้ผลลัพธ์ออกมา ด้วยพรอมป์ต์เพียงไม่กี่ชุด โดยไม่มี pipeline ขนาดใหญ่
โมเดลยุคหลังใช้ทรัพยากรประมวลผลมากกว่านี้มาก จึงดูว่านี่อาจเป็นเพียง ผลงานระดับขอบล่าง เท่านั้น
Terence Tao สร้างหน้า wiki ชื่อ “AI contributions to Erdős problems” ขึ้นมาแล้ว
จาก หน้า GitHub และ โพสต์บน Mathstodon ผลลัพธ์ครั้งนี้ (ปัญหา 728) คือ รายการสีเขียว รายการแรกในหน้านั้น หรือก็คือกรณีแรกที่ AI แก้ได้จริง
สงสัยว่าผู้เชี่ยวชาญในสาขาซับซ้อนอย่างฟิสิกส์หรือคณิตศาสตร์ ใช้ AI สนทนาเพื่อขอความช่วยเหลือกันด้วยหรือไม่
ถ้าแยกตามสาขา ประโยชน์จะลดหลั่นกันไปดังนี้: การเขียนโปรแกรม > applied ML > สถิติ/คณิตศาสตร์ประยุกต์ > คณิตศาสตร์บริสุทธิ์
ตอนนี้สามารถลองใช้ Aristotle ได้ทันที — https://aristotle.harmonic.fun/
และลิงก์ไปยังหน้าส่วนตัวของ Stanford ก็ผิดด้วย (ต้องเอา www ออก)
ผลลัพธ์ครั้งนี้เป็นทฤษฎีบทเกี่ยวกับจำนวนเต็ม ซึ่งเป็นขอบเขตที่ โครงสร้างพื้นฐานของ Mathlib รองรับได้ดี
นิยามที่ใช้ก็ไม่ซับซ้อนมาก จึงทำให้บทพิสูจน์ประเภทนี้มีโอกาสสำเร็จสูง ถึงอย่างนั้นก็ยังเป็นความสำเร็จที่น่าทึ่งมาก
นี่เป็นตัวอย่างที่แสดงให้เห็นศักยภาพของ แนวทาง AI แบบเฉพาะทาง ที่ก้าวเลย LLM ทั่วไปไปแล้ว
บทความของ Aristotle อยู่ที่ arXiv:2510.01346
แค่ใช้สถาปัตยกรรม Transformer ก็ไม่ได้แปลว่าจะเป็น LLM ทั้งหมด — ถ้า ไม่ได้ฝึกด้วยข้อมูลภาษา ก็เรียกว่า LLM ไม่ได้
กล่าวคือ ทุกขั้นตอนล้วนอยู่บนพื้นฐานของ LLM
ภายในปี 2026 ดูเหมือนว่า AI จะเริ่มจัดการ ปัญหาคณิตศาสตร์ที่ยังไม่มีคำตอบ ได้มากขึ้นเรื่อย ๆ
กรณีนี้แม้ยังไม่ใช่อัตโนมัติเต็มรูปแบบ แต่ก็ใกล้เคียงกับระดับที่ AI แก้ได้เองเกือบหมดหลังได้รับฟีดแบ็กจากมนุษย์
ผมคิดว่าข้อถกเถียงแบบ “LLM ก็เป็นแค่นกแก้วเชิงสถิติ” คงจบแล้ว จากนี้ไปประเด็นจริงจะอยู่ที่ ทำอย่างไรให้ใช้งานได้จริง