開源數學定理證明模型 五項評測三項奪冠

訓練與部署的錯位

近年開源模型在定理證明基準上的成績持續上升，但增長路徑日趨同質：擴大模型與數據規模，部署階段再疊加檢索與多輪修正流程，邊際收益遞減。

檢索訊號、編譯器反饋與失敗修復大多只在外部接入，模型訓練階段並未系統學習利用這些訊號，形成訓練與部署之間的策略錯位，制約魯棒性與泛化。