تواجه النماذج اللغوية الكبيرة (LLMs) القائمة على اللغة غير الرسمية (مثل لغة الإنسان) التي تم تدريبها باستخدام التعلم بالتعزيز (RL) تحديًا كبيرًا: فإن عمليات التحقق منها، التي توفر إشارات تدريبية حاسمة، ليست موثوقة ولا قابلة للتوسيع. في الواقع، لا يمكن للنماذج الكبيرة الخاصة الشائعة إنتاج برامج قابلة للتحقق. هناك بديل واعد، لكنه ما زال غير مكتشف جيدًا، وهو الاستدلال القائم على اللغة الرسمية. من خلال تأسيس LLMs في أنظمة رسمية صارمة حيث تعمل نماذج التوليد في مساحات لغوية رسمية (مثل Dafny)، يمكن تحقق الاستدلال والنتائج بشكل تلقائي وقابل للبرهنة رياضيًا. هذه القدرة تُعد أساسية لتحقيق التحقق الرسمي الواسع النطاق والموثوق من البرمجيات. من الشائع استخدام سلسلة الأفكار المُعلمة من قبل الإنسان والبديهيات البشرية الأخرى لتعزيز قدرات الاستدلال والبرمجة لدى LLMs. ولكن للأسف، أصبح تقديم هذه البديهيات أمرًا مكلفًا للغاية ومُرهقًا للقيام به في المهام البرمجية المعقدة. في هذه الدراسة، نستكشف بشكل منهجي طرق تقليل البديهيات البشرية باستخدام اللغة الرسمية Dafny كبيئة رئيسية لتجاربنا الأولية. يعتمد نظامنا بشكل رئيسي على إدخال نظام تجميع بيانات تلقائي وقابل للتوسيع، وتصميمات مُتقنة لتعلم التعزيز (RL) مدمجة مع ملاحظات من مُحقق اللغة الرسمية. نقدم DafnyComp، وهو معيار للبرامج الرسمية المركبة مع وصفات تلقائية التحويل للوصف (auto-formalized specifications) لاستخدامها في الاستدلال حول الوصف. يسمح مرحلة التدقيق المُشرف (SFT) للنماذج الصغيرة (مثل 0.5B) بإنتاج كود Dafny مُصحح بناءً على القواعد وقابل للتحقق، وتتفوق على النماذج الخاصة. كما أن تعلم التعزيز مع التقوية (regularization) يحسن الأداء بشكل أكبر، ويحقق تعميمًا أقوى للمهام خارج المجال، ويتفوق على جميع النماذج الأساسية القوية في معيار DafnyComp الصعب.