証明の自動形式化（proof autoformalization）とは、自然言語で書かれた非形式的な数学的証明を、Lean 4 のような形式言語による形式的証明へと翻訳することを目指す研究である。これまでに、大規模言語モデル（LLM）を用いた証明自動形式化モデルが複数開発されてきたが、既存の評価は主に、厳選されたデータセットに含まれる整形式の非形式的証明を翻訳する能力に焦点を当ててきた。2026年6月12日に投稿された本プレプリント論文は、堅牢な証明自動形式化器であれば、こうした理想化された証明から逸脱した非形式的証明に対しても忠実であり続けるべきだと主張し、証明自動形式化モデルの堅牢性に関する初の研究を提示している。
論文では、摂動を二つのカテゴリに定式化し、それぞれの下での堅牢性を評価している。第一の「大域的摂動」は、非形式的証明を異なる文体で言い換えるものであり、この場合、形式化の結果は一貫したものにとどまるべきである。第二の「局所的摂動」は、証明中の値、記号、または証明ステップを変更するもので、場合によっては反事実的な形で変更される。堅牢な形式化は、元の記述に戻ったり独自に別の解釈を推論したりするのではなく、その摂動を忠実に反映すべきである。
評価のために著者らは、miniF2F と MATH-500 の両方に対して二種類の摂動を含むベンチマークを構築し、大域的摂動の下で証明自動形式化の正しさがどれほど安定しているか、また局所的摂動の下でその出力が摂動をどれほど忠実に反映しているかを自動的に測定する手法を設計した。
続いて著者らは、最近の七つのモデルを評価した。その結果、すべてのモデルが大域的摂動に敏感であり、証明の文体が言い換えられると元の正しさを維持できなかった。また局所的摂動の下では、ほとんどのモデルが忠実性を保てず、変更された値、記号、証明ステップをそのまま反映できないことが示された。この結果は、現在の LLM ベースの証明自動形式化システムが、理想化されていない入力に対して依然として明確な弱点を抱えていることを示している。
論文のコードとデータは https://github.com/ucr-rai/robust-proof-autoformalization で公開されている。本論文はプレプリントであり、著者は Zhengtao Gui 氏ら三名である。投稿履歴によれば、v1 は 2026年6月12日 18:10:21 UTC に公開され、全文は約 246 KB、主題分類は計算と言語（cs.CL）で、人工知能（cs.AI）および機械学習（cs.LG）にも関連する。DOI は https://doi.org/10.48550/arXiv.2606.14867、arXiv 番号は arXiv:2606.14867v1 である。