用於自動定理證明的生成式語言建模

OpenAI 開發了 GPT-f，這是一個基於 transformer 的語言模型，專為自動定理證明而設計。該系統證明了生成式語言建模可以解決傳統自動定理證明器的一個主要限制：生成原始數學術語的能力。

GPT-f and the Metamath Formalization Language

GPT-f 是一個專為 Metamath 形式化語言構建的自動證明器和證明助手。透過將基於 transformer 的語言建模應用於形式化數學任務，研究人員旨在縮小人類進行定理證明的方式與自動化系統通常運作方式之間的差距。

Key Capabilities and Contributions

GPT-f 的主要成就係其能夠生成原始數學術語以促進證明。這種能力讓系統能夠找到新的、簡短的證明，隨後被收錄進 Metamath 主函式庫。

根據研究，這標誌著首次有基於深度學習的系統貢獻了被形式化數學社群採用的證明。

Implications for Automated Theorem Proving

傳統的自動定理證明器通常在生成原始數學術語方面面臨困難，而這正是人類擅長的任務。GPT-f 顯示了生成式語言模型可以用於克服這一瓶頸，為開發更強大的自動證明助手提供了一條路徑，使其能夠貢獻有意義且經過驗證的數學知識。