プログラム合成

2013年、ペンシルベニア大学、カリフォルニア大学バークレー校、マサチューセッツ工科大学の研究者らによって、構文誘導型合成（SyGuSと略記）と呼ばれるプログラム合成問題の統一フレームワークが提案された。^{[ 6 ]} SyGuSアルゴリズムへの入力は、論理仕様と、有効な解の構文を制約する式の文脈自由文法から構成される。 ^{[ 7 ]}例えば、2つの整数の最大値を返す関数fを合成する場合、論理仕様は次のようになる。

( f ( x , y ) = x ∨ f ( x , y ) = y ) ∧ f ( x , y ) ≥ x ∧ f ( x , y ) ≥ y

そして文法は次のようになるかもしれない。

< Exp > ::= x | y | 0 | 1 | < Exp > + < Exp > | ite( < Cond > , < Exp > , < Exp > ) < Cond > ::= < Exp > <= < Exp >

ここで「ite」は「if-then-else」を表します。

ite(x <= y, y, x)

これは文法と仕様に準拠しているため、有効な解決策となるでしょう。

2014年から2019年にかけて、毎年開催される構文誘導型合成コンペティション（SyGuS-Comp）では、プログラム合成のためのさまざまなアルゴリズムが競技形式で比較されました。^{[ 8 ]}このコンペティションでは、 SMT-Lib 2に基づく標準化された入力フォーマットである SyGuS-IF が使用されました。たとえば、次の SyGuS-IF は、2 つの整数の最大値（上記参照）を合成する問題をエンコードしたものです。

(セットロジックLIA) (synth-fun f ((x Int) (y Int)) Int ((i Int) (c Int) (b Bool)) ((i Int (cxy (+ ii) (ite bii))) (c Int (0 1)) (b Bool ((<= ii))))) (declare-var x Int) (declare-var y Int) (制約 (>= (fxy) x)) (制約 (>= (fxy) y)) (制約 (または (= (fxy) x) (= (fxy) y))) （チェックシンセ）

準拠したソルバーは、次のような出力を返す可能性があります。

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

反例誘導型帰納合成（CEGIS）は、健全なプログラム合成器を構築するための効果的なアプローチです。^{[ 9 ] [ 10 ]} CEGISは、候補プログラムを生成するジェネレータと、候補が仕様を満たしているかどうかをチェックする検証器という2つのコンポーネントの相互作用を伴います。

入力の集合I、可能なプログラムの集合P、および仕様Sが与えられたとき、プログラム合成の目標は、Iのすべての入力iに対してS ( p , i ) が成り立つようなP内のプログラムp を見つけることです。CEGIS は、ジェネレータと検証器によってパラメータ化されています。

• ジェネレータは入力の集合Tを受け取り、T内のすべての入力に対して正しい候補プログラムcを出力します。つまり、T内のすべての入力tに対してS ( c , t ) が成り立つような候補です。
• 検証器は候補プログラムcを受け取り、プログラムがすべての入力に対してS を満たす場合はtrueを返し、そうでない場合は反例、つまりS ( c , e ) が失敗するようなI内の入力eを返します。

CEGISは、ジェネレーターと検証器をループで実行し、反例を蓄積します。

アルゴリズムcegisは入力です : プログラムジェネレータ生成、 検証者検証、 仕様spec、 出力：仕様を満たすプログラム、または失敗 inputs := 空の集合 loop candidate := generate ( spec , inputs ) if verify ( spec , candidate ) then return candidate else verifyが反例eを生成する add e to inputs end if

CEGISの実装では、通常、検証ツールとしてSMTソルバーが使用されます。

CEGISは、反例誘導型抽象化洗練（CEGAR）に触発されたものである。 ^{[ 11 ]}

証明規則には以下が含まれます。

• 節以外の解決方法（表を参照）。

例えば、55行目はアサーション式を解くことによって得られます。${\displaystyle E}$51から${\displaystyle F}$52から、どちらもいくつかの共通のサブフォーミュラを共有しています${\displaystyle p}$. 分解は、次の式の選言として形成されます。${\displaystyle E}$、 と${\displaystyle p}$に置き換えられました${\displaystyle {\it {true}}}$、 そして${\displaystyle F}$、 と${\displaystyle p}$に置き換えられました${\displaystyle {\it {false}}}$この解決文は論理的に次の連言から導かれる。${\displaystyle E}$そして${\displaystyle F}$より一般的には、${\displaystyle E}$そして${\displaystyle F}$統合可能な部分式は2つだけ必要です${\displaystyle p_{1}}$そして${\displaystyle p_{2}}$それぞれ、その分解液は${\displaystyle E\theta }$そして${\displaystyle F\theta }$以前と同様に、${\displaystyle \theta }$は、​${\displaystyle p_{1}}$そして${\displaystyle p_{2}}$この規則は節の解決を一般化するものである。^{[ 22 ]}

親式のプログラム項は、58行目に示すように結合され、レゾルベントの出力を形成します。一般的には、${\displaystyle \theta }$後者にも適用されます。サブ式${\displaystyle p}$出力に表示される場合は、計算可能なプロパティに対応するサブフォーミュラのみを解決するように注意する必要があります。

• 論理変換。

例えば、${\displaystyle E\land (F\lor G)}$変換可能${\displaystyle (E\land F)\lor (E\land G)}$）は、アサーションとゴールの両方で同じ意味を持つため、同様に使用されます。

• 連言的主張と選言的目標の分離。

下記の例文の11行目から13行目にその例を示します。

• 構造的誘導。

このルールにより、再帰関数の合成が可能になります。与えられた事前条件と事後条件「与えられた${\displaystyle x}$そのため${\displaystyle {\textit {pre}}(x)}$、 探す${\displaystyle f(x)=y}$そのため${\displaystyle {\textit {post}}(x,y)}$適切なユーザー指定の整列${\displaystyle \prec }$の領域${\displaystyle x}$常に「主張」を追加することは賢明です。${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$「. ^{[ 23 ]}このアサーションで解決すると、再帰呼び出しが導入される可能性があります。${\displaystyle f}$プログラム期間中。

例として、Manna、Waldinger (1980)、p.108-111 に、整列順序を使用して 2 つの与えられた整数の商と余りを計算するアルゴリズムが合成されている。${\displaystyle (n',d')\prec (n,d)}$定義される${\displaystyle 0\leq n'<n}$（110ページ）

マレーは、これらの規則が一階述語論理に対して完全であることを示した。^{[ 24 ]} 1986年、マンナとワルディンガーは、等号も扱うために一般化されたE分解規則とパラモジュレーション規則を追加した。^{[ 25 ]}後に、これらの規則は不完全であることが判明した（しかし、それでも健全である）。^{[ 26 ]}

おもちゃの例として、最大値を計算する関数プログラム${\displaystyle M}$2つの数字${\displaystyle x}$そして${\displaystyle y}$以下のように導出できる。

要件の説明「最大値は任意の与えられた数値以上であり、与えられた数値のいずれかである」から始めて、一次式${\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$は、その形式的な翻訳として得られます。この式は証明されるべきものです。逆スコレム化により、^{[注4 ]} 10行目の仕様が得られ、大文字と小文字はそれぞれ変数とスコレム定数を表します。

11行目で分配法則の変換規則を適用した後、証明目標は選言となり、したがって12行目と13行目の2つのケースに分割できます。

最初のケースに移ると、1行目の公理を用いて12行目を解くと、プログラム変数がインスタンス化される。${\displaystyle M}$14行目。直感的には、12行目の最後の連言は、次の値を規定している。${\displaystyle M}$この場合は、 を考慮に入れなければなりません。正式には、上記の 57 行目に示されている非節解決ルールが 12 行目と 1 行目に適用されます。

• p はA=Aとx=Mの共通例x=xであり、後者の式を構文的に統一することによって得られる。
• F[ p ]が真∧ x=xであり、これはインスタンス化された行 1から得られます( pの周りのコンテキストF[⋅]が見えるように適切にパディングされています)。
• G[ p ]は、インスタンス化された行 12 から得られるx ≤ x ∧ y ≤ x ∧ x = xである。

降伏 ${\displaystyle \lnot (}$真∧偽) ∧ ( x ≤ x ∧ y ≤ x ∧真${\displaystyle )}$、これは以下のように簡略化されます。${\displaystyle x\leq x\land y\leq x}$。

同様に、14行目は解決によって15行目、そして16行目を生成します。また、2番目のケースでは、${\displaystyle x\leq M\land y\leq M\land y=M}$13行目も同様に処理され、最終的に18行目になります。

最後のステップでは、58行目の解決ルールを使用して、両方のケース（つまり16行目と18​​行目）が結合されます。このルールを適用するには、準備ステップ15 → 16が必要でした。直感的には、18行目は「in case」と読むことができます。${\displaystyle x\leq y}$出力${\displaystyle y}$は（元の仕様に関して）有効ですが、15行目には「${\displaystyle y\leq x}$出力${\displaystyle x}$は有効です。ステップ 15 → 16 により、ケース 16 と 18 の両方が相補的であることが確立されました。^{[注 5 ]}行 16 と 18 の両方にプログラム項が含まれているため、条件式がプログラム列に現れます。目標式は${\displaystyle {\textit {true}}}$導出され、証明が完了し、プログラム列の「${\displaystyle {\textit {true}}}$「行にはプログラムが含まれています。」