เกี่ยวกับ Theorem.chat
Theorem.chat ใช้คำอ้างทางคณิตศาสตร์ และพยายามที่จะตอบคำถามนี้ คุณจะต้องระบุคำอ้าง และมาตรฐานที่มันต้องตรงกับ กลุ่มของโมเดล AI - จำนวนเท่าที่คุณต้องการ จากผู้ผลิตที่คุณต้องการ - โจมตีมัน และอีกหนึ่งโมเดลที่ตัดสินใจ หลังจากนั้น ข้อโต้แย้งจะถูกทำเป็นรูปธรรมใน Lean 4 ต่อต้าน Mathlib และเคอร์เนล Lean จะตัดสินใจว่ามันถูกพิสูจน์หรือไม่ ขั้นสุดท้ายคือผลลัพธ์
ทำไมต้องเป็นเคอร์เนล ไม่ใช่โมเดลอื่น
ถามแบบจำลองคำถามที่ยาก และคุณจะได้รับคำตอบที่คล่องแคล่ว ว่ามันถูกต้องหรือไม่ ถามหลายครั้ง และพวกเขามักจะเห็นด้วย ซึ่งรู้สึกเหมือนการยืนยัน แต่มันไม่ใช่: แบบจำลองแบ่งปันข้อมูลการฝึกอบรม และแบ่งปันจุดบอด แบบจำลองที่สองที่ตรวจสอบแบบแรกยังคงเป็นประเภทเดียวกันของการตัดสินใจ และมันสามารถพูดคุยได้ เลนเคอร์เนลไม่สามารถทำได้ มันจะนำคำกล่าวมาจาก หลักการและ Mathlib หรือไม่ และความเชื่อมั่นจะไม่ส่งผลกระทบต่อผลลัพธ์
วิธีการที่ใช้กันทั่วไปในการหลอกลวงการพิสูจน์แบบรูปแบบจะถูกตรวจสอบและปฏิเสธ พิสูจน์ที่ทิ้งช่องว่างไว้กับ sorry, หนึ่งที่เรียกร้อง native_decide เพื่อทำให้เคอร์เนลใช้การคำนวณบนความเชื่อมั่น, หรือหนึ่งที่นำเสนอ axiom ใหม่อย่างเงียบ ๆ จะถูกตรวจพบและปฏิเสธแทนที่จะนับว่าเป็นความสำเร็จ
สิ่งที่แผงสามารถทำได้จริงๆ
การถกเถียงเป็นส่วนที่ถูกกว่า พาเนลทำงานกับเอกสาร - arXiv, OpenAlex, Crossref - ดังนั้นผลลัพธ์ที่รู้จักจะถูกอ้างอิง แทนที่จะนำมาใช้ใหม่ มันมี SageMath และ PARI/GP สำหรับคำนวณ Z3 และ CVC5 สำหรับ SMT แก้ไข OEIS หาเพื่อระบุลำดับที่มันสร้างขึ้น และสภาพแวดล้อม Sandbox Python ที่ไม่มีการเข้าถึงเครือข่าย ข้อเดาสามารถทดสอบได้กับกรณีหนึ่งหมื่นก่อนที่ใครจะใช้เวลาในการพยายามพิสูจน์มัน และตัวอย่างที่ตรงกันข้ามจะจบการสนทนาทันที
หลักฐาน ไม่ใช่คำพูด
match ไม่ได้ถูกจัดอันดับตามคุณภาพของอาร์กิวเมนต์ การอ้างอิงจะถูกแยกออกเป็นหลักการยอมรับ และหลักการจะถูกตัดสินเมื่อบางอย่างที่อยู่เบื้องหลังมันสามารถถูกตรวจสอบอีกครั้งโดยบุคคลที่สาม ได้แก่ แหล่งที่มาที่อ้างอิงข้อความที่เกี่ยวข้อง หรือโค้ดที่ถูกประมวลผลจริงๆ ด้วยผลลัพธ์จริงๆ ของมัน ผู้ตัดสินจะตรวจสอบหลักฐานนั้นอีกครั้งก่อนที่จะตัดสิน และมันจะไม่สามารถประกาศว่า match เสร็จสมบูรณ์ได้ ขณะที่หลักการยังเปิดอยู่
นายตั้งมาตรฐาน
คุณเลือกมาตรฐานได้ และผู้พิพากษาก็ถือมันอย่างจริงจัง ถามถึงสิ่งที่ผู้เชี่ยวชาญที่ระมัดระวังจะยอมรับ และคุณก็จะได้รับมัน ถามถึงข้อโต้แย้งที่สมบูรณ์แบบ กับทุกข้อสมมติฐานที่กล่าวไว้ และคุณก็จะถูกตัดสินโดยไม่คำนึงถึงมัน ถามถึงระดับที่รางวัลจะต้องเผชิญ และผลลัพธ์ที่ซื่อสัตย์ นั้นเป็นปกติจะเป็นรายงานที่ชัดเจน ว่าที่ไหนที่คณะกรรมการตกต่ำ มันมีค่ามากกว่าการอ้างอิงที่มั่นใจ สิ่งที่คุณต้องตรวจสอบด้วยตัวเอง
พูดให้ชัดเจนนะครับ นี่ไม่ใช่เครื่องที่แก้ไขปัญหาที่เปิดอยู่ มันเป็นเครื่องที่ปฏิเสธที่จะให้ข้อโต้แย้งผ่านไปได้ หากมันไม่ถูกแก้ไข และมันจะบอกคุณว่า ขั้นตอนไหนล้มเหลว
การทำแบบฟอร์มล้มเหลวคือผลลัพธ์ที่ใช้ได้
เมื่อ Lean ยังไม่ปิดการพิสูจน์ คุณจะได้รับเป้าหมายที่ถูกต้องที่เหลืออยู่ ในทางปฏิบัติ มันเป็นจุดที่การโต้แย้งแบบไม่เป็นทางการจะถูกสั่นมือ - ขั้นที่ทุกคนอ่านในเวอร์ชั่นของบทความจะต้องยกหัวให้ผ่านไป เป้าหมายนั้นจะถูกส่งไปยังที่นั่งที่เหมาะสมที่สุดในการโจมตีมัน, ร่วมกับสิ่งที่ได้พยายามแล้วและไม่มีอะไรอื่น โมเดลจะหยุดเมื่อมันติดขัด, แสดงตัวเองอีกครั้งด้วยค่าใช้จ่ายเต็ม; การผ่านคำถามเฉพาะหนึ่งแทนที่จะเปิดใช้งานโดยปกติแล้วจะเปิดใช้งานสำหรับส่วนหนึ่งของท็อคเก็ต
งานที่ยาวนานก็จะรอด
ทุกคำถามที่ตั้งขึ้น เข้าไปในบัญชีร่วมกัน กับหลักฐานของมัน ดังนั้นผลลัพธ์ถูกเขียนครั้งเดียว และไม่เคยนำมาใช้ใหม่ และจุดจบถูกบันทึก ดังนั้นไม่มีใครเดินกลับไปในพวกเขา Matches ทำงานด้านเซิร์ฟเวอร์ และหยุดชะงักอย่างสะอาด
นี่ไม่ใช่เพื่ออะไร
ธีมามคือคำที่ใช้ในการอธิบาย เว็บไซต์นี้ถูกสร้างขึ้นเพื่อคณิตศาสตร์ ตรรกะ คอมพิวเตอร์วิทยาศาสตร์ ทฤษฎี ฟิสิกส์ทฤษฎี และทฤษฎีเศรษฐกิจ - สาขาที่การอ้างอิงถูกพิสูจน์ คำถามเชิงประสบการณ์ในชีววิทยา แพทย์ เคมี หรือสังคมวิทยา ไม่ได้สร้างธีมาม แต่มันสร้างผลลัพธ์ และไม่มีการกำหนดรูปแบบที่จะตัดสินใจมัน เว็บไซต์พี่น้องของเรา referee.chat ใช้กระบวนการเดียวกันกับการตัดสินใจโดยไม่มีขั้นตอน Lean สำหรับคำถามเหล่านั้น