出力制約と表記正規化によるLLM 形式証明のタクティク選択評価
LLM による Lean 形式証明生成では，最終正否判定は Lean の機械検証で定まる． しかし実用上は，\emph{正しい証明の中から「参照タクティク列（問題特化タクティク）を同定できるか」}が重要であり， この同定には参照タクティク列との文字列一致（canonical）が有用な指標となる． 一方で生出力には，説明文・コードフェンス・改行・別名などの表記揺れが混入しやすく， 「実際には同等のタクティク列」であっても文字列一致が崩れて，タクティク選択が不安定になる． 本稿はこの課題に対し，出力制約（Gate）と表記正規化（style-canon）によりタクティク列を安定な正規形へ写像し， canonical に基づくタクティク選択を頑健化する三段評価パイプラインを提案する． また評価データとしてformal\_bench v0.4を作成した．実験を行った結果， 出力制約が弱い条件では Lean 成功率が 1.00 でも canonical がほぼ 0 となり選択が破綻し得る一方， 提案パイプラインにより canonical の一致率が回復し，問題特化タクティクの同定と比較が安定することを示す．
Mar 5, 2026