學習探索有趣的數學
為何重要
這項研究揭示了大型語言模型從「窩裡橫」（模仿訓練資料）邁向「自主發現」（探索未被驗證的定理）的關鍵技術路徑。對於形式化驗證與 AI Agent 領域而言，自動生成高價值命題並構建自我擴充套件的數學圖書館，是解決學術研究繁重勞動與自動化潛力的重大突破。
大型語言模型（LLMs）雖已能解決複雜數學問題，但新定理的實用性仍有待確認。研究團隊提出以「證明長度」與「語句長度」的比率來定義定理的「內在有趣性」，並訓練了一個 27B 引數模型來精準預測證明難度。
- 定義的「內在有趣性」包含證明長度佔語句長度的比例，該指標與下游的實用性強烈相關。
- 訓練出的 27B 模型在預測證明難度上，準確度優於目前領先的通用語言模型。
- 最佳化新指標後，產生的定理與既有庫 Mathlib 的重疊率從 91.9% 大幅下降至 30.6%。