講演情報
[4Yin-A-45]大規模言語モデルを用いた行間を埋める自動証明
〇潘 俊洋1、松崎 拓也1 (1. 東京理科大学)
キーワード：
形式証明、大規模言語モデル、形式スケッチ、行間補完、証明支援系（Lean）
豊富な自然言語による数学証明を自動形式化に活用するため，Jiang ら（2023）は Draft, Sketch, and Prove（DSP）という枠組みを提案した．DSP は自然言語による証明から，証明の一部が未記述のまま残る部分的な形式証明（形式スケッチ）を生成し，形式スケッチ中の未完成部分を補完することで形式証明を完成させる手法である．Jiang らは形式スケッチの補完のために，手設計の戦略集合や外部証明補助ツールを組み合わせた探索を用いていた．本研究では，既存の自動形式証明モデルを用いて，形式スケッチの行間（未証明の部分）を自動補完するタスクに取り組む．具体的には，完全な形式証明のうち中間命題の証明部分を <proof> マークでマスクし，形式スケッチとマスクした証明断片（補完片）を，元の証明へ復元可能な形で抽出して，教師付き学習データを構築した．そして，DeepSeek-Prover-V2-7B を QLoRA で微調整し，形式スケッチを入力として補完片のみを出力するように学習した．MiniF2F と FormalMATH から構成したテストデータで評価した結果，pass@32 = 95.08% を達成した．