数学の証明を自然言語で書かれた非形式的な形式から、Lean 4などの形式言語での形式的な証明に変換する「証明自動形式化」は、数学の形式化を加速させる重要な技術として注目されています。大規模言語モデル（LLM）を活用したこの分野の研究は急速に進展していますが、既存の評価方法には大きな課題がありました。 従来の研究では、キュレーションされたデータセットから抽出した整形式の非形式的証明を対象に評価が行われてきました。しかし現実の証明自動形式化システムには、より高い頑健性が求められます。本研究は、理想的な形式から外れた非形式的証明であっても、システムが正確性と忠実性を維持できるかどうかを検証する初めての包括的な研究です。 研究では2種類の摂動（変動）を定義して頑健性を評価しています。グローバル摂動は非形式的証明を異なるスタイルで言い換えるもので、この場合でも形式化が一貫性を保つべきとされます。一方、ローカル摂動は値、記号、または証明ステップを変更するもので、反事実的な変更を含む可能性があり、堅牢な形式化はシステムが独断的に推測するのではなく、摂動を忠実に反映すべきです。 miniF2FとMATH-500ベンチマークを用いた評価では、7つの最近のモデルすべてがグローバル摂動に対して敏感であり、ローカル摂動では忠実性を保つことに大きく失敗することが明らかになりました。この研究結果は、証明自動形式化の実用化に向けて改善すべき重要な課題を浮き彫りにしています。