Lean4 ช่วยค้นพบบั๊กเล็ก ๆ ในงานวิจัยล่าสุดของ Terence Tao
(mathstodon.xyz)- Terence Tao พบข้อผิดพลาดเล็กน้อยแต่ไม่ใช่เรื่องเล็กในงานวิจัยของตน ระหว่างทำ โครงการทำให้เป็นรูปแบบทางการด้วย Lean4
- ข้อผิดพลาดปรากฏใน การให้เหตุผลหน้า 6 ของงานวิจัยบน arXiv หมายเลข
2310.05328โดย1/2 log((n - 1)/(n - k - 1))มีค่าเป็นอนันต์เมื่อn = 3, k = 2 - ปัญหานี้จำกัดอยู่กับค่า
nขนาดเล็ก โดยสำหรับn >= 8การให้เหตุผลเดิมยังใช้ได้ และกรณีnเล็กสามารถจัดการโดยตรงด้วยวิธีที่หยาบกว่าได้ - Lean ต้องการการพิสูจน์
0 < n - 3แต่สมมติฐานมีเพียงn > 2ทำให้ tacticlinarithไม่สามารถหาความขัดแย้งที่จำเป็นได้ - Tao มองว่าสามารถแก้การให้เหตุผลนี้ได้ด้วยการปรับ ค่าคงที่เชิงตัวเลข บางส่วน และจะใส่ เชิงอรรถ ในฉบับใหม่ว่าความไม่แม่นยำของการให้เหตุผลเดิมถูกค้นพบระหว่างความพยายามทำให้เป็นรูปแบบทางการด้วย Lean
ข้อผิดพลาดที่การทำให้เป็นรูปแบบทางการด้วย Lean4 เปิดเผย
- Terence Tao พบว่ามีบั๊กเล็กน้อยแต่ไม่ใช่เรื่องเล็กในงานวิจัยของตน ระหว่างดำเนิน โครงการทำให้เป็นรูปแบบทางการด้วย Lean4
- เป้าหมายของการทำให้เป็นรูปแบบทางการคือการให้เหตุผลในหน้า 6 ของงานวิจัย arXiv หมายเลข
2310.05328 - นิพจน์ที่เป็นปัญหามีรูปแบบดังนี้
1/2 log((n - 1)/(n - k - 1))
- นิพจน์นี้มีค่าเป็นอนันต์ในกรณี
n = 3, k = 2
ขอบเขตของข้อผิดพลาดและวิธีแก้ไข
- ปัญหานี้เกิดขึ้นเฉพาะเมื่อค่า
nมีขนาดเล็ก- สำหรับ
n >= 8การให้เหตุผลดังกล่าวยังคงใช้ได้ - สำหรับ
nเล็ก สามารถจัดการโดยตรงด้วยวิธีที่หยาบกว่าได้ แต่ค่าคงที่จะด้อยลง
- สำหรับ
- Tao มองว่าสามารถแก้การให้เหตุผลในหน้านั้นได้ด้วยการเปลี่ยน ค่าคงที่เชิงตัวเลข บางตัว
- ในงานวิจัยฉบับใหม่ เขาวางแผนจะเพิ่ม เชิงอรรถ ว่าการให้เหตุผลเดิมไม่แม่นยำอยู่เล็กน้อย และถูกค้นพบระหว่างการพยายามทำให้เป็นรูปแบบทางการด้วย Lean
จุดเฉพาะที่ Lean ไปต่อไม่ได้
- ณ จุดที่การทำให้เป็นรูปแบบทางการล้มเหลว Lean ต้องการให้พิสูจน์
0 < n - 3- สมมติฐานที่ใช้ได้มีเพียง
n > 2 - tactic
linarithไม่สามารถสรุปความขัดแย้งจากการปฏิเสธของ0 < n - 3ได้
- สมมติฐานที่ใช้ได้มีเพียง
1 ความคิดเห็น
ความคิดเห็นจาก Hacker News
เมื่อต้นเดือนนี้ เขาเริ่มเรียน Lean4 ด้วยความช่วยเหลือของ GPT-4: https://mathstodon.xyz/@tao/111208692505811257
โพสต์ Mastodon ของเขาจำนวนมากในเดือนนี้เกี่ยวกับความคืบหน้าในการเรียนรู้ และเป็นกรณีตัวอย่างที่น่าสนใจว่า โมเดลภาษาขนาดใหญ่ สามารถเร่งงานของผู้ที่มีผลงานระดับสูงสุดได้มากเพียงใด
น่าสนใจว่าเครื่องมือแบบนี้อาจยิ่งเพิ่มความเหลื่อมล้ำได้ หากมีแต่ผู้มีทักษะสูงเท่านั้นที่ใช้มันได้อย่างมีประสิทธิภาพ
ถ้าอยากเริ่มสัมผัส Lean4 แบบง่าย ๆ Natural Number Game เป็นตัวเลือกที่ดี: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
ถ้าอยากอ่านอย่างเดียวโดยไม่เล่นเกม ดูที่นี่: https://lean-lang.org/theorem_proving_in_lean4/introduction.html
ตอนแรกเคยเขียน Alloy ผิดเป็น Allow
หลายปีก่อน ระหว่างหาวิธีลดข้อผิดพลาดในโปรแกรมที่ผมเขียน ผมได้รู้จัก TLA+ ของ Lamport และได้เรียนรู้วิธีเขียนสเปกเชิงรูปแบบ โดยคิดพฤติกรรมของโปรแกรมเป็น state machine
TLA+ ช่วยให้ผมเข้าใจ abstraction ได้ชัดเจนขึ้น และหลังจากนั้นก็พบซีรีส์ Software Foundations ที่ใช้ proof assistant อย่าง Coq เพื่อสร้างซอฟต์แวร์ที่ถูกต้องเชิงรูปแบบด้วย แบบฝึกหัดทำออกมาเหมือนเกมเล็ก ๆ จึงแก้โจทย์ได้ค่อนข้างสนุก: https://softwarefoundations.cis.upenn.edu/
สเปกเชิงรูปแบบซึ่งเป็น abstraction ระดับสูงจะเน้นไปที่ภาษาเฉพาะสำหรับอธิบายโค้ด ส่วน code contract ซึ่งเป็น abstraction ระดับต่ำจะใกล้กับการแทนที่ตรรกะการตรวจสอบด้วยโมเดลที่ดีกว่า ครั้งหนึ่ง C# เคยมี Code Contracts[1] ซึ่งเป็นวิธีที่เรียบง่ายแต่ทรงพลังในการตรวจสอบ contract ตอนคอมไพล์ด้วย Z3 SMT solver[2] แต่ไม่กี่ปีต่อมาก็ถูกยกเลิก[3] และเมื่อถูกนำออกจาก .NET Runtime ก็เท่ากับจบลงโดยปริยาย ตอนนี้สิ่งที่ใกล้เคียงที่สุดใน C# น่าจะเป็น Dafny[4] และฝั่งพัฒนา C# ก็ยังคงพิจารณาวิธีนำสิ่งนี้เข้าไปในภาษาโดยตรง[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Idris2 ดูเหมือนจะมุ่งเป็นภาษาทั่วไป พร้อมทั้งให้ระบบชนิดข้อมูลที่ก้าวหน้ากว่าสำหรับการพิสูจน์ทฤษฎีบท: https://github.com/idris-lang/Idris2
ยังมีหนังสือที่แตกแขนงออกมาในระดับหนึ่ง ซึ่งใช้ Agda แทน Coq ด้วย: https://plfa.github.io/
ยังไม่ได้อ่าน แต่ใส่ไว้ในลิสต์แล้ว และคิดว่า Agda หรือ Idris น่าจะให้ความรู้สึกเหมือนภาษาโปรแกรมมากกว่า Coq
ผมคาดหวังกับ dependent types มากจริง ๆ แต่คงยังออกมาได้ยากในระยะใกล้นี้
Dependent Haskell กำลังอยู่ระหว่างพัฒนา แต่ได้ยินว่าการยัดมันเข้าไปในภาษาที่มีอยู่เดิมภายหลังนั้นยาก และผู้สร้าง Idris เองก็เคยบอกว่าหวังให้ Idris เป็นโมเดลสำหรับภาษาอื่น แต่การยอมรับในกระแสหลักดูจะยาก Coq, Agda, F* ก็ไม่ได้ถูกออกแบบมาเป็นภาษาทั่วไป การทำคอมไพเลอร์นั้นซับซ้อนและไวยากรณ์ก็อาจยืดยาวได้ แต่สิ่งที่ผมต้องการคือความเรียบง่าย ผมอยากเข้ารหัสทุกอย่างที่รู้เกี่ยวกับอินพุตและเอาต์พุต ตอนนี้ในภาษากระแสหลัก เรามักรู้เกี่ยวกับอาร์กิวเมนต์หรือเอาต์พุตมากกว่าที่ระบบชนิดข้อมูลอนุญาตให้แสดงออกได้
ถ้าเป็นแนวทางแบบ gradual เหมือน TypeScript ที่สามารถเพิ่มข้อมูลข้อจำกัดของค่าระดับ type ในตำแหน่งใดก็ได้ โดยไม่ต้องพิสูจน์ทุกอย่างทุกที่ก็คงดี
ตัวอย่างเช่น หากเรารู้ทั้งรายการตัวเลขและความยาวของมัน ก็สามารถใช้ dependent types สร้าง type ของรายการที่รวมความยาวไว้อย่างชัดเจน และรับประกันได้ตอนคอมไพล์ว่าการดำเนินการจะรักษาความยาวนั้นไว้ หากกำหนดฟังก์ชันให้รับเฉพาะรายการความยาว 3 แต่ส่งรายการความยาว 4 เข้าไป ก็จะคอมไพล์ไม่ผ่าน ทำให้จับข้อผิดพลาดได้ก่อนรัน ให้ความรู้สึกเหมือนเป็น ชั้นตรวจสอบความปลอดภัยเพิ่มเติม ที่ทำให้ type มีพลังในการสื่อความหมายมากขึ้น และเข้ารหัสความสัมพันธ์ที่ซับซ้อนระหว่างตัวแปรได้
หากหนึ่งในผู้มีปัญญาโดดเด่นที่สุดในยุคของเราสามารถขยายขอบเขตการทำงานด้วยการผสาน โมเดลภาษาขนาดใหญ่กับการพิสูจน์อัตโนมัติ อนาคตของชุดเทคโนโลยีนี้ก็ดูสดใสมาก
จุดเริ่มต้นคือการแก้บั๊ก ต่อด้วยการช่วยตรวจสอบความถูกต้อง และท้ายที่สุดน่าจะผลักดันการค้นพบใหม่ ๆ พร้อมขยายขีดจำกัดออกไป เราน่าจะต้องมีคำเรียกปรากฏการณ์ที่ไดนามิกแบบกฎของมัวร์ไป “แพร่เชื้อ” ให้กับสาขาที่เดิมทีไม่มีคุณสมบัติสะสมแบบนั้น สำหรับบริบทเพิ่มเติม Terence Tao กำลังใช้ Copilot เพื่อเรียนรู้ Lean: https://mathstodon.xyz/@tao/111271244206606941
แม้เขาอาจทำได้โดยไม่ต้องมี Copilot แต่แรงเสียดทานในการยอมรับเครื่องมือใหม่อาจทำให้ไม่ได้เริ่มด้วยซ้ำ โมเดลภาษาขนาดใหญ่มีศักยภาพสูงในสถานการณ์แบบ “จักรยานสำหรับความคิด” เช่นนี้
เมื่อไม่กี่ปีก่อน ผมก็เคยพบบั๊กหนึ่งในบทความบล็อกคณิตศาสตร์ของ Terence Tao ด้วย พอแจ้งไป เขาก็แก้ไขและกล่าวขอบคุณ
แน่นอนว่ามันไม่ได้ขึ้นหน้าแรกของ Hacker News
ตอนแรกกังวลว่า Lean4 จะเป็นโมเดลภาษาขนาดใหญ่อีกตัว แต่จริง ๆ แล้วเป็น เครื่องมือที่แข็งแกร่งและเชื่อถือได้ พอสมควร
สงสัยว่าสามารถผสาน ตัวตรวจสอบพิสูจน์แบบเป็นทางการ อย่างตัวตรวจสอบพิสูจน์ของ Lean เข้ากับโมเดลภาษา ที่สร้างคู่ “ข้อคาดการณ์-บทพิสูจน์” สังเคราะห์ในภาษาทางการอย่าง Lean ได้หรือไม่
เราสามารถใช้ตัวตรวจสอบพิสูจน์ของ Lean ตรวจสอบโดยอัตโนมัติว่าบทพิสูจน์สังเคราะห์ที่โมเดลภาษาเขียนขึ้นนั้นถูกต้องหรือไม่ แล้วนำข้อมูลนั้นไปใช้เป็นสัญญาณรางวัลของการเรียนรู้แบบเสริมกำลังกับโมเดลภาษาต้นทาง เพื่อทำให้มันเขียนบทพิสูจน์ได้ดีขึ้น หรือจะใช้บทพิสูจน์สังเคราะห์ที่ถูกต้องจากรอบก่อนหน้าเป็นข้อมูลฝึกเพื่อฝึกโมเดลใหม่ก็ได้ นอกจากนี้ยังทำให้มีลักษณะเชิงปฏิปักษ์มากขึ้นได้ด้วย โดยแยกเป็นโมเดลสร้างข้อคาดการณ์และโมเดลพิสูจน์/หักล้าง แล้วเพิ่มโมเดลที่คาดการณ์ว่าบทพิสูจน์สังเคราะห์จะผ่านการตรวจสอบจากตัวตรวจสอบพิสูจน์ของ Lean หรือไม่ ยิ่งโมเดลคาดการณ์ว่าความน่าจะเป็นของคำตอบถูกต่ำเท่าไร เมื่อโมเดลสร้างบทพิสูจน์ให้บทพิสูจน์ที่ถูกต้องจริง ก็จะได้รับรางวัลมากขึ้นเท่านั้น สุดท้าย หากเพิ่มโมเดลที่คาดการณ์รางวัลที่โมเดลสร้างบทพิสูจน์จะได้รับสำหรับข้อคาดการณ์สังเคราะห์เฉพาะหนึ่ง ๆ โมเดลสร้างข้อคาดการณ์ก็จะได้รับรางวัลจากการสร้างข้อคาดการณ์ที่มีรางวัลคาดหวังสูง ซึ่งไม่ยากหรือไม่ง่ายเกินไปสำหรับโมเดลสร้างบทพิสูจน์ ระบบโดยรวมอาจสร้างบทพิสูจน์สังเคราะห์ที่ยากขึ้นเรื่อย ๆ และนำไปสู่การเรียนรู้ด้วยตนเองที่ดีขึ้นของโมเดลสร้างบทพิสูจน์ โดยหลักการแล้วอาจขยายไปถึงความสามารถเหนือมนุษย์ในการสร้างบทพิสูจน์ได้ คล้ายกับ GAN หรือการเล่นกันเองของ AlphaGo Zero ส่วนที่ยากคือการบูตสแตรปในช่วงต้น เพราะการฝึกโมเดลสร้างในครั้งแรกต้องใช้ข้อมูลบทพิสูจน์ Lean ที่มนุษย์จัดหาให้ แต่เมื่อบทพิสูจน์สังเคราะห์ดีพอแล้ว ระบบก็สามารถเรียนรู้ด้วยตนเองต่อไปได้โดยอัตโนมัติ
ท้ายที่สุดเราอาจได้โมเดลที่รู้ทฤษฎีบททั้งหมดและบทพิสูจน์ที่ถูกต้องทั้งหมดในวรรณกรรมคณิตศาสตร์
สำหรับขั้นแรก ๆ ที่เริ่มจากการเรียนรู้แบบมีผู้สอนด้วยบทพิสูจน์ที่มีอยู่เพื่อค้นหาบทพิสูจน์ใหม่ มี TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) เป็นต้น ส่วนใหญ่มีโมเดลภาษาในรูปแบบใดรูปแบบหนึ่งอยู่ภายใน แต่ถ้ากำลังมองหาโมเดลภาษาขนาดใหญ่ที่ได้รับความสนใจมากในช่วงหลัง ก็มี GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), COPRA (https://arxiv.org/abs/2310.04353) อย่างไรก็ตาม ในตอนนี้โมเดลเหล่านี้ดูเหมือนจะยังไม่มีประสิทธิภาพเท่ากับเครื่องมือเฉพาะทางที่ไม่ใช่โมเดลภาษาขนาดใหญ่ ในด้านการเรียนรู้ด้วยการเรียนรู้แบบเสริมกำลังที่ก้าวข้ามบทพิสูจน์ที่มนุษย์เขียน มี TacticZero (https://openreview.net/forum?id=edmYVRkYZv), บทความของ OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), งานในตระกูล HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491) รวมถึงงานที่ทีม University of Massachusetts และฉันกำลังทำอยู่
บริบทก่อนหน้าว่า Tao ใช้ เครื่องมือโมเดลภาษาขนาดใหญ่ รวมถึง GPT-4 อย่างไรในการเดินทางครั้งนี้ อยู่ที่นี่: https://mathstodon.xyz/@tao/111233986893287137
สามารถติดตามความคืบหน้าของเขาได้บน GitHub เช่นกัน: https://github.com/teorth/symmetric_project/