出力制約と表記正規化によるLLM形式証明のタクティク選択評価

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点である．