Leanstral 1.5: كيف يساعد AI في إثبات خصائص الشفرة؟

أطلقت Mistral في 2 يوليو 2026 نموذج Leanstral 1.5 المتخصص في هندسة البراهين باستخدام Lean 4، بترخيص Apache 2.0. تتناول هذه القراءة بتاريخ 5 يوليو ما يعنيه هذا الاتجاه للمطور، وكيف يختلف عن طلب شفرة تبدو صحيحة.

العثور على برهان وفحصه

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

للتوضيح، تخيل دالة تعالج قائمة من العناصر. سؤال «هل تعمل مع هذين المثالين؟» يختلف عن سؤال «هل تحافظ على عدد العناصر لكل مدخل يحقق الشروط المحددة؟». كلاهما مفيد، لكنهما لا يطلبان النوع نفسه من الأدلة.

والفرق عملي لفريق البرمجة: قبل اختيار الأداة، يحتاج إلى معرفة الادعاء الذي يريد فحصه. كلمة «صحيح» وحدها لا تحدد إن كان المقصود شكل المخرج أم محتواه أم خاصية أخرى.

ما دور النموذج وما دور Lean؟

تشرح وثائق Lean تمثيل القضايا والبراهين داخل الإطار نفسه، بحيث يجب أن ينسجم البرهان مع التعريفات والقواعد التي يستند إليها.

وتصف Mistral حلقة يقترح فيها النموذج برهانًا، ويتلقى ملاحظات المترجم، ثم يحاول تحسينه. هنا يؤدي الاقتراح والفحص وظيفتين منفصلتين: يبحث النموذج عن مسار، ويفحص النظام ما إذا كان المخرج يثبت القضية المكتوبة.

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

جودة المواصفات جزء من النتيجة

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

وللمطور المبتدئ، يمكن أن يبدأ التعلم بقاعدة صغيرة، ثم تدوين شروطها وفهم ما يقبله المدقق. بعد ذلك يصبح تقييم مساعدة AI أكثر وضوحًا: هل قربته من برهان للخاصية المطلوبة، أم غيّر السؤال إلى شيء أسهل؟

أهمية الاتجاه أنه ينقل نقاش الثقة إلى أسئلة قابلة للفحص: ما الذي طُلب؟ ما الذي أُثبت؟ وتحت أي افتراضات؟ هذه قراءة في الإعلان ومنهج العمل، وليست اختبارًا مستقلًا لأداء النموذج أو حكمًا على صحة أي مشروع كامل.