في عالم أنظمة التفكير الرسمي، يُعتبر الوصول إلى أداء على مستوى المسابقة الدولية غير مسبوق. ومع ذلك، لا يزال هناك تفتت في المشهد الحالي، حيث يتم التعامل مع الجبر ونظرية الأعداد في إطار Lean، في حين أن الهندسة تعتمد على لغات محددة النطاق تقدم ضمانات رسمية محدودة. هذا الانقسام يزيد من قاعدة الحوسبة الموثوقة ويعيق تطوير نموذج موحد.

لا توجد حلول في Lean لتحديات الهندسة، حيث تقدم الجهود الحالية مثل LeanEuclid وLeanGeo أنظمة بديهيات مخصصة غير متوافقة مع Mathlib القياسي، مما يحد من إمكانية التدريب على نطاق واسع. ومع ذلك، فإن التلقائية في الشكل الهندسي تطرح تحديات فريدة، مثل ضرورة جعل الافتراضات الضمنية صريحة بدلاً من تركها للحلول الخارجية، ويجب أن تتكيف النماذج مع البنية التحتية الصغيرة والمتطورة بسرعة للهندسة في Mathlib.

هنا تأتي Euclean، وهو إطار عمل رباعي المراحل لتنفيذ الشكل الهندسي تلقائيًا. يتضمن الإطار: توضيح القيود، تثبيت التكوين، رسم خارطة التشكيل، والإصلاح التكراري. تم بناء مجموعتين من البيانات العملاقة: OMNI-Geometry التي تحتوي على 768 مشكلة تنافسية وNumina-Geometry التي تحتوي على 177,597 مشكلة. هذه هي أكبر مجموعة بيانات للتشكيل الهندسي في Lean.

أظهرت التقييمات البشرية دقة تصل إلى 48.89% في TOP1 و73.33% في TOP5. كما عزز تدريب نموذج Goedel v2 باستخدام تشكيلاتنا جودة البرهان، حيث زادت نسبة النجاح من 13.6% إلى 15.1%. وهذا يؤكد جودة مجموعة البيانات لتقديم البرهنات الذكية الموحدة.

للاستزادة، يمكنكم زيارة المستودع الخاص بالمشروع!

ما هو رأيكم في هذه الخطوات الثورية نحو توحيد معالجة الهندسة في الأنظمة الذكية؟ شاركونا آرائكم في التعليقات.