[
    {
        "id": "osp-15566",
        "type": "article-journal",
        "title": "LeanPlan: التخطيط الأمثل بالاستدلالات المولّدة بالنماذج اللغوية الكبيرة وبراهين القبول",
        "author": [
            {
                "family": "Pereira",
                "given": "André G."
            },
            {
                "family": "Corrêa",
                "given": "Augusto B."
            },
            {
                "family": "Meneguzzi",
                "given": "Felipe"
            },
            {
                "family": "Seipp",
                "given": "Jendrik"
            }
        ],
        "URL": "https://omanscience.com/ar/articles/leanplan-optimal-planning-with-llm-generated-heuristics-and-admissibility-proofs",
        "language": "en",
        "issued": {
            "date-parts": [
                [
                    2026
                ]
            ]
        },
        "abstract": "يمكن لنماذج اللغة الكبيرة الرائدة أن تولّد دوال إرشادية توجّه البحث لتحقيق أداء متطور في التخطيط المُرضي، حيث يكون أي خطة مقبولة. لكن هذه الإرشادات لا يُضمن أن تكون مقبولة، وقد تؤدي إلى خطط دون المثالية. نقدم LeanPlan، وهو أول نظام تخطيط يجد خططاً مثالية بإرشادات مولّدة بـ LLM يُتحقق آلياً من قبولها. وبالنظر إلى وصف المجال ومهام التدريب، تستخدم حلقة وكيلية تغذية راجعة من المخطط لتحسين إرشاد قابل لإعادة الاستخدام خاص بالمجال تكرارياً، وإثبات قبوله، والافتراضات المطلوبة للمجال. وينفذ LeanPlan الإرشاد وإثباته ومخططاً فعّالاً، مع تأسيس وبحث مُتحقَّق آلياً في Lean 4. وعلى عشرة مجالات من المسابقة الدولية للتخطيط وثلاثة مجالات جديدة، نقيّم LeanPlan باستخدام مهام اختبار تصل إلى 57 ضعفاً من عدد الكائنات في مهام التدريب. ومع GPT-5.6 Sol في الحلقة الوكيلية، نجحنا في توليد الإرشادات وإثباتات القبول لجميع هذه المجالات. وباستخدام الإرشادات الناتجة، يوسّع LeanPlan عادة عدداً أقل من الحالات مقارنةً بالمخطط المتطور Scorpion، ويحل عدداً أكبر من المهام إجمالاً."
    }
]