評估Lean 4中證明自動形式化的魯棒性
本文首次系統研究證明自動形式化模型在Lean 4中的魯棒性。提出了全域性擾動（改寫風格）和區域性擾動（修改值、符號或步驟）來測試模型的忠信度，發現所有七個評估模型均對全域性擾動敏感，且多數無法忠實反映區域性擾動。
證明自動形式化旨在將自然語言撰寫的非正式數學證明轉化為Lean 4等正式語言中的形式證明。近年來，基於大型語言模型（LLM）的自動形式化方法取得了顯著進展，但現有評估通常僅關注從精選資料集中選取的、結構良好的非正式證明。然而，現實場景中的非正式證明可能偏離這些理想情況，例如使用不同的表述風格或包含錯誤。為此，來自加州大學河濱分校的研究人員首次系統研究了證明自動形式化模型的魯棒性。
研究者提出了兩類擾動來模擬現實中的變體。第一類是全域性擾動，即用不同風格改寫非正式證明，此時形式化結果應保持一致。第二類是區域性擾動，即修改證明中的某個值、符號或步驟，甚至可以是反事實的修改；魯棒的模型應忠實反映這一變化，而非自動糾回原樣或自行推斷。他們基於miniF2F和MATH-500資料集構建了包含兩類擾動的基準測試，並自動評估了模型在全域性擾動下正確性的穩定性以及區域性擾動下輸出的忠實性。
實驗評估了七個近期模型，包括GPT-4o、Claude 3.5等。結果顯示所有模型均對全域性擾動敏感，即改變證明的表述風格後，形式化結果的正確率明顯下降。在區域性擾動下，大多數模型無法保持忠實，它們常常忽略修改後的值或步驟，而輸出與原始證明一致的形式化結果。這表明當前自動形式化模型在應對非理想輸入時存在顯著脆弱性。
該研究揭示了當前自動形式化模型的脆弱性，並提供了公開程式碼與資料，為後續改進提供了方向。研究者希望透過這項工作，推動開發更魯棒的自動形式化系統，以支援數學證明的自動化驗證。