Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
يُعد Lean Refactor إطار عمل وكيلًا يعتمد على الاسترجاع المعزز، يعمل على تحسين براهين Lean لتحقيق أهداف متعددة — بما في ذلك ضغط الرموز (tokens)، وسرعة التجميع، وتوافق الإصدارات — من خلال الاختيار الديناميكي لاستراتيجيات إعادة الهيكلة المنسقة دون الحاجة إلى إعادة تدريب النموذج.