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

LLMを数式処理や形式証明へ応用する研究が進む一方，Lean形式証明生成では，正しい証明が複数のタクティク列で実現できるという性質がある．このとき実運用・大規模評価では，単に「正しいか（Leanが受理するか）」だけでなく，参照タクティク列（問題特化タクティク）を安定に生成・同定できるかが重要になる．例えば同じゴールを閉じても，探索的・冗長なタクティク列は実行時間やログ量を悪化させ得るため，参照タクティク列との文字列一致（canonical）により「狙ったタクティクが出ているか」を測りたい．しかしタクティク列には空白・改行・別名・括弧の有無など，同値だが異なる表記が複数存在し，生出力のままの文字列一致は表記差に敏感で，タクティク選択（同定）が破綻する．なお最終正否判定はLean機械検証で十分であるが，本稿の目的は「正しい証明の中から問題特化タクティクを同定・比較する」ことであり，そのためcanonicalを主要指標として扱う．そこで本研究では，Gate（出力制約）とstyle-canon（表記正規化）を前段に置き，最終判定をLean実行に統一する三段評価パイプラインにより，表記揺れ由来の偽陰性を縮減する（図1）．評価について,我々はformalbenchv0.4（以降，本ベンチ）[1]を作成し，本ベンチを用いてGPT-4o-miniとClaude3.5Sonnetの出力に対して，canonical採点とLean検証を同一条件下で比較した．また補助的に，ringnfの利用傾向など生成出力の軽量解析も行う．本稿の研究課題は，RQ1：出力制約が弱い条件でcanonicalに基づくタクティク同定がどの程度破綻し，どの表記要因（改行・空白・別名等）が主因となるかの把握，RQ2：Gateとstyle-canonによりcanonicalの一致率をどこまで回復でき，問題特化タクティクの選択（同定）と検証スループットをどこまで安定化できるかの検証，の2点である．