ภาษาการใช้เหตุผลเชิงรูปแบบใหม่ที่เรียกว่า Litex ได้เกิดขึ้น โดยสัญญาว่าจะปฏิวัติวิธีที่ผู้คนเข้าถึงการพิสูจน์ทางคณิตศาสตร์และการใช้เหตุผลเชิงตรรกะ โครงการโอเพนซอร์สนี้อ้างว่าเป็นภาษาเชิงรูปแบบแรกที่ใครก็สามารถเรียนรู้ได้ในเวลาเพียง 1-2 ชั่วโมง แม้จะไม่มีประสบการณ์ด้านคณิตศาสตร์หรือการเขียนโปรแกรม อย่างไรก็ตาม ชุมชนเทคโนโลยีกำลังตั้งคำถามอย่างจริงจังต่อการอ้างที่ทะเยอทะยานเหล่านี้
การอ้างเรื่องความเรียบง่ายเจอกับการตรวจสอบความเป็นจริง
Litex วางตำแหน่งตัวเองว่าเรียบง่ายกว่าภาษาเชิงรูปแบบที่มีอยู่แล้วอย่าง Lean 4 อย่างมาก ผู้สร้างแสดงการเปรียบเทียบแบบเคียงข้างกัน ซึ่งการแก้ระบบสมการหลายตัวแปรดูเหมือนจะตรงไปตรงมากว่าใน syntax ของ Litex พวกเขาอ้างว่านี่แสดงถึงการลดอุปสรรคการเรียนรู้และต้นทุนการสร้างการพิสูจน์ลง 10 เท่า
การตอบสนองของชุมชนค่อนข้างผสมผสาน ผู้ใช้หลายคนกำลังดิ้นรนกับปัญหาเอกสารพื้นฐานและคำอธิบายที่ไม่ชัดเจนของแนวคิดหลัก ชีทสรุปของภาษานี้มีคำอธิบายที่สับสน และแม้แต่ความแตกต่างพื้นฐานระหว่างคำสั่งอย่าง have, let, และ know ก็ไม่ได้อธิบายอย่างชัดเจน ผู้แสดงความคิดเห็นคนหนึ่งสังเกตว่าการเรียนรู้ความแตกต่างเหล่านี้ให้เชี่ยวชาญเพียงอย่างเดียวก็ต้องใช้เวลามาก ซึ่งขัดแย้งกับการอ้างว่าเรียนรู้ได้ใน 1-2 ชั่วโมง
การเปรียบเทียบ Litex กับ Lean 4
- Litex: อ้างว่ามีไวยากรณ์ที่เหมือนภาษาธรรมชาติ ใช้เวลาเรียนรู้ 1-2 ชั่วโมง ไม่จำเป็นต้องมีพื้นฐานการเขียนโปรแกรม
- Lean 4: เป็นภาษาทางการที่มีชื่อเสียงซึ่งมีพื้นฐานจากทฤษฎีประเภท ต้องการความเชี่ยวชาญอย่างมาก มีการสนับสนุนไลบรารีทางคณิตศาสตร์อย่างครอบคลุม
- ความยาวของโค้ด: ตัวอย่าง Litex แสดงประมาณ 10 บรรทัด เทียบกับ Lean 4 ที่ใช้ประมาณ 25 บรรทัดสำหรับการพิสูจน์เดียวกัน
- เส้นโค้งการเรียนรู้: Litex อ้างว่าใช้เวลา 1-2 ชั่วโมง เทียบกับ Lean 4 ที่ต้องใช้เวลาหลายเดือนหรือหลายปีในการศึกษา
รากฐานทางเทคนิคยังคงไม่ชัดเจน
ข้อกังวลหลักที่ชุมชนยกขึ้นมาเน้นไปที่รากฐานทางคณิตศาสตร์พื้นฐานของ Litex ไม่เหมือนกับภาษาเชิงรูปแบบที่มีอยู่แล้วซึ่งระบุฐานทฤษฎีอย่างชัดเจน เอกสารของ Litex ล้มเหลวในการอธิบายว่าใช้ระบบคณิตศาสตร์แบบไหน หรือสามารถจัดการกับการพิสูจน์ประเภทใดได้บ้าง ผู้ใช้กำลังถามคำถามพื้นฐานเกี่ยวกับความหมายและการแสดงการพิสูจน์ที่ยังไม่ได้รับคำตอบ
โครงการอ้างว่ามีความแม่นยำ 100% บนชุดข้อมูล GSM8K โดยไม่ต้องฝึก แต่ให้รายละเอียดเพียงเล็กน้อยเกี่ยวกับวิธีการบรรลุหรือตรวจสอบสิ่งนี้ การขาดความโปร่งใสทางเทคนิคนี้ทำให้ผู้เชี่ยวชาญสงสัยเกี่ยวกับความสามารถและความน่าเชื่อถือที่แท้จริงของภาษานี้
สถานะโครงการและทรัพยากร
- เวอร์ชัน: v0.1.10-beta (ยังไม่พร้อมใช้งานจริง)
- ลิขสิทธิ์: โอเพนซอร์ส
- คุณสมบัติหลัก: การรวม Python ( pylitex ), แพลตฟอร์มการเรียนรู้ออนไลน์, ไลบรารีมาตรฐานอยู่ระหว่างการพัฒนา
- ชุมชน: แชท Zulip , ที่เก็บข้อมูล GitHub , ชุดข้อมูล Hugging Face
- การอ้างสิทธิ์: ความแม่นยำ 100% ในชุดข้อมูล GSM8K , ลดอุปสรรคการเรียนรู้และต้นทุนการสร้างการพิสูจน์ลง 10 เท่า
ช่องว่างระหว่างการตลาดกับความเป็นจริง
บางทีแง่มุมที่ถกเถียงกันมากที่สุดคือแนวทางการตลาดของ Litex การอ้างว่าแม้แต่เด็กก็สามารถทำสมการหลายตัวแปรให้เป็นรูปแบบเชิงรูปแบบได้ใน 2 นาทีได้รับการวิพากษ์วิจารณ์เป็นพิเศษ สมาชิกชุมชนชี้ให้เห็นว่าเด็กโดยทั่วไปไม่เข้าใจสมการหลายตัวแปรตั้งแต่แรก ทำให้การอ้างนี้ไร้ความหมาย
การอ้างว่า LLM มีความฉลาดนั้นชัดเจนในตัวเองจนการปฏิเสธแนวคิดนี้ต้องการหลักฐาน? นั่นกลับหัวกลับหาง!
การเปรียบเทียบกับ Lean 4 ก็ถูกท้าทายเช่นกัน ในขณะที่ Litex แสดงการพิสูจน์ Lean 4 ที่ซับซ้อนซึ่งใช้เวลาหลายชั่วโมงของงานผู้เชี่ยวชาญ ผู้ใช้ที่มีประสบการณ์โต้แย้งว่านักพัฒนา Lean 4 ที่มีความสามารถสามารถแก้ปัญหาเดียวกันได้ในไม่กี่นาที ไม่ใช่หลายชั่วโมง
ข้อกังวลของชุมชนเกี่ยวกับความแท้จริง
สมาชิกชุมชนบางคนได้ตั้งคำถามเกี่ยวกับความแท้จริงของโครงการ โดยมีข้อเสนอแนะว่าส่วนหนึ่งของเอกสารอาจถูกสร้างขึ้นโดยเครื่องมือ AI สไตล์การเขียนที่มีการอ้างซ้ำๆ และภาษาการตลาด ได้กระตุ้นความสงสัยเกี่ยวกับว่านี่แสดงถึงนวัตกรรมทางเทคนิคที่แท้จริงหรือเป็นเนื้อหาเชิงส่งเสริมการขายเป็นหลัก
โครงการมีองค์ประกอบทางเทคนิคที่ถูกต้องบางอย่าง รวมถึงที่เก็บ GitHub และเครื่องมือพื้นฐาน อย่างไรก็ตาม ช่องว่างระหว่างการอ้างทางการตลาดและความสามารถที่แสดงให้เห็นยังคงเป็นเชื้อเพลิงให้ความสงสัยของชุมชนเกี่ยวกับศักยภาพที่แท้จริงของ Litex ในพื้นที่การใช้เหตุผลเชิงรูปแบบ