الملخص
تمت ترجمة أجزاء من هذه الصفحة آلياً وقد تحتوي على أخطاء.
يتزايد اعتماد وكلاء البرمجة في أتمتة تطوير براهين Lean، لكن نجاح التجميع وحده لا يثبت أن المرشح يبرهن العبارة المقصودة تحت افتراضات مقبولة. نقدم FORALL-LEAN-AGENT، وهو إطار مستقل عن الواجهة للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات. يجمع الإطار بين مساحات عمل معزولة، وأدوات Lean، ومراجعة جديدة مع مقارنة العبارات، وتدقيقات للمسلمات، وتحقق مستقل من البراهين حيثما كان مدعومًا. وتُربط أدلة التحقق وقرارات المراجعين بالأثر المرشح نفسه، فيصبح القبول قابلًا للتتبع. ونقيّم الإطار على VeriSoftBench وPutnamBench وكلتا المسألتين في مسار التحقق من البرمجيات في Lean Eval. وعلى المجموعة الفرعية من 100 مهمة في VeriSoftBench، يرفع دمج FORALL-LEAN-AGENT نجاح قواعد المعيار لـ GPT-5.6 Sol عند الجهد المنخفض من 93 إلى 100، مع خفض الكلفة من 69 دولارًا إلى 62 دولارًا. ويقبل تقييم PutnamBench جميع المسائل الـ672 بمتوسط 4.72 دولار لكل مسألة. وتبين هذه النتائج أن تصميم حزمة الوكيل يمكن أن يحسّن الصحة والكفاءة، مع توفير أدلة تتجاوز عدد الحلول الإجمالي.
الكلمات المفتاحية
الموضوع
بيانات النشر
- المجلة
- غير متاح
- وصول مفتوح
- وصول مفتوح أخضر
اقتبس هذه المقالة
APA 7
Lwin, N. O. (2026). FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات. https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification
MLA 9
Lwin, Naing Oo. "FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات." https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
شيكاغو (المؤلف–التاريخ)
Lwin, Naing Oo. 2026. "FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات." https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
هارفارد
Lwin, N. O. (2026) 'FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات', Available at: https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
فانكوفر
Lwin NO. FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات. https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification
IEEE
N. O. Lwin, "FORALL-LEAN-AGENT: للاستدلال القابل للتدقيق في الرياضيات الصورية والتحقق من البرمجيات," https://omanscience.com/ar/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.