數學推理合成資料集：設計與品質檢查

合成資料集不是把數學題大量改寫後丟進微調流程，而是一個可重現的資料產品。若希望模型學到可遷移的數學推理能力，資料集在生成前就要先定義：要解哪一類問題、哪些變化應保留、答案如何驗證、哪些資料絕不能流進測試集。

上一篇〈LLM 數學微調：合成資料的生成、驗證與評估重點〉談的是整體資料品質流程；本文則聚焦在建立「數學推理合成資料集」時，如何把需求、題型、標籤與驗證設計成可維護的工程規格。

先定義評估，再開始生成

最常見的失敗是先生成幾十萬筆資料，再尋找能提高的分數。更穩健的順序相反：先建立一組完全隔離的評估題，定義要觀察的能力，再決定訓練資料要補足哪些缺口。

例如，若目標是國中程度的多步驟文字題，評估不只要有加減乘除，也要包含單位換算、比例、條件順序改寫、無關資訊，以及資料不足時能否提出澄清。若只用一種固定模板生題，模型可能只學會辨識題面格式。

把題目看成「隱藏規格」與「自然語言表面」

好的合成資料生成器會先建立可檢查的隱藏規格，再生成對人類可讀的題目。隱藏規格可以包含變數、單位、運算式、約束條件與正確答案；自然語言題面只是這個規格的一種敘述方式。

這種設計有兩個好處。第一，答案能由規格重新計算，而不是依賴模型自評。第二，同一個底層關係可以生成不同敘事、數字範圍與條件順序的題目，讓資料多樣性來自真正的問題結構，而不只是同義詞替換。

每筆資料應保留哪些欄位？

除了題目與答案，建議為每個樣本保留足以追查的 metadata。概念上可以像這樣：

{
  "sample_id": "唯一識別碼",
  "problem_family": "比例與單位換算",
  "latent_spec": "可重算的變數與關係",
  "question": "自然語言題面",
  "final_answer": "已驗證答案",
  "answer_format": "數字與單位",
  "verifier": "驗證器與版本",
  "difficulty_tags": ["多步驟", "干擾資訊"],
  "split": "train | validation | test",
  "source_lineage": "種子資料與生成規則"
}

不需要把所有內部推理細節都暴露給使用者或寫進訓練資料，但至少要保存能重現與驗證的規格。當某一批資料被發現有問題時，這些欄位能幫助團隊定位是某個生成器版本、題型家族還是驗證器造成，而不是只能整批刪除。

從種子資料擴充，而非隨機堆量

一個實用方法是先準備少量高品質種子題，將每題拆成可變動的維度：數字、單位、對象、條件順序、需要的運算、干擾資訊與答案格式。生成時有系統地改變一至兩個維度，再用隱藏規格重算答案。

MetaMath 研究以不同視角重寫數學問題，並透過產生多條候選路徑、只保留答案正確的路徑來建立資料。這是「多視角擴充加上篩選」的研究例子；其效果是在特定模型與基準下觀察，不能替代自己的任務測試。MetaMath：Bootstrap Your Own Mathematical Questions for LLMs

MathGenie 則從小型問題—解答資料出發，擴充解法後以反向翻譯生成新題目，並為程式整合的解法設計驗證策略。它說明了「先處理可驗證的結構，再生成題面」的另一條路徑。MathGenie：Question Back-translation

四道品質閘門

第一道：規格與答案可執行

針對能程式化的題型，以獨立執行器重新計算答案，並檢查格式、單位、範圍與四捨五入規則。若規格本身無法執行，資料不應進入下一步。

第二道：題面是否忠實表達規格

答案正確不代表題目正確。應抽樣或以另一個受控程序檢查題面是否遺漏條件、誤換單位、把「至少」寫成「至多」，或引入規格中沒有的新資訊。這一層特別重要，因為模型可能產生看似自然但語意改變的改寫。

第三道：多樣性與去重

建立題型家族、生成規則、語言表達與數值範圍的分布報表，並以文字相似度與底層規格比對偵測近似重複。若同一個公式只換人名與數字就出現數萬次，資料量增加的意義有限。

第四道：資料切分與洩漏防護

train、validation、test 的切分應在生成規則與題型家族層級就規劃好，而不是最後才隨機切列。相同或近似的隱藏規格不應同時出現在訓練與測試中；公開評測資料也不應被不加辨識地混入生成來源。每次資料集版本更新，都應重新執行去重與切分稽核。

形式化驗證很強，但不是萬無一失

對定理證明或可形式化的邏輯題，定理證明器可用來檢查步驟的形式正確性。Theorem Prover as a Judge 的研究正是嘗試以形式化與定理證明回饋篩選／改進合成推理資料；同時，研究也指出把自然語言自動形式化本身仍會出錯。換句話說，驗證器能提高資料品質，但驗證器的輸入與失敗案例同樣需要被監測。Theorem Prover as a Judge for Synthetic Data Generation