核心概念
miniCTX 是一個新的基準測試,旨在評估神經定理證明器在真實世界場景中的性能,其中證明依賴於新的上下文資訊,例如定義、引理和檔案結構。
摘要
miniCTX:利用(長)上下文資訊進行神經定理證明的新基準測試
這篇研究論文介紹了 miniCTX,這是一個用於評估神經定理證明器的新基準測試。miniCTX 的獨特之處在於它側重於真實世界的定理證明,其中證明依賴於豐富的數學上下文,而這些上下文在訓練模型時可能並不可見。
開發一個基準測試,用於評估神經定理證明器在真實世界場景中的性能,其中證明依賴於新的上下文資訊。
測試現有神經定理證明模型在處理真實世界定理證明任務中的能力。
建立 miniCTX 基準測試,其中包含來自各種 Lean 專案的真實世界定理,以及證明這些定理所需的上下文資訊。
開發 NTP-TOOLKIT,用於自動從 Lean 專案中提取相關定理和上下文。
在 miniCTX 上評估幾種現有的基準模型,包括不同的微調和提示策略,以及使用前提選擇的方法。
提出檔案微調,這是一種強大的基準方法,用於使用完整檔案上下文訓練模型,其中在訓練期間提供定理陳述及其周圍的上下文。