提升 AI 數學技能：反例驅動推理如何改變大型語言模型

數學大型語言模型（LLMs）展現了強大的問題解決能力，但它們的推理能力往往受到模式識別的限制，而不是基於真正的概念理解。當前的模型在訓練過程中主要依賴於接觸到類似的證明，這使得它們在面對新的數學問題時受到限制。這種限制使得LLMs無法進行高級數學推理，特別是在需要區分密切相關數學概念的問題上。LLMs通常缺乏的一種高級推理策略是反例證明，這是一種用來駁斥錯誤數學主張的核心方法。缺乏足夠的生成和使用反例的能力，妨礙了LLMs在高級數學概念推理中的表現，因此降低了它們在正式定理驗證和數學探索中的可靠性。

之前改善LLMs數學推理的嘗試可以分為兩種主要方法。第一種方法是合成問題生成，這種方法在大量由種子數學問題生成的數據集上訓練LLMs。例如，WizardMath使用GPT-3.5生成不同難度的問題。第二種方法是正式定理證明，這種方法訓練模型使用如Lean 4等證明系統，像Draft-Sketch-Prove和Lean-STaR，幫助LLMs進行結構化的定理證明。雖然這些方法增強了問題解決能力，但它們也有嚴重的限制。合成問題生成主要是記憶而非真正的理解，使得模型在面對新問題時容易失敗。另一方面，正式定理證明技術受到結構化數學語言的限制，這限制了它們在各種數學背景中的應用。這些限制突顯了需要一種替代的範式——一種關注概念理解而非模式識別的範式。

為了解決這些限制，提出了一個以反例為驅動的數學推理基準，稱為COUNTERMATH。這個基準專門設計用來評估和增強LLMs在證明中使用反例的能力。這項創新包括高品質的基準、數據工程過程和全面的模型評估。COUNTERMATH包含1,216個數學主張，每個主張都需要一個反例來駁斥。這些問題是從大學教科書中精心挑選的，並經過專家廣泛驗證。為了增強LLMs的反例推理能力，實施了一個自動數據收集過程，過濾和精煉數學證明數據，以獲得基於反例的推理示例。對於最先進的數學LLMs，如OpenAI的o1模型和經過微調的開源變體，COUNTERMATH進行了嚴格的評估。通過將重點轉向基於示例的推理，而非僅僅是定理證明，這種方法開啟了一條新的、尚未充分探索的訓練數學LLMs的路徑。

COUNTERMATH是基於四個核心數學學科構建的：代數、拓撲學、實分析和泛函分析。數據是通過多步驟過程建立的。首先，從教科書中收集數學陳述，並通過光學字符識別（OCR）轉換為結構化數據。數學家然後審查和註釋每個問題，以確保邏輯一致性和準確性。由於原始數據是中文，因此進行專業翻譯，並進行額外檢查。還提出了一個任務內數據工程框架，自動檢索基於反例的推理訓練數據。在這個框架中，應用了GPT-4o過濾和精煉技術，以從ProofNet和NaturalProof等外部來源提取相關證明。進行精煉以確保每個證明明確展示反例，這樣LLMs就能更有效地學習基於反例的推理。

對於最先進的數學LLMs在COUNTERMATH上的評估顯示了反例驅動推理的顯著差距。大多數模型無法使用反例來判斷陳述的真偽，這反映出深刻的概念弱點。不同數學領域的表現也不一，代數和泛函分析表現較好，而拓撲學和實分析因其抽象性仍然非常具挑戰性。開源模型的表現不如專有模型，只有少數模型具有中等的概念推理能力。然而，使用基於反例的數據進行微調顯著提高了性能，增強了判斷準確性和基於示例的推理。一個經過微調的模型，僅用1,025個基於反例的訓練樣本，表現顯著優於其基線版本，並且在分佈外的數學測試中具有強大的泛化能力。下表1的詳細評估顯示了基於F1分數和推理一致性指標的性能比較。在開源模型中，Qwen2.5-Math-72B-Instruct表現最佳（41.8 F1），但落後於專有模型如GPT-4o（59.0 F1）和OpenAI o1（60.1 F1）。微調帶來了顯著的提升，Qwen2.5-Math-7B-Instruct-SFT + Hint提示達到41.1 F1，證實了基於反例的訓練的有效性。

這個提議的方法提出了COUNTERMATH，一個基於反例的推理基準，旨在改善LLMs的數學概念能力。利用精心策劃的問題集和自動數據精煉過程，顯示出現有的LLMs在深度數學推理方面並不熟練，但可以通過基於反例的訓練大大增強。這些結果暗示未來的人工智慧研究需要專注於增強概念理解，而不是僅僅依賴於接觸式學習。反例推理不僅在數學中至關重要，還在邏輯、科學研究和正式驗證中發揮作用，因此這種方法可以擴展到各種基於人工智慧的分析任務中。

查看論文。這項研究的所有功勞都歸於這個項目的研究人員。此外，隨時在Twitter上關注我們，並別忘了加入我們的75k+機器學習SubReddit。

🚨 推薦閱讀 – LG AI研究發布NEXUS：一個先進的系統，整合代理人工智慧系統和數據合規標準，以解決人工智慧數據集中的法律問題。