DeepSeek เปิดตัว Prover-V2 โมเดลพิสูจน์ทฤษฎีบทคณิตศาสตร์ 671B พารามิเตอร์

เมื่อวันที่ 30 เมษายน พ.ศ. 2568 DeepSeek ได้เปิดตัว DeepSeek-Prover-V2-671B โมเดล AI ที่ออกแบบมาเฉพาะสำหรับการพิสูจน์ทฤษฎีบททางคณิตศาสตร์ โมเดลนี้สร้างขึ้นบนสถาปัตยกรรม Mixture-of-Experts (MoE) ขนาด 671B พารามิเตอร์ ซึ่งเป็นฐานเดียวกับที่ขับเคลื่อน DeepSeek-V3 แต่มุ่งเน้นงานเฉพาะทางคือการสร้างและตรวจสอบการพิสูจน์เชิงรูปนัย (formal proof) ภายในเฟรมเวิร์ก Lean 4 ข้อมูลอย่างเป็นทางการระบุว่าโมเดลนี้ทำอัตราผ่านการทดสอบบนชุด MiniF2F-test ได้ถึง 88.9% และสามารถแก้โจทย์จากคลังข้อสอบ PutnamBench (โจทย์การแข่งขันคณิตศาสตร์ระดับมหาวิทยาลัย Putnam ของสหรัฐฯ) ได้ 49 ข้อ จากทั้งหมด 658 ข้อ โมเดลนี้เปิดให้ดาวน์โหลดแบบโอเพนซอร์สบน Hugging Face พร้อมสัญญาอนุญาตที่ให้ใช้งานเชิงพาณิชย์ได้

ความหมายเชิงเทคนิค: สถาปัตยกรรม MoE ช่วยลดต้นทุนการประมวลผล

แม้จำนวนพารามิเตอร์รวมจะสูงถึง 671B แต่ด้วยการออกแบบแบบ MoE ทำให้ในแต่ละครั้งที่สร้างหนึ่งโทเคน มีเพียงประมาณ 37 พันล้านพารามิเตอร์เท่านั้นที่ถูกเรียกใช้งานจริง ส่วนที่เหลือจะอยู่ในสถานะพัก กลไก “ปลุกใช้ตามความจำเป็น” นี้ทำให้ DeepSeek รักษาความจุความรู้ขนาดใหญ่ไว้ได้ พร้อมควบคุมต้นทุนการประมวลผลต่อการอนุมานหนึ่งครั้งให้อยู่ในระดับใกล้เคียงโมเดลขนาดกลาง สำหรับงานพิสูจน์เชิงรูปนัยที่ต้องลองผิดลองถูกและย้อนกลับซ้ำ ๆ ประสิทธิภาพการอนุมานจึงเป็นตัวกำหนดโดยตรงว่าโมเดลจะสำรวจเส้นทางการพิสูจน์ได้มากเพียงใดในเวลาที่จำกัด นี่คือปัจจัยที่ทำให้ Prover-V2 กล้าท้าทายโจทย์ระดับ Putnam

เทียบกับโมเดลรุ่นก่อนและคู่แข่งในสายเดียวกัน

การพิสูจน์ทฤษฎีบทเชิงรูปนัยเป็นสาขาการประยุกต์ใช้ AI ที่ค่อนข้างเฉพาะทางแต่มีความท้าทายทางเทคนิคสูง ก่อนหน้านี้ความก้าวหน้าในสาขานี้ส่วนใหญ่กระจุกตัวอยู่ในห้องแล็บชั้นนำเพียงไม่กี่แห่ง การที่ DeepSeek เลือกเปิด Prover-V2 แบบโอเพนซอร์สและอนุญาตให้ใช้เชิงพาณิชย์ได้ เท่ากับเป็นการนำความสามารถที่เคยกระจุกตัวมาเปิดให้นักวิจัยและองค์กรทั่วโลกเข้าถึงได้ในต้นทุนต่ำ สอดคล้องกับกลยุทธ์ที่ DeepSeek ยึดถือมาตั้งแต่ยุค R1 คือใช้โมเดลโอเพนซอร์สแย่งชิงอำนาจนำในสาขาเทคนิคเฉพาะทาง แทนที่จะแข่งขันเฉพาะในสนามแชทบอทเอนกประสงค์

ปฏิกิริยาในวงการ: แรงกดดันจากกลยุทธ์โอเพนซอร์สที่ต่อเนื่อง

จังหวะเวลาการเปิดตัว Prover-V2 อยู่ก่อนที่ DeepSeek จะเตรียมเปิดตัวโมเดลเรือธงรุ่นถัดไปอย่าง “R2” จึงถูกมองว่าเป็นการอุ่นเครื่องแสดงศักยภาพทางเทคนิค สำหรับผู้ผลิต AI รายอื่น การที่ DeepSeek เปิดโมเดลระดับสูงแบบโอเพนซอร์สและใช้เชิงพาณิชย์ได้ฟรีซ้ำแล้วซ้ำเล่า กำลังบีบพื้นที่การตั้งราคาและความแตกต่างของค่ายโมเดลปิด และทำให้ “ความสามารถด้านการให้เหตุผลทางคณิตศาสตร์” กลายเป็นสมรภูมิใหม่ที่ฝั่งโอเพนซอร์สกำลังไล่ตามอย่างรวดเร็ว ต่อจากสมรภูมิการเขียนโค้ด

ความหมายสำหรับผู้บริหาร

Prover-V2 เป็นเครื่องมือเชิงวิชาการสูง ผู้บริหารส่วนใหญ่คงไม่ได้ใช้งานโดยตรง แต่แนวโน้มที่สะท้อนออกมานั้นน่าจับตา นั่นคือ AI กำลังก้าวหน้าอย่างรวดเร็วในงานที่ต้องการตรรกะเข้มงวดและตรวจสอบความถูกต้องได้ ในอนาคตงานบริหารที่เน้น “ความผิดพลาดเป็นศูนย์” เช่น การตรวจสอบโมเดลการเงิน การตรวจความสอดคล้องของเงื่อนไขสัญญา หรือการคำนวณตรวจสอบสเปกทางวิศวกรรม อาจมีเครื่องมือ AI ลักษณะเดียวกันมาช่วยงาน จึงควรติดตามว่าเทคโนโลยีสายนี้จะเข้าสู่การใช้งานจริงในองค์กรเมื่อใด