VALG、型付き証明グラフで定理の書き換えを追跡――COLTの未解決9サブ課題で当初のスコープを維持できたのは2件のみ

[VALG](https://arxiv.org/abs/2608.13060)は、形式証明エージェントが通常避けるステップに取り組もうとしている。研究課題がまだ完全に形式化されていない段階で、元の問題を途中ですり替えることなく、エージェントが仮定や定理の目標をどのように修正するかという課題だ。システムはまず文献を検索し、異なる研究上の視点からブランチを構築する。その後、実現可能な各アイデアを、データモデル、学習器、oracle、損失、量化条件、単一の目標を含む「定理コントラクト」として固定する。

証明段階に入ると、VALGは論証を型付き有向非巡回グラフとして表現する。ソースノードは元の仮定、中間ノードは補題、唯一のシンクノードは目標定理である。グローバルチェッカーが、ノードのインターフェース、確率と収束のモード、パラメータ依存関係、閉じた論証の整合性を先に確認する。その後、ローカルエージェントが依存関係の順序に従って導出を完成させ、最後に構造、厳密性、引用、境界ケースなどを担当する独立したレビュアーの判定を統合する。失敗が特定部分の導出に限られる場合は、その部分だけをやり直す。証明の構成が成立しない場合はグラフを再構築する。定理そのものに障害がある場合に限り、元の問題との関係を明示した制限版または緩和版を作成する。

著者らは、COLT 2026の未解決問題を扱う5本の論文から9件のサブ課題を選び、評価を行った。対象はテンソル分解、1-bit平均推定、深層モデルと線形モデル、差分プライバシー学習、オンライン最適化に及ぶ。9回の実行で計22件の内部確定済み定理候補が残ったが、元の研究概要のスコープに沿う候補を生成できたのは2回だけだった。それ以外は特殊ケース、制限された手法、または条件付き定理だった。この比率自体が重要なシグナルである。エージェントが監査可能な研究過程を維持できることは、未解決問題を広く解決できることを意味しない。

[オープンソース実装](https://github.com/DechenZhang/VALG-ML-Theory-Agent)は、Codexのスキル、サブエージェント、ファイル化された中間成果物で構成され、人間による承認モードとautopilotモードの両方を備える。エンジニアリングおよび研究チームが次に注目すべきなのは、候補が独立した専門家による再審査や、Leanなどの証明支援系による形式化に耐えられるかどうかだ。現時点の「internally finalized」は、あくまでシステム自身によるレビュー結果であり、学術界で検証済みの新定理と見なすことはできない。