プログラム合成

コンピュータサイエンスにおいて、プログラム合成とは、与えられた高水準の形式仕様を証明可能に満たすプログラムを構築する作業である。プログラム検証とは対照的に、プログラムは与えられるのではなく構築される。しかし、どちらの分野も形式証明技術を利用しており、どちらも異なる程度の自動化アプローチから構成されている。自動プログラミング技術とは対照的に、プログラム合成における仕様は通常、適切な論理計算における非アルゴリズム的なステートメントである。^[1]

プログラム合成の主な用途は、仕様を満たす正確で効率的なコードを書くというプログラマの負担を軽減することです。しかし、プログラム合成は、スーパー最適化やループ不変量の推論にも応用できます。^[2]

1957年にコーネル大学で開催された記号論理学夏期講座で、アロンゾ・チャーチは数学的要件から回路を合成する問題を定義しました。^[3]この研究は回路のみに言及しておりプログラムには言及していませんが、プログラム合成に関する最も初期の記述の1つと考えられており、一部の研究者はプログラム合成を「チャーチの問題」と呼んでいます。1960年代には、人工知能の研究者によって「自動プログラマー」に関する同様のアイデアが検討されました。^[要出典]

それ以来、様々な研究コミュニティがプログラム合成の問題を検討してきました。注目すべき研究としては、 1969年のBüchiとLandweberによるオートマトン理論的アプローチ^[4]や、 MannaとWaldingerによる研究（1980年頃）などがあります。現代の高水準プログラミング言語の開発も、プログラム合成の一形態として理解することができます。

21世紀初頭、形式検証コミュニティや関連分野では、プログラム合成というアイデアに対する実用的な関心が急増しました。Armando Solar-Lezamaは、プログラム合成問題をブール論理でエンコードし、ブール充足可能性問題のアルゴリズムを使用してプログラムを自動的に見つけることが可能であることを示しました。^[5]

2013年、ペンシルベニア大学、カリフォルニア大学バークレー校、マサチューセッツ工科大学（ MIT）の研究者らによって、プログラム合成問題のための統一フレームワーク「構文誘導合成（Syntax-guided Synthesis、様式化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年まで、毎年開催されるSyntax-Guided Synthesis Competition（SyGuS-Comp）では、プログラム合成のさまざまなアルゴリズムを競うイベントが開催されました。^{[8]このコンテストでは、} SMT-Lib 2に基づく標準化された入力形式であるSyGuS-IFが使用されました。たとえば、次のSyGuS-IFは、2つの整数の最大値を求める問題をエンコードします（上記参照）。

(セットロジックLIA)
(シンセファン f ((x Int) (y Int)) Int
  ((i Int) (c Int) (b ブール値))
  ((i Int (cxy (+ ii) (ite bii)))
   (c 整数 (0 1))
   (b ブール値 ((<= ii)))))
