Lean 4における証明自動形式化のロバスト性の評価

証明自動形式化は、自然言語で書かれた数学の非形式的な証明を、Lean 4などの形式言語で表現された形式証明に変換することを目的とする。近年、大規模言語モデル（LLM）に基づく自動形式化手法が開発されてきたが、既存の評価は主に厳選されたデータセットの整った非形式証明に焦点を当ててきた。しかし、現実の非形式証明は、異なる表現スタイルや誤りを含むなど、これらの理想的なものから逸脱する可能性がある。そこで、カリフォルニア大学リバーサイド校の研究者たちは、証明自動形式化モデルのロバスト性に関する初の組織的な研究を実施した。

研究者は2種類の摂動を定式化した。グローバル摂動は非形式証明を異なるスタイルで言い換えるもので、形式化は一貫しているべきである。ローカル摂動は値、記号、証明ステップを変更するもので（反事実的な場合もある）、堅牢な形式化は摂動を忠実に反映すべきであり、元に戻したり独自に推論したりしてはならない。miniF2FおよびMATH-500データセットに両方の摂動を含むベンチマークを構築し、グローバル摂動下での正しさの安定性とローカル摂動下での出力の忠実性を自動測定した。

評価された7つの最近のモデル（GPT-4o、Claude 3.5など）はすべて、グローバル摂動に敏感であり、証明の表現スタイルを変えると形式化の正解率が顕著に低下した。ローカル摂動に対しては、ほとんどのモデルが忠実性を維持できず、変更された値やステップを無視して元の証明に一致する形式化を出力する傾向があった。これは、現在の自動形式化モデルが非理想的な入力に対して脆弱であることを示している。

この研究は、現在の自動形式化モデルの脆弱性を明らかにし、公開されたコードとデータは今後の改善のための基礎を提供する。研究者は、この研究を通じて、数学的証明の自動検証を支援する、より堅牢な自動形式化システムの開発を促進したいと考えている。