LeanGraphSearch يستخدم تبعيات المكتبة لتوجيه البحث الآلي عن البراهين
تختبر ورقة أولية في أكتوبر ما إذا كان تتبع رسم تبعيات Mathlib يساعد نظام برهنة بالذكاء الاصطناعي في العثور على اللمّات المساندة التي يحتاجها.
البحث داخل بنية مكتبة صورية
يستطيع مساعد البرهان الصوري التحقق من برهان مكتمل، لكن نظام الذكاء الاصطناعي يحتاج أولاً إلى العثور على التعريفات واللمّات التي تجعل البرهان ممكناً. تقدم ورقة أولية أُرسلت في 15 أكتوبر نظام LeanGraphSearch، وهو أسلوب استرجاع يستخدم بنية التبعيات في مكتبة الرياضيات Lean 4 المسماة Mathlib لتوسيع قائمة الحقائق المعروضة على نموذج يولد البراهين.
من تشابه الكلمات إلى المتطلبات المساندة
يبدأ الأسلوب ببحث دلالي معتاد يسترجع التصريحات التي تشبه عباراتها المبرهنة المستهدفة أو حالة البرهان. ثم يتبع الروابط الموجهة من تلك التصريحات إلى الحقائق السابقة التي تعتمد عليها، مستخدماً درجة على نمط PageRank مخصصة للاستعلام. وتقارن مرحلة إعادة ترتيب ثانية المرشحين الموسعين بالاستعلام الأصلي. والهدف هو العثور على متطلبات مفيدة حتى عندما تختلف صياغتها عن المسألة التي يحاول النموذج برهنتها.
يقيم المؤلفون النهج على معيارين للاسترجاع وثلاثة معايير لبرهنة مبرهنات في Lean. ويوردون قيمة Recall@100 أعلى من LeanSearch v2 في مجموعة فرعية مختارة من MathlibQR، ومعدلات إكمال براهين أفضل من النظام الأساسي عند عدة ميزانيات للتأمل. أما المكاسب التي يوردونها مقابل LeanSearch v2 فهي أصغر. وتجمع الورقة أيضاً الاسترجاع مع ملاحظات مترجم Lean وسجل محلي للمحاولات الفاشلة السابقة.
أداة لسير عمل البرهان الصوري لا مبرهنة جديدة
يتعلق هذا العمل بالبنية المحيطة بالرياضيات الصورية: كيف يسترجع نظام ذكاء اصطناعي معرفة موجودة قابلة للقراءة آلياً قبل كتابة البرهان. يستطيع مدقق Lean التحقق من نص برهان صوري مكتمل، لكن تحسن نتائج المعايير لا يثبت وحده قدرة النظام على حل مسائل بحثية مفتوحة باستقلال. وتعكس النتائج تقارير المؤلفين عن مجموعات البيانات والنماذج والميزانيات وخطوط الأساس التي اختاروها. هذه ورقة أولية غير محكمة، ولم يُعِد MathsAI إجراء التجارب.