(宣言変数 x Int)
(宣言変数 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、
    出力: spec を満たすプログラム、または失敗するプログラム

    inputs  := 空集合
    loop 
        candidate  := generate ( spec , inputs )
         if  verify ( spec , candidate ) then 
            return  candidate 
        else  verify反例 e を生成するe をinputsに
        追加
            するend if

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

CEGISは反例誘導抽象化改良（CEGAR）に触発された。 ^[11]

1980年に発表されたマンナとウォルディンガーのフレームワーク^{[12] [13]}は、ユーザーが指定した1階仕様式から始まります。その式に対して証明が構築され、それによって統一置換から関数型プログラムも合成されます。

フレームワークはテーブル レイアウトで表示され、列には次のものが含まれます。

• 参照用の行番号（「Nr」）
• すでに確立されている公式、公理や前提条件（「主張」）
• 事後条件を含む、まだ証明されていない公式（「目標」）^{[注 1]}
• 有効な出力値を表す用語（「プログラム」） ^{[注 2]}
• 現在の行の正当化（「Origin」）

最初に、背景知識、事前条件、事後条件がテーブルに入力されます。その後、適切な証明ルールが手動で適用されます。フレームワークは、中間式の可読性を高めるために設計されています。古典的な解決とは異なり、節正規形は不要ですが、任意の構造でジャンクタを含む式（「非節解決」）を使用して推論することができます。目標列、または同等のアサーション列でが導出されたときに証明は完了です。このアプローチによって取得されたプログラムは、から開始された仕様式を満たすことが保証されます。この意味で、それらは構築によって正しいです。 ^[14]条件、再帰、算術およびその他の演算子^[注3]で構成される、最小限でありながらチューリング完全な^[15]純粋に機能的なプログラミング言語のみがサポートされています。この枠組みの中で行われたケーススタディでは、例えば、除算、剰余、^[16]平方根、^[17]項の統一、^[18]リレーショナルデータベースクエリへの回答^[19]やいくつかのソートアルゴリズム[ ^{20 ]}を計算するアルゴリズムが合成されました。^[21]${\displaystyle {\it {true}}}$${\displaystyle {\it {偽}}}$

証明規則には次のものが含まれます。

• 非節解決（表を参照）。

例えば、行 55 は、51 のアサーション式と52 のアサーション式を解決して得られます。これらは両方とも、共通の部分式 を共有しています。解決子は、を で置き換えたの選言として形成され、 をで置き換えた となります。この解決子は、との連言から論理的に導かれます。より一般的には、と には、それぞれ との2 つの統一化可能な部分式のみが必要です。その場合、それらの解決子は、前と同様にとから形成されます。ここで、 はとの最も一般的な統一子です。この規則は、節 の解決を一般化します。^[22]${\displaystyle E}$${\displaystyle F}$${\displaystyle p}$${\displaystyle E}$${\displaystyle p}$${\displaystyle {\it {true}}}$${\displaystyle F}$${\displaystyle p}$${\displaystyle {\it {偽}}}$${\displaystyle E}$${\displaystyle F}$${\displaystyle E}$${\displaystyle F}$${\displaystyle p_{1}}$${\displaystyle p_{2}}$${\displaystyle E\theta }$${\displaystyle F\theta }$${\displaystyle \theta}$${\displaystyle p_{1}}$${\displaystyle p_{2}}$

親式のプログラム項は、行 58 に示すように結合され、解決子の出力を形成します。一般的なケースでは、は後者にも適用されます。出力にサブ式が表示されるため、計算可能なプロパティに対応するサブ式のみを解決するように注意する必要があります。${\displaystyle \theta}$${\displaystyle p}$

• 論理変換。

たとえば、 は、アサーションでもゴールでも )に変換できます。どちらも同等だからです。${\displaystyle E\land (F\lor G)}$${\displaystyle (E\land F)\lor (E\land G)}$

• 結合的アサーションと分離的目標の分割。

下のおもちゃの例の 11 行目から 13 行目に例が示されています。

• 構造誘導。

この規則により、再帰関数の合成が可能になります。与えられた事前条件と事後条件「となるようなが与えられた場合、となるような を見つける」と、のドメインの適切なユーザー指定の整列化に対して、アサーション「」を追加することは常に適切です。^[23]このアサーションで解決すると、プログラム項にへの再帰呼び出しが導入される可能性があります。${\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'))}$${\displaystyle f}$

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

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

簡単な例として、2 つの数値の最大値を計算する関数型プログラムは次のようにして導出できます。^{[引用が必要]}${\displaystyle M}$${\displaystyle x}$${\displaystyle y}$

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

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

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

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

となり、 true ∧ false ) ∧ ( x ≤ x ∧ y ≤ x ∧ trueとなり、これは次のように簡略化されます。 ${\displaystyle \lnot (}$${\displaystyle )}$${\displaystyle x\leq x\land y\leq x}$

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

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

• 帰納的プログラミング
• メタプログラミング
• プログラムの導出
• 自然言語プログラミング
• 反応合成

• David, Cristina; Kroening, Daniel (2017-10-13). 「プログラム合成：課題と機会」. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences . 375 (2104): 20150403. doi :10.1098/rsta.2015.0403. ISSN  1364-503X. PMC 5597726.  PMID 28871052  .
• Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018-11-20). 「検索ベースのプログラム合成」Communications of the ACM . 61 (12): 84–93. doi :10.1145/3208071. ISSN  0001-0782.
• Zohar Manna、Richard Waldinger (1975)。「プログラム合成における知識と推論」。人工知能。6 ( 2 ): 175–208。doi :10.1016/0004-3702(75)90008-9。
• Solar-Lezama, Armando (2008)。スケッチによるプログラム合成(PDF) (Ph.D.)。カリフォルニア大学バークレー校。