代数图构造的神经符号发现

中文摘要 AI 辅助

目前存在多种搜索具有指定性质的图的方法，比如SAT求解器和专用生成器，这些方法将结果以原始数据形式返回，如邻接矩阵或编码字符串。这些原始数据可以证明图的存在，但无法揭示图的任何结构性质。本文研究的问题是：仅提供这种原始数据时，能否自动发现简短的代数描述，例如Cayley图$\text{Cay}(\boldsymbol{"}, summary_cn":"提出一种基于通用大语言模型的神经符号智能体，结合SageMath计算机代数系统，可从原始图数据中发现代数图构造，在100个高度对称图基准上全部成功，还找到Bernhart-Kainen可散度猜想的最小反例。

英文摘要

There are several methods for searching for graphs with prescribed properties, such as SAT solvers and specialized generators. These methods return the result as raw data: an adjacency matrix or a string encoding. The raw data certifies that the graph exists, but it does not reveal any structural properties of the graph. We ask whether one can automatically discover a short algebraic description if only this raw data is provided. We look for a description such as a Cayley graph $\mathrm{Cay}(Γ, S)$ or a lexicographic product $C_5[K_3]$. We address this question with a neurosymbolic approach. We propose an agent that runs on a general-purpose large language model with no fine-tuning or per-target training. The model interleaves reasoning with calls to the computer algebra system SageMath: it analyzes the target graph, proposes and tests candidate constructions, and revises them until the output matches the target. The agent communicates with SageMath through a Model Context Protocol (MCP) server, which we release as a general-purpose bridge. Whether a construction matches the target is checked by a single exact isomorphism test, and therefore rests on the symbolic side and not on the model. We test the approach on a benchmark of 100 highly symmetric graphs, namely two-orbit graphs on up to 25 vertices; the benchmark was fixed in advance. Our agent could find verified algebraic constructions for all of them, without falling back to raw encodings. A strong template-enumeration baseline reaches only about $20\%$, and a catalog lookup could not identify any of these graphs. However, construction quality declines when symmetry is removed. As a concrete application, we identify the smallest known counterexample to the Bernhart-Kainen dispersability conjecture, a $16$-vertex graph that enumeration found as raw data. For this graph, our agent found an explicit algebraic construction.

发表机构

• TU Wien（维也纳技术大学）

机构由 AI 辅助整理，请以论文原文为准。