Automated conjecturing with \emph{TxGraffiti}

「TxGraffiti による自動推測」の技術的概要

問題定義
本論文は、数学的対象（特にグラフ）の数値不変量間の、数学的に有用で冗長性がなく、解釈可能な不等式の生成という、自動推測の課題に取り組む。自動定理証明は成熟した分野であるが、自動推測生成は歴史的に「過剰な命題」問題に苦しんできた。これは、体系的な列挙が、データベース上で真であるが、陳腐または冗長な膨大な数の命題を生み出す現象である。目標は、これらの命題をフィルタリングし、真の新たな情報（情報性）を提供し、人間の検証と証明に適するものを特定することである。

手法
本論文は、数学的対象の有限かつバージョン管理されたスナップショット表上で動作する、ヒューリスティックおよび最適化に基づくシステムであるTxGraffiti（テキサス・グラフィティ）を紹介する。その前身である Graffiti や Graffiti.pc が探索中に不変量を動的に計算するのに対し、TxGraffiti は証拠基盤を静的なアーティファクトとして扱う。

推測生成パイプラインは、以下の段階で構成される。

1. データキュレーション（スナップショット表）:

   • 行が対象（グラフ）を、列が事前計算された数値不変量（例：独立数 $\alpha$、マッチング数 $\mu$）およびブール述語（例：「連結である」、「正則である」）を表す表が構築される。
   • キュレーション戦略は、ランダム性よりも網羅性を優先し、特に極値構成、等式の証人（鋭い場合）、および反例を包含して、表が診断的に豊かであることを保証する。

2. 最適化による候補生成:

   • 選択された目標不変量 $\alpha$ とブール述語 $P$（仮説）に対して、システムは $\alpha \le mx + b$ または $\alpha \ge mx + b$ の形式のアフィン境界（ここで $x$ は予測子不変量）を検索する。
   • 複雑な式木を列挙するのではなく、TxGraffiti は単純なパラメトリック仮説クラス（単変量アフィン境界）を固定し、**線形計画問題（LP）**を解くことで係数を適合させる。
   • 上限 LP: 述語 $P$ を満たすすべての行について $\alpha_i \le mx_i + b$ という制約の下で、総スラック $\sum (mx_i + b - \alpha_i)$ を最小化する。
   • 下限 LP: $\alpha_i \ge mx_i + b$ という制約の下で、総スラックを最大化する（または負のスラックを最小化する）。
   • システムは、派生列（例：$n-\mu$、$\Delta^2$）でスキーマを拡張することで、多変量境界および非線形関係もサポートするが、デフォルトの Web インターフェースは解釈性の観点から単一予測子モデルを優先する。

3. フィルタリング（静的ダルマティアンヒューリスティック）:

   • 冗長性を管理するため、TxGraffiti は静的ダルマティアンヒューリスティックを採用する。
   • タッチ数: 不等式が等式として成立する（鋭い事例）スナップショット内の対象の個数として定義される。
   • 選択ロジック: 候補はタッチ数でソートされる。候補が、以前に受け入れられた代表者の鋭い集合によってまだカバーされていない少なくとも 1 つの対象に触れる場合、その候補は「代表者」として受け入れられる。ある候補の鋭い集合が受け入れられた代表者のそれと同一である場合、それは「エイリアス」（同じ等式軌跡の異なる構文形式）として保持される。新しい鋭い事例を追加しない候補は破棄される。

主要な貢献

• システムアーキテクチャ: TxGraffiti は、インタラクティブな Web アプリケーションおよびオープンソースの Python パッケージ（txgraffiti）として提供されるモジュール型システムとして提示される。これは不変量の計算と推測生成を分離し、固定データセット上での迅速な反復を可能にする。
• 最適化ベースの適合: 本論文は、文法ベースの列挙（式を生成し、それらをテストする）から、最適化ベースの適合（特定の予測子に対して最も tight な境界を見つけるために LP を解く）へとパラダイムを転換する。これにより、生成された候補は構造的に「テーブル上で真」であり、tightness に対して最適化されることを保証する。
• 静的ダルマティアンフィルタリング: 固定されたスナップショットへのダルマティアンヒューリスティックの適応により、高い「タッチ」（多くの鋭い証人）を持つ境界を優先し、冗長性を排除する、単一パスかつ決定論的なフィルタリングプロセスが可能になる。
• 解釈性: 仮説クラスを単純なアフィンテンプレートに制限し、係数を有理数化することで、システムは簡潔で人間が読み取れる推測を生成する。

結果
本論文は、いくつかの例を通じてシステムの有効性を示す。

• ワークフローの図示: 全支配数 $\gamma_t$ を用いて、システムは $\Delta(G) \le 3$ であるグラフに対して $\gamma_t(G) \ge \frac{2}{3}R(G)$ という境界を生成した。これはすぐに $\Delta(G)$ を含む定理に一般化され、標準的な評価を用いて証明された。
• 刺激された出版物: 本論文は、TxGraffiti の推測として生まれ、その後証明されたいくつかのグラフ理論的結果をカタログ化している。
  • 独立数対マッチング数: $r$-正則グラフに対して $\alpha(G) \le \mu(G)$ という推測は [51] で証明された。
  • ゼロフォース境界: ゼロフォース数（$Z, Z_t, Z_+$）と支配数および独立数パラメータとの関係に関するいくつかの不等式が推測され、証明された。これには、爪なしグラフに対する $Z(G) \le \beta(G)$ や、3 正則グラフに対する境界が含まれる。
  • 未解決問題: システムは、$\Delta \le 3$ である連結グラフに対する $Z(G) \le \alpha(G) + 1$ という推測を特定したが、これは部分的な結果は存在するものの、依然として中心的な未解決問題である。

意義と主張
本論文は、TxGraffiti を自律的に深い定理を発見するツールではなく、人間の数学的探求を促進する構造化された証拠生成器として位置づける。

• 経験的妥当性: システムは、キュレーションされたスナップショットのすべての事例で成立する「テーブル上で真」の命題を生成する。著者は明示的に「定理」という用語を形式的証明によって確立された命題に留保し、システムの出力を推測として区別する。
• 哲学的立場: Fajtlowicz（Graffiti を設計した人物）の経験的視点を踏襲し、本論文は、機械が妥当で深い推測を生み出す能力は経験的事実であり、機械をオープンエンドな数学的発見における意味ある参加者とする見方を支持すると論じる。
• スケーラビリティと再現性: スナップショット表をバージョン管理され監査可能なアーティファクトとして扱うことで、TxGraffiti はデータ破損の堅牢性の問題に対処し、証拠基盤が成長するにつれて推測が再現および洗練されることを保証する。

著者は、現在の実装がグラフ不変量に焦点を当てているが、「スナップショット表パラダイム」および最適化とフィルタリングのパイプラインは、対象が計算可能な特徴と述語を許容するあらゆる分野に広く適用可能であると結論づける。