VALG 以型別化證明圖追蹤定理改寫，9 個 COLT 開放子題僅 2 組維持原始範圍

[VALG](https://arxiv.org/abs/2608.13060) 嘗試處理形式證明代理通常避開的一步：當研究問題尚未完全形式化時，代理如何修改假設與定理目標，又不在過程中悄悄換掉原題。系統先檢索文獻，從不同研究視角建立分支，再把每個可行想法固定成包含資料模型、學習器、oracle、損失、量化條件及唯一目標的「定理合約」。

進入證明階段後，VALG 將論證表示成有型別的有向無環圖：來源節點是原始假設，中間節點是引理，唯一匯點是目標定理。全域檢查器先確認節點介面、機率與收斂模式、參數依賴及閉合論證是否相容；局部代理才依依賴順序完成推導，最後由結構、嚴謹度、引用及邊界案例等獨立審查器合併判決。失敗若只在某段推導便局部重做；若證明架構不成立則重建圖；只有定理本身受阻時，才建立與原問題明確相連的限制版或放寬版。

作者以 5 篇 COLT 2026 開放問題中的 9 個子題測試，涵蓋張量分解、1-bit 均值估計、深度模型與線性模型、差分私隱學習及線上最佳化。9 次執行共留下 22 個內部定稿定理候選，只有 2 次產生符合原始研究簡報範圍的候選，其餘是特殊案例、受限方法或條件式定理。這個比例反而是重要訊號：代理能維持可稽核的研究軌跡，不等於已能普遍解決開放問題。

[開源實作](https://github.com/DechenZhang/VALG-ML-Theory-Agent)以 Codex 技能、子代理及檔案化中間產物組成，並保留人工核准與 autopilot 兩種模式。工程與研究團隊下一步應關注候選能否經獨立專家重審或 Lean 等證明助理形式化；目前的「internally finalized」仍是系統自身審查結果，不能視為學界已驗證的新定理。