本記事では、構造から実体への定理自動形式化（SITA）という新しいフレームワークを提案します。大規模言語モデル（LLM）が数学的推論において進展を見せている一方で、抽象的な構造を具体的な設定に適用する際の定理形式化には課題が残ります。SITAは、抽象的な数学理論とその具体的な応用との間のギャップを埋めることを目指しており、形式化された抽象構造をモジュールテンプレートとして扱い、これを用いて具体的なインスタンスの形式化を行います。具体的なインスタンスが与えられると、それに対応するLeanの定義や宣言を生成し、Leanの型クラスメカニズムを用いて統合し、構造的仮定をチェックすることで証明された定理を構築します。また、LLMに基づく生成とフィードバックを使用した洗練によって、自動化と形式的正確性の両立を図っています。最適化問題のデータセットに対する実験により、SITAが抽象構造に基づく多様なインスタンスの形式化に効果的であることが示されました。