既存の非形式的な言語に基づく（例えば、人間の言語）大規模言語モデル（LLM）は、重要な訓練信号を提供する検証プロセスが信頼性もスケーラビリティも欠如しているという大きな課題に直面しています。実際、一般的な大規模な特許付きモデルでは、検証可能なプログラムを生成することが困難です。形式的な言語に基づく推論が有望な代替手段である一方で、その研究はまだほとんど進んでいません。LLMを厳密な形式的システムに根ざさせ、生成モデルを形式的言語空間（例えば、Dafny）で動作させる方法により、推論プロセスおよび結果の自動的かつ数学的に証明可能な検証が可能になります。この能力は、大規模で信頼性の高い形式的ソフトウェア検証を実現するために不可欠です。通常、人間がアノテートした思考の連鎖やその他の人間の事前知識を用いて、LLMの推論およびコード生成能力を誘導することが行われます。しかし、複雑なプログラミングタスクを監督するためにこのような事前知識を提供することは、実際上、受け入れがたいほどに手間がかかります。本研究では、形式的言語Dafnyを主な環境として、パイロット研究の枠組みの中で人間の事前知識を削減する方法を体系的に探求します。我々のパイプラインは、自動的でスケーラブルなデータ整理プロセスを導入し、形式的言語検証器からのフィードバックを組み込んだ慎重な強化学習（RL）の設計に依存しています。また、我々は、自動的に形式化された仕様を備えた合成的な形式的プログラムのベンチマークであるDafnyCompを導入しました。このSFT（Supervised Fine-Tuning）段階により、たとえば0.5Bの小規模モデルでも、構文的に正しいかつ検証可能なDafnyコードを生成することが可能となり、特許付きモデルを上回ります。正則化付きの強化学習により、性能がさらに向上し、ドメイン外のタスクへの汎化能力が強化され、DafnyCompベンチマークにおいてすべての強力なベースラインを上回る結果を得ました。