論文の概要: VALG: An Agentic System for ML Theory Research
- arxiv url: http://arxiv.org/abs/2608.13060v1
- Date: Thu, 13 Aug 2026 10:23:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 18:29:38.476228
- Title: VALG: An Agentic System for ML Theory Research
- Title（参考訳）: VALG:ML理論研究のためのエージェントシステム
- Abstract要約: 我々は,多レベル検証,学習理論問題の適応的定式化,グラフ構造化された証明開発を組み合わせたエージェントシステムであるVALGを開発した。
VALG は COLT 2026 のオープンな5つの問題から9つのサブプロブレムに対して評価する。
- 参考スコア（独自算出の注目度）: 35.29223690479372
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Machine learning theory studies learning procedures through mathematical setups in which the data model, training protocol, oracle access, loss, metric, and randomness define the phenomenon that a theorem is meant to explain. Solving an open problem therefore requires the problem formulation, theorem target, and proof mechanism to be developed in concert. Researchers formulate hypotheses, test them through preliminary theoretical or empirical analysis, and refine both assumptions and proofs. We investigate whether this process can be organized as an autonomous agentic workflow for ML theory research. We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development. Within each source-relative theorem branch, VALG maintains a fixed mathematical specification, checks the theorem-level composition of a typed proof-dependency graph, and constructs and reviews local proofs in dependency order. When a proof attempt fails, VALG identifies whether the obstruction lies in a derivation, the proof structure, or the theorem formulation and routes the next attempt accordingly. Formulation-level obstructions initiate an explicitly related variant or relaxation, preserving the mathematical relation between the resulting theorem and the source problem. We evaluate VALG on nine subproblems from five COLT 2026 open problems. Two runs produce internally finalized theorem candidates that match the scope of their source briefs; the remaining seven yield restricted-method results, special cases, or conditional theorems. These case studies show how VALG keeps source-scope matches, relaxations, conditional results, and blocked attempts mathematically distinct. VALG is open source at https://github.com/DechenZhang/VALG-ML-Theory-Agent.
- Abstract（参考訳）: 機械学習理論は、データモデル、トレーニングプロトコル、オラクルアクセス、損失、メートル法、ランダムネスが、定理が説明しようとする現象を定義する数学的設定を通じて、学習手順を研究する。
したがって、オープンな問題の解決には、共同で開発する問題定式化、定理のターゲット、証明メカニズムが必要である。
研究者たちは仮説を定式化し、予備的な理論的または経験的な分析を通じてそれらを検証し、仮定と証明の両方を洗練させる。
本稿では,ML理論研究のための自律的なエージェントワークフローとして,このプロセスを組織化できるかどうかを検討する。
我々は,多レベル検証,学習理論問題の適応的定式化,グラフ構造化された証明開発を組み合わせたエージェントシステムであるVALGを開発した。
VALGは、各ソース相対定理ブランチ内で、固定された数学的仕様を維持し、型付き証明依存グラフの定理レベル構成をチェックし、依存順序で局所的な証明を構築してレビューする。
証明試みが失敗すると、VALGは、障害が導出、証明構造、あるいは定理の定式化の中に存在するかどうかを特定し、それに従って次の試みをルーティングする。
定式化レベルの障害は明示的に関連する変種や緩和を開始し、結果の定理と元問題の間の数学的関係を保存する。
VALG は COLT 2026 のオープンな5つの問題から9つのサブプロブレムに対して評価する。
2つのランは、ソースブリーフのスコープに一致する内部決定された定理候補を生成し、残りの7つの収率制限されたメソッド結果、特別な場合、条件付き定理を生成する。
これらのケーススタディは、VALGがソーススコープの一致、緩和、条件付き結果、ブロックされた試みを数学的に区別する方法を示している。
VALGはhttps://github.com/DechenZhang/VALG-ML-Theory-Agentでオープンソースとして公開されている。
関連論文リスト
- A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。
目的は文書をリーンに変えることである。ゲームは開発がコンパイルされたときに勝利し、残念なことは含まない。マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。
ケーススタディは、ドブルシンの平均場経路を通した非線形ブラソフ方程式の正当性に対する完全で公理クリーンな定式化である。
論文 参考訳（メタデータ） (2026-07-09T23:17:54Z) - Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory [17.20738506776148]
漸近統計理論はAI支援形式化の挑戦的な領域である。
複数のエージェントから構築された仮説に分類したLean 4形式化パイプラインを提案する。
結果として得られるリーン開発は、公理的クリーンでソース忠実です。
論文 参考訳（メタデータ） (2026-06-03T20:03:38Z) - A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
定理証明のための自己表現アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。
定理の基底グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。
論文 参考訳（メタデータ） (2026-06-01T08:12:47Z) - Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
エージェント定理プロバーは、数学的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証とを結合したパイプラインである。
本稿では, 検証された証明に到達する有限水平成功確率として定義される分布的視点を提案し, 証明可能性を導入する。
本稿では,エージェント定理の証明者が実世界の偏りのある問題分布にいつ,なぜ成功するのかを,原理的かつコンポーネントに敏感に説明する。
論文 参考訳（メタデータ） (2026-02-11T05:22:24Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z) - Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
I-FKGC(inductive few-shot knowledge graph completion)と呼ばれる課題に焦点をあてる。
帰納的推論(inductive reasoning)の概念に着想を得て,I-FKGCを帰納的推論問題とした。
本稿では,仮説の連成分布をモデル化したニューラルプロセスに基づく仮説抽出器を提案する。
第2のモジュールでは、この仮説に基づいて、クエリセットのトリプルが抽出された仮説と一致するかどうかをテストするグラフアテンションベースの予測器を提案する。
論文 参考訳（メタデータ） (2024-08-03T13:37:40Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。