本論文では，定理証明支援系Coqと大規模言語モデルを組み合わせた定理証明の自動化手法を提案する． まず，Coqのスクリプトとそれに対応するゴール，次に適用すべきtacticのデータセットを作成した． このデータセットで大規模言語モデルに追加学習を行い，学習したモデルを用いてCoqのtacticを生成し検証した． 本手法により，形式言語を使用した定理証明を目的とした大規模言語モデルへの追加学習が効果的であることを示した．