論文の概要: AutoGraphForge: Towards Automated Graph Theory Discovery
- arxiv url: http://arxiv.org/abs/2609.03478v1
- Date: Thu, 03 Sep 2026 07:35:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-04 18:28:38.970206
- Title: AutoGraphForge: Towards Automated Graph Theory Discovery
- Title（参考訳）: AutoGraphForge: グラフ理論の自動発見を目指す
- Abstract要約: AutoGraphForgeは、自動グラフ理論の導出-拡散-ホルマライゼーション-自明なシステムである。
新規性フィルタは、既知の結果によって既に候補が示唆されているか否かを線形プログラムを介して決定する。
HPCクラスタ上で数ラウンド実行されると、リフューテーションデータセットを生き残った6,522ドルの予想が生成される。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator proposes conjectures over a small, evolving snapshot table $T$ (initially a few hundred graphs with their computed invariants) that grows only by counterexamples to its own conjectures. A novelty filter of $559$ classical and folklore relations, closed under transitive composition and linear identity substitution, decides via a linear program whether a candidate is already implied by known results. Surviving candidates are tested against a dataset of about $348,000$ graphs, unioning the complete House of Graphs invariant export, the exhaustive census of all connected graphs on at most nine vertices, several extremal families (strongly regular, minimal Ramsey, Cayley, cages, barbells, lollipops, spiders), and random models. Counterexample-search algorithms then attack the remainder. Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset, the novelty filter and every active-search run -- among them nontrivial relations between the annihilation number and the edge-cover number for bipartite and regular graphs, which we prove by hand. A subsequent formalization and proving stage deterministically translates each surviving conjecture into a Lean 4 statement skeleton; every candidate proof is kernel-verified against a pinned mathlib4 and our custom invariant preamble. This stage integrates two neural provers -- DeepSeek-Prover-V2-671B (served with vLLM) and the Lean-specialised OProver-32B -- behind the independent kernel check. It is implemented end-to-end and passes initial sanity checks, with the full pipeline currently running on the cluster.
- Abstract（参考訳）: 本稿では,計算パイプラインであるAutoGraphForgeを,自動グラフ理論のコンジェクション・リフューティング・フォーマライズ・プロファイリングシステム向けに開発するプロジェクトについて報告する。
Graffiti3ジェネレータは、小さな進化したスナップショットテーブルに$T$(当初は計算された不変量を持つ数百グラフ)の予想を提案し、それ自身の予想に対して反例によってのみ成長する。
推移的構成と線形同一性置換の下で閉じた559ドルの古典的・民俗的関係の新規フィルタは、候補者が既に既知の結果によって示唆されているか否かを線形プログラムで決定する。
生存可能な候補は、約348,000ドルのグラフのデータセットに対してテストされ、完全なハウス・オブ・グラフの不変輸出、少なくとも9つの頂点上の全ての連結グラフの徹底的な国勢調査、いくつかの極端家族(通常、最小限のラムゼー、ケイリー、ケージ、バーベル、ロリポップ、クモ)、ランダムモデルである。
反例探索アルゴリズムが残りを攻撃する。
HPCクラスタ上で数ラウンド実行されると、このループは、難読化データセット、ノベルティフィルタ、そして全てのアクティブサーチランを生き残った6,522ドルの予想が得られます。
その後の形式化と証明段階は、生き残った各予想を決定論的にLean 4文の骨格に変換する。
このステージでは、DeepSeek-Prover-V2-671B(vLLMで提供)とLean-specialized OProver-32Bという2つのニューラルプローバを、独立カーネルチェックの裏で統合している。
エンドツーエンドで実装され、初期健全性チェックをパスし、完全なパイプラインは現在、クラスタ上で実行されています。
関連論文リスト
- GRAND-HC: Graph-Refined Author Name Disambiguation [58.02589236670033]
From-Scratch Name Disambiguation (SND) は、曖昧な名前を共有する論文を、異なる現実世界の著者のクラスタにまとめる。
完全なエンドツーエンドSNDフレームワークである textbfGRAND-HC を提案する。
論文 参考訳（メタデータ） (2026-08-24T08:21:28Z) - Neurosymbolic Discovery of Algebraic Graph Constructions [22.962110170304594]
この生データのみを提供する場合、短い代数的記述を自動的に発見できるかどうかを問う。
本研究では,汎用的な大規模言語モデル上で,微調整や目標ごとの訓練を行わないエージェントを提案する。
提案手法は高対称性グラフ100のベンチマークで検証する。
論文 参考訳（メタデータ） (2026-08-08T13:07:51Z) - Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound [0.0]
mathbbR3$ の最小コシェン=スペクターベクトル系に対する最もよく知られた下界は、半分が DRAT を出力するが、幾何的半分がそうでないような計算証明に依存する。
正則な正則な正則ケースツリー証明を導入し、その分割は分解因子と正則な二乗分解である。
すべての証明書、チェッカー、証明は、単一のビルドから利用可能で、再生可能である。
論文 参考訳（メタデータ） (2026-07-29T02:53:00Z) - Formalizing Flag Algebras in Lean [8.924529562496874]
ラズボロフのフラッグ代数法は、極端グラフ理論の不等式を証明する強力なツールである。
本手法の機械チェックによる形式化と,証明から保護までのコンパイラについて述べる。
ケーススタディは7つのターン型上界の形式的証明を与える。
論文 参考訳（メタデータ） (2026-07-26T07:07:29Z) - Quantum Algorithm for Identifying Hidden Graphs: Spectral Theory and Numerical Evidence [0.0]
隠れた$d$正規基底グラフを識別するための量子アルゴリズムを、その難解バージョンへのアクセスから$n$頂点に$G$を与える。
我々のアルゴリズムは概念的には単純で、$G_rm spire$ 上で連続時間ウォークし、古典的には pret*$ で 1 つのアダマールテストを行う。
論文 参考訳（メタデータ） (2026-05-11T20:44:32Z) - Accelerated Evolving Set Processes for Local PageRank Computation [75.54334100808022]
この研究は、パーソナライズされたPageRank計算を高速化するために、ネストした進化したセットプロセスに基づく新しいフレームワークを提案する。
このような局所化手法の時間複雑性は、PPRベクトルの$epsilon$-approximationを得るために$mintildemathcalO(R2/epsilon2), tildemathcalO(m)$によって上界となることを示す。
論文 参考訳（メタデータ） (2025-10-09T09:47:40Z) - Graph Random Features for Scalable Gaussian Processes [52.89901965157282]
離散入力空間上のスケーラブルなガウス過程へのグラフランダム特徴(GRF)の適用について検討する。
我々は、(穏やかな仮定の下で) GRF に対するベイズ的推論が、正確なカーネルに対して$O(N3)$のノード数に対して$O(N3/2)$の時間複雑性を楽しむことを証明した。
論文 参考訳（メタデータ） (2025-09-03T20:13:23Z) - On the Unlikelihood of D-Separation [69.62839677485087]
解析的な証拠として、大きなグラフ上では、d-分離は存在が保証されたとしても珍しい現象である。
PCアルゴリズムでは、その最悪ケース保証がスパースグラフで失敗することが知られているが、平均ケースでも同じことが言える。
UniformSGSでは、既存のエッジに対してランニング時間が指数的であることが知られているが、平均的な場合、それは既存のほとんどのエッジにおいても期待されるランニング時間であることを示す。
論文 参考訳（メタデータ） (2023-03-10T00:11:18Z) - Graph Signal Sampling for Inductive One-Bit Matrix Completion: a
Closed-form Solution [112.3443939502313]
グラフ信号解析と処理の利点を享受する統合グラフ信号サンプリングフレームワークを提案する。
キーとなる考え方は、各ユーザのアイテムのレーティングをアイテムイットグラフの頂点上の関数(信号)に変換することである。
オンライン設定では、グラフフーリエ領域における連続ランダムガウス雑音を考慮したベイズ拡張(BGS-IMC)を開発する。
論文 参考訳（メタデータ） (2023-02-08T08:17:43Z) - AnchorGAE: General Data Clustering via $O(n)$ Bipartite Graph
Convolution [79.44066256794187]
我々は、グラフ畳み込みネットワーク(GCN)を構築するために使用される生成グラフモデルを導入することにより、グラフに非グラフデータセットを変換する方法を示す。
アンカーによって構築された二部グラフは、データの背後にある高レベル情報を利用するために動的に更新される。
理論的には、単純な更新が退化につながることを証明し、それに従って特定の戦略が設計される。
論文 参考訳（メタデータ） (2021-11-12T07:08:13Z) - Inferring Hidden Structures in Random Graphs [13.031167737538881]
本研究では,ランダムなグラフ上に植えられた群集群集の検出と復元の2つの推論問題について検討する。
我々は、パラメータ $(n,k,q)$ や $Gamma_k$ の特定の性質の観点から、構造を検出・復元するための下限を導出し、これらの下限を達成するための計算学的に最適なアルゴリズムを示す。
論文 参考訳（メタデータ） (2021-10-05T09:39:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。