كل المقالات
GenLimitLib يختبر مكتبات Lean قابلة لإعادة الاستخدام في الرياضيات بالذكاء الاصطناعي
تستكشف ورقة أولية بتاريخ 29 سبتمبر كيف تساعد الرياضيات الصورية المنظمة الذكاء الاصطناعي في بناء براهين متحقق منها.
إعادة استخدام المعرفة الرياضية
يقدم شوانغبينغ لي وبنغ تشانغ مكتبة GenLimitLib بلغة Lean، لتنظيم نتائج من 30 ورقة حول توليد سلاسل جديدة صحيحة انطلاقاً من أمثلة.
وتورد ورقتهما الأولية المنشورة في 29 سبتمبر نجاح 79 محاولة برهان من أصل 100 عند إتاحة مكتبة بحثية فرعية، مقابل 48 باستخدام تعريفات أساسية. وتلقت الحالتان الأوراق نفسها وعبارات مبرهنات ثابتة.
يشمل التقييم خمس مهام برهنة في مجال متخصص، ولا يمثل الرياضيات عموماً. وتشير النتائج إلى فائدة المعرفة الصورية القابلة لإعادة الاستخدام في بناء براهين بالذكاء الاصطناعي. ما زال العمل أولياً، ولم تُعِد MathsAI التجارب.