Logic of Differentiable Logics: Towards a Uniform Semantics of DL

要約

微分可能ロジック (DL) は、論理仕様を満たすようにニューラル ネットワークをトレーニングする方法として最近提案されています。
DL は、仕様を記述した構文と、構文内の式を損失関数に変換する解釈関数で構成されます。
これらの損失関数は、標準の勾配降下法アルゴリズムを使用したトレーニング中に使用できます。
既存の DL にはさまざまな種類があり、それらが扱われる形式のレベルが異なるため、その特性と実装の体系的な比較研究が困難になっています。
この論文では、微分可能ロジックの論理 (LDL) と呼ばれる、DL を定義するためのメタ言語を提案することで、この問題を解決します。
構文的には、既存の DL の構文を FOL に一般化し、ベクトルと学習器に関する推論のための形式主義を初めて導入します。
意味的には、さまざまな既存の DL から生じる損失関数を定義するためにインスタンス化できる一般的な解釈関数が導入されています。
私たちは LDL を使用して、既存の DL のいくつかの理論的特性を確立し、ニューラル ネットワーク検証における実証研究を実施します。

要約(オリジナル)

Differentiable logics (DL) have recently been proposed as a method of training neural networks to satisfy logical specifications. A DL consists of a syntax in which specifications are stated and an interpretation function that translates expressions in the syntax into loss functions. These loss functions can then be used during training with standard gradient descent algorithms. The variety of existing DLs and the differing levels of formality with which they are treated makes a systematic comparative study of their properties and implementations difficult. This paper remedies this problem by suggesting a meta-language for defining DLs that we call the Logic of Differentiable Logics, or LDL. Syntactically, it generalises the syntax of existing DLs to FOL, and for the first time introduces the formalism for reasoning about vectors and learners. Semantically, it introduces a general interpretation function that can be instantiated to define loss functions arising from different existing DLs. We use LDL to establish several theoretical properties of existing DLs, and to conduct their empirical study in neural network verification.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google