Lean 4 自動形式化における表面感度
arXiv cs.LG / 2026/4/28
💬 オピニオンIdeas & Deep AnalysisModels & Research
要点
- この論文は、Lean 4 自動形式化の出力がパラフレーズ（言い換え）によって変わるとき、それが本当の意味の不一致なのか、浅い失敗に起因するのかを調べます。
- ProofNet# と miniF2F のデータセットに対して 60 個の決定論的パラフレーズ規則を適用し、GPT 系列モデルとオープンウェイト 7B の複数自動形式化器で検証しています。
- 元の出力とパラフレーズ後の出力の両方がコンパイルに成功する場合、ペアの形式化は BEq+ の下で意味的に同等であり、さらに GTED では構造的にも非常に近いことが示されます。
- 一方で、パラフレーズは出力がコンパイルできるかどうかに大きく影響し、感度の主因が意味の分岐ではなく「コンパイル境界での失敗」であることが分かります。
- 著者らは、今後の学習介入やベンチマーク設計ではコンパイル境界の頑健性に焦点を当て、コンパイル条件付きの同等性と表面一貫性を分けて評価すべきだと提案しています。
