核心概念
提出了一種新的圖神經網絡程式設計語言 $\mu\mathcal{G}$,旨在解決深度學習模型的可解釋性和可信度問題。$\mu\mathcal{G}$ 提供了一種形式化的方式來定義和組合圖神經網絡,並具有嚴格的語義定義。
要約
本文提出了一種新的圖神經網絡程式設計語言 $\mu\mathcal{G}$。
-
語法介紹:
- $\mu\mathcal{G}$ 包含基本項 $\iota$、$\psi$、$\nabla_\phi^\sigma$、$\Delta_\phi^\sigma$,以及序列組合、並行組合、選擇和迭代等操作符。
- 這些項和操作符的組合可以定義各種圖神經網絡模型。
-
語義定義:
- 給出了 $\mu\mathcal{G}$ 表達式的形式化的去符號化語義。
- 證明了去符號化語義與操作語義的等價性。
- 定義了 $\mu\mathcal{G}$ 的類型系統,並證明了類型安全性。
-
圖形化表示:
- 介紹了 $\mu\mathcal{G}$ 程序的圖形化表示,提供了一種更加直觀的使用方式。
-
應用展示:
- 展示了如何使用 $\mu\mathcal{G}$ 定義一些流行的圖神經網絡模型。
- 展示了如何使用 $\mu\mathcal{G}$ 進行 CTL 模型檢查。
總的來說,$\mu\mathcal{G}$ 是一種新穎的圖神經網絡程式設計語言,旨在提高深度學習模型的可解釋性和可信度。它提供了一種形式化的方式來定義和組合圖神經網絡,並具有嚴格的語義定義。