HN 日本語サマリー

← 一覧へ戻る
プログラミング

RustとZ3を用いたループフリープログラムの合成 (2020年)

Synthesizing Loop-Free Programs with Rust and Z3 (2020) (fitzgen.com)

16 pointsby karelpeeters0 コメント

要約

本記事は、プログラム合成、特にループフリーでコンポーネントベースのプログラムを合成する手法について解説しています。SMTソルバーZ3とRustを用いた実装例を通して、この技術のモチベーション、課題、および具体的なアプローチを説明しています。これにより、複雑なプログラムを自動生成する可能性と、そのための現代的な手法への理解を深めます。

全文翻訳

RustとZ3によるループフリープログラムの合成

仕様を満たすプログラムを自動的に見つけることをプログラム合成と呼びます。主な困難は、探索空間が非常に大きいことです。サイズ(n)のプログラムの数は指数関数的に増加します。サイズ(n)のプログラムをすべて列挙し、それぞれが仕様を満たすかチェックし、次にサイズ(n+1)のプログラムへと進むといった単純な方法はスケールしません。しかし、この分野は、よりスマートな探索技術を用いて探索空間を削減し、SMTソルバーのパフォーマンス向上を活用し、時には問題の範囲を限定することで進歩してきました。

この記事では、現代のプログラム合成の一アプローチである、反例導出型反復合成（counterexample-guided iterative synthesis）によるコンポーネントベースのループフリープログラムの合成について説明します。これは、GulwaniらによるSynthesis of Loop-Free Programsで説明されている手法です。これらの用語の意味を正確に解き明かし、Z3ソルバーを使用したRustによる実装も紹介します。

この記事の目的は二つあります：

  1. プログラム合成に馴染みのない方々（私もそうでした）が、このトピックについて少しでも詳しくなり、新しいことを学べるようにすることです。多くの例を提供し、論文の密な論理式を、より小さく、取り組みやすい断片に分解するように努めました。
  2. この種のプログラム合成に既に馴染みのある方々が、実装におけるパフォーマンスの問題を診断するのを手助けしてくれることを願っています。私は文献で報告されている合成結果を再現できていません。より難しいベンチマーク問題の一部では、私の忍耐力が尽きる前に、シンセサイザーは解を見つけることさえ失敗します。

目次

動機

なぜ自分でプログラムを書く代わりに、プログラムが他のプログラムを書くようにするのか？ 私が単に怠惰だからか？ もちろんです。しかし、私ほど怠惰でない人がプログラムを合成したいと思うには、多くの正当な理由があります。

一部のプログラムは手書きで正確に書くのが非常に難しく、プログラムシンセサイザーがあなたや私では失敗するところで成功するかもしれません。素早く！ 3つのビット操作命令だけを使って、単語の最も右にあるゼロビットを分離するにはどうすればよいですか？

              ,--- 最も右にあるゼロビット。
              |
              V
入力:  011010011

出力: 000000100
              ^
              |
              '--- そのビットだけがセットされている。

もうわかりましたか？

…

さて、答えはこちらです：

isolate_rightmost_zero_bit(x): // x = 011010011
    a ← not x                  // a = 100101100
    b ← add 1, x               // b = 011010100
    c ← and a, b               // c = 000000100
    return c

私たちのプログラムシンセサイザーは、1秒未満で一つの解を見つけ、それを最小長の解を1分程度で見つけます。私自身が手で同じことをするのには、それよりもかなり長い時間がかかるでしょう。この記事の残りの部分で、この問題に戻り、実行例として使用します。

プログラムシンセサイザーを使用するもう一つの理由は、手で書く時間よりもはるかに多くのプログラムを書く必要がある場合です。例えば、コンパイラのピーホールオプティマイザーを考えてみてください。これは、命令シーケンスのスライディングウィンドウを考慮し、各シーケンスについて、同等だがより高速または小さい命令シーケンスを知っているかどうかをチェックします。より良い命令シーケンスを知っている場合、元の命令をより良いものに置き換えます。

ピーホールオプティマイザーは通常、最適化されていない命令シーケンスと、マッチを置き換えるための改善された命令シーケンスをペアにするパターンマッチングルールから構築されます：

new PeepholeOptimizer(
    pattern0 → replacement0
    pattern1 → replacement1
    pattern2 → replacement2
    // ...
    patternn → replacementn
)

各 replacementi は、小さな最適化されたミニプログラムです。もし私たちがゼロから手書きで新しいピーホールオプティマイザーを書くとしたら、私たち自身で(n)個の最適化されたミニプログラムを書く必要があります。そして(n)は大きくなる可能性があります：LLVMのInstCombineピーホールオプティマイザーには、1,000以上のパターンと置換のペアがあります。その半数でも、私自身が書きたいと思う量よりはるかに多いです。

これらの最適化されたミニプログラムを手書きする代わりに、各元の命令シーケンスを仕様として使用し、プログラムシンセサイザーに渡し、シンセサイザーが同じことを行う最適な命令シーケンスを見つけられるかどうかを確認できます。最後に、これらの元の命令シーケンスとそれらの合成された最適な命令シーケンスをすべてパターンと置換のペアとして使用して、ピーホールオプティマイザーを自動的に構築できます！このアイデアは、BansalらによってAutomatic Generation of Peephole Superoptimizersで最初に提案されました。

*編集: John Regehr氏が、このアイデアはBansalらの論文が発表された2006年よりもずっと以前から存在していたことを指摘してくれました。彼は、1980年のThe Design and Application of a Retargetable Peephole Optimizer by Davidson et alを例として挙げましたが、これも初めてのことではなかったと述べています。

私たちのタスクの概要

プログラム合成とは、仕様を取り込み、それに対応するプログラムを自動的に見つける行為です。問題を少し扱いやすくするために、二つの方法でその範囲を限定しています：

  1. ループフリー: ループのないプログラムのみを合成します。
  2. コンポーネントベース: 与えられたコンポーネントライブラリの構成として表現できるプログラムのみを合成します。

ループフリーという制限は、多くのユースケースではそれほど制限になりません。例えば、ピーホールオプティマイザーは、ループ境界をまたぐ命令シーケンスを考慮しないことがよくあります。

コンポーネントベース合成とは、シンセサイザーがターゲット言語の任意の式の任意の組み合わせを使用するのではなく、コンポーネントのライブラリを与えられ、それらの各コンポーネントをちょうど一度だけ使用するプログラムを合成することを意味します。シンセサイザーは、仕様を満たす構成を見つけるまで、コンポーネントを並べ替え、その入力と出線を再配線します。

つまり、(N)個のコンポーネントのライブラリが与えられた場合、次のような形式のプログラムを構築します。

synthesized_program(inputs...):
    temp0 ← component0(params0...)
    temp1 ← component1(params1...)
    // ...
    tempN-1 ← componentN-1(paramsN-1...)
    return tempN-1

ここで、paramsi の各パラメータは、プログラムの早い段階で定義された tempj 変数か、元の inputs のいずれかです。

例えば、二つのコンポーネント

  • f(a)
  • g(a, b)

と入力パラメータ x が与えられた場合、シンセサイザーは次の候補プログラムのいずれかを構築できます（暗黙的に最後に定義された変数を返します）：

a ← g(x, x)
b ← f(x)

または

a ← g(x, x)
b ← f(a)

または

a ← f(x)
b ← g(x, x)

または

a ← f(x)
b ← g(a, x)

または

a ← f(x)
b ← g(x, a)

または

a ← f(x)
b ← g(a, a)

これだけです。これらは、その二つのコンポーネントだけを与えられた場合に構築できるすべてのプログラムです。

シンセサイザーは、次のプログラムを構築できません。なぜなら、それはすべてのコンポーネントを使用しないからです：

a ← f(x)

そして、シンセサイザーは次のプログラムを構築できません。なぜなら、それは f コンポーネントを複数回使用しているからです：

a ← f(x)
b ← f(a)
c ← g(b, b)

そして最後に、次のプログラムを構築できません。なぜなら、この最後のプログラムは、私たちのライブラリにコンポーネントとして含まれていない h という関数を使用しているからです：

a ← f(x)
b ← h(a, x)

次の表は、コンポーネントベース合成の特性を、完全に一般的なプログラム合成と比較して説明しています：

一般的な合成コンポーネントベース合成
合成されるプログラムの形状ターゲット言語の任意の式の任意の数を使用ライブラリのコンポーネントのみを使用
合成されるプログラムのサイズ可変ライブラリのサイズと全く同じ。なぜなら、ライブラリの各コンポーネントはちょうど一度だけ使用されるから

私たちのシンセサイザーでは、コンポーネントは固定ビット幅整数（SMTソルバーの専門用語では「ビットベクトル」とも呼ばれます）上の関数となり、仮想命令セットの単一命令に対応します：add、and、xor など。しかし、原理的には、より高レベルの関数や、SMTクエリでエンコードできるものでも構いません。SMTクエリについては後述します。

コンポーネントベース合成は合成問題を容易にしますが、シンセサイザーを呼び出すたびに、コンポーネントのライブラリを選択するという決定を私たちに強います。各コンポーネントは合成プログラムでちょうど一度だけ使用されますが、複数の加算を実行するプログラムを合成したい場合は、ライブラリに add コンポーネントの複数のインスタンスを含めることができます。コンポーネントが少なすぎると、シンセサイザーは解を見つけられない可能性があります。コンポーネントが多すぎると、シンセサイザーが遅くなり、デッドコードを含む非最適化プログラムを生成する可能性があります。

要約すると、ループフリーコンポーネントベース合成では、シンセサイザーの入力は次のようになります。

  • 仕様、および

  • コンポーネントのライブラリ。

その出力は、指定されたコンポーネントで表現された、仕様を満たすプログラム、またはそのようなプログラムを見つけられない場合はエラーです。

問題の形式化

プログラムを合成するには、望ましいプログラムの動作を記述する仕様が必要です。仕様は、プログラムがこれらの入力で与えられたときの出力を記述する論理式です。

仕様を次のように定義します：

  • (\vec{I}) をプログラム入力、

  • (O) をプログラム出力、

  • (\phi_\mathrm{spec}(\vec{I}, O)) を入力と出力の関係を表す式とします。この式は、(O) が入力 (\vec{I}) に対するプログラムの望ましい出力である場合に真であるべきです。

与えられたコンポーネントのライブラリは、各コンポーネントの動作を記述する仕様のマルチセットです。各コンポーネント仕様には、入力の数（例：add(a, b) コンポーネントは2つの入力を取り、not(a) コンポーネントは1つの入力を取る）と、コンポーネントの入力とその出力の関係を表す論理式が含まれています。コンポーネントの入力、出力、および式はすべて、プログラム仕様と同様の表記法ですが、添え字が付いています：

  • (\vec{I}_i) は (i^\mathrm{th}) コンポーネントの入力変数、

  • (O)_i は (i^\mathrm{th}) コンポーネントの出力変数、

  • (\phi)_i(\vec{I}_i, O)_i は (i^\mathrm{th}) コンポーネントの入力とその出力を関係付ける論理式です。

ライブラリ内のコンポーネントの数を (N) と定義します。

右端のゼロビットを分離する例について、望ましい解を見つける能力を維持しながら、シンセサイザーに与えることができる最小のコンポーネントライブラリは何でしょうか？ それは、解プログラムの3つの命令それぞれに対応するコンポーネントのみで構成されるライブラリになります：not、add1、およびandコンポーネント。

コンポーネント定義説明
( \phi)_0(I)_0, O)_0 )( O)_0 = \texttt{bvadd}(1, I)_0 )ビットベクトル上の加算1操作。
( \phi)_1(I)_1, I)_2, O)_1 )( O)_1 = \texttt{bvand}(I)_1, I)_2 )ビットごとのAND操作。
( \phi)_2(I)_3, O)_2 )( O)_0 = \texttt{bvnot}(I)_3 )ビットごとのNOT操作。

プログラム合成は存在-全称問題として表現できます。つまり、仕様を満たすプログラム (P) が存在するかどうかを見つけたいのです。これは、すべての入力に対して仕様を満たすプログラム (P) が存在するかどうかを問うものです。

( \begin{align} & \exists P: \ & \quad \forall \vec{I},O: \ & \quad \quad P(\vec{I}) = O \implies \phi_\mathrm{spec}(\vec{I}, O) \end{align} )

これを分解して英語に翻訳しましょう：

( \exists P )プログラム (P) が存在し、
( \forall \vec{I},O )すべての入力 (\vec{I}) と出力 (O) に対して、
( P(\vec{I}) = O )プログラムを (\vec{I}) で実行して出力 (O) を得ると、
( \implies )その場合
( \phi_\mathrm{spec}(\vec{I}, O) )私たちの仕様 (\phi_\mathrm{spec}) が満たされる。

この存在-全称形式化は、最終的な実装が（Z3である）SMTソルバーにほぼこの公式をクエリすることになるため、理解することが重要です。それは正確に同じではありません：

  • (P) はコンポーネントに関するいくつかの詳細を隠している抽象化です。
  • いくつかの代数変換を実行します。
  • 問題全体を一度に単一のクエリとしてソルバーに提示しません。

それでも、実装はこの形式化から派生しており、この形式化を理解せずに進むことはできません。

SMTソルバーの簡単な紹介

SMTソルバーとそれらの機能について簡単に説明せずに、これ以上進むことはできません。Z3のようなSMTソルバーは、論理式（未束縛変数を含む可能性がある）を取り込み、それが次のいずれであるかを返します：

  • 充足可能: 未束縛変数への代入が存在し、表明を真にする。また、それらの代入を記述するモデルも提供される。

  • 充足不能: 式の表明は偽である。それらを真にできる未束縛変数への値の代入は存在しない。

SMTソルバーは、SMT-LIB2と呼ばれるLisp風の入力言語で表明を受け取ります。以下は、充足可能なSMTクエリの例です：

;; `x` は何らかの整数ですが、どれかはわかりません。
(declare-const Int x)

;; しかし、`x + 2 = 5` であることはわかっています。
(assert (= 5 (+ x 2)))

;; 主張が充足可能かどうかを確認します。
;; この場合、そうなるはずです！
(check-sat)

;; モデルを取得します。これには、自由変数に対する代入が含まれています。
;; モデルは `x` が `3` であると報告するはずです！
(get-model)

オンラインZ3エディタでこのスニペットを開いて実行！

そこには (\exists) 存在量化子はありませんが、ソルバーは暗黙的に (\exists x: x + 2 = 5) の (x) の解を見つけています。つまり、(x + 2) が5に等しくなるような (x) が存在します。一部のSMTソルバーは、明示的な (\exists) 存在量化子と (\forall) 全称量化子がネストされた高階論理式を扱うためのいくつかのサポートを持っていますが、これらのモードは通常はるかに遅く、また不完全です。私たちは、第一階の、暗黙的に (\exists) 存在する量化子クエリにのみ依存できます。つまり、未束縛変数を含む可能性のある式で、ネストされた (\exists) 存在量化子や (\forall) 全称量化子を含まない式です。

例に二番目の主張を追加すると、充足不能になります：

(declare-const x Int)

(assert (= 5 (+ x 2)))

;; NEW: また、x + 1 は 10 であるべきです。
(assert (= 10 (+ x 1)))

;; 今回は、`x` に対する競合する要件があるため、充足不能になるはずです。
(check-sat)
(get-model)

オンラインZ3エディタでこのスニペットを開いて実行！

主張 10 = x + 1 と 5 = x + 2 は x に競合する要件を課すため、両方の主張を真にできる x の値は存在せず、したがってクエリ全体が充足不能になります。

反例導出型反復合成

反例導出型反復合成（CEGIS）は、第二階の存在-全称クエリ（私たちのプログラム合成問題のようなもの）を、市販のSMTソルバーで解決することを可能にします。CEGISは、これらの難しいクエリを複数の第一階の、(\exists) 存在する量化子クエリに分解することでこれを実現します。これらは、市販のSMTソルバーが得意とする種類のクエリです。まず、一般的なCEGISを見て、その後、コンポーネントベースCEGISに具体的に何が必要かを見ていきます。

CEGISは、初期の有限個の入力セットを選択することから始まります。少なくとも一つは必要ですが、それがどこから来たかは実際には関係ありません。乱数ジェネレータを使用できます。その後、ループを開始します。ループの最初のステップは有限合成であり、これは少なくとも入力セット内の入力に対して正しいプログラムを生成します。すべての入力に対して正しい場合もあれば、そうでない場合もありますが、それはまだわかりません。次に、その候補プログラムを取り、それを検証します。すべての入力に対して正しいかどうか（その場合は完了）、または候補プログラムが間違っている入力が存在するかどうか（反例と呼ばれる）を判断したいのです。反例が存在する場合、それをセットに追加し、ループの次の反復に進みます。有限合成が次に生成するプログラムは、すべての古い入力、およびこの新しい反例に対しても正しいものになります。反例は、より多くの入力に対して正しい、より一般的なプログラムを生成するように有限合成を強制し、最終的にすべての入力に対して機能する完全に一般的なプログラムを生成します。

前置きはこれくらいにして、一般的なCEGISアルゴリズムを以下に示します：

(\begin{align} & \texttt{CEGIS}(\phi_\mathrm{spec}(\vec{I}, O)): \ & \qquad S = \langle \text{初期有限入力} \rangle \ & \qquad \ & \qquad \textbf{loop}: \ & \qquad \qquad \texttt{// 有限合成。}\ & \qquad \qquad \textbf{for $P$ in } \exists P,O_0,\ldots,O extbackslash_{\lvert S \rvert - 1}: \ & \qquad \qquad \qquad \left( P(S_0) = O_0 \land \phi_\mathrm{spec}(S_0, O_0) \right) \ & \qquad \qquad \qquad \land \ldots \ & \qquad \qquad \qquad \land \left( P(S extbackslash_{\lvert S \rvert - 1}) = O extbackslash_{\lvert S \rvert - 1} \land \phi_\mathrm{spec}(S extbackslash_{\lvert S \rvert - 1}, O extbackslash_{\lvert S \rvert - 1}) \right) \ & \qquad \qquad \textbf{if } \texttt{unsat}: \ & \qquad \qquad \qquad \textbf{error} \text{ “no solution”} \ & \qquad \qquad \ & \qquad \qquad \texttt{// 検証。}\ & \qquad \qquad \textbf{solve for $\vec{I}$ in } \exists \vec{I},O: ,, P(\vec{I}) = O \land \lnot \phi_\mathrm{spec}(\vec{I}, O) \ & \qquad \qquad \textbf{if } \texttt{unsat}: \ & \qquad \qquad \qquad \textbf{return $P$} \ & \qquad \qquad \textbf{else}: \ & \qquad \qquad \qquad \textbf{append $\vec{I}$ to $S$} \ & \qquad \qquad \qquad \textbf{continue} \end{align})

CEGISは、存在-全称合成問題を二つの部分に分解します：

  1. 有限合成: 最初 のクエリ、有限合成クエリは、少なくとも有限の例入力 (S) に対して正しいプログラムを見つけます。その内訳は次のとおりです：

    ( \exists P,O_0,\ldots,O extbackslash_{\lvert S \rvert - 1}: )プログラム (P) と出力 (O_0,\ldots,O extbackslash_{\lvert S \rvert - 1}) が存在し、
    ( ( ,, P(S_0) = O_0 )(O_0) は (S_0) の入力に対するプログラムの出力であり
    ( \land )かつ
    ( \phi_\mathrm{spec}(S_0, O_0) ,, ) )(S_0) の入力と出力 (O_0) に対して仕様が満たされる、
    ( \land \ldots )かつ…
    ( \land \left( P(S extbackslash_{\lvert S \rvert - 1}) = O extbackslash_{\lvert S \rvert - 1} \land \phi_\mathrm{spec}(S extbackslash_{\lvert S \rvert - 1}, O extbackslash_{\lvert S \rvert - 1}) \right) )(O extbackslash_{\lvert S \rvert - 1}) は (S extbackslash_{\lvert S \rvert - 1}) の入力に対するプログラムの出力であり、仕様がこれらの入力と出力に対して満たされる。

    注意：これは第一階の、存在する量化子クエリであり、ネストされた (\forall) 全称量化子をすべての可能な入力に対して使用していません！代わりに、有限セット (S) の各例に対して、(P(S_i) = O_i \land \phi_\mathrm{spec}(S_i, O_i)) の新しいコピーをインスタンス化します。

    例えば、(S = \langle 3, 4, 7 \rangle) の場合、有限合成クエリは次のようになります：

    (\begin{align} & \exists P,O_0,O_1,O_2: \ & \qquad \left( P(3) = O_0 \land \phi_\mathrm{spec}(3, O_0) \right) \ & \qquad \land ,, \left( P(4) = O_1 \land \phi_\mathrm{spec}(4, O_1) \right) \ & \qquad \land ,, \left( P(7) = O_2 \land \phi_\mathrm{spec}(7, O_2) \right) \ \end{align})

    このインライン展開は、有限入力セット (S) が実際には（通常は数十程度、多くてもそれ以下）すべての可能な入力セットのサイズ（例えば、32ビット幅のビットベクトルは (2^{32}) 個ある）よりもはるかに小さいからです。

    クエリが充足不能だった場合、(S) のすべての入力に対して仕様を実装できるプログラムは存在しません。(S) はすべての入力のサブセットであるため、すべての入力に対して仕様を実装できるプログラムは存在しないことを意味します。そして、それが私たちが探しているものであるため、検索が失敗したことを意味し、エラーを返します。

    クエリが充足可能だった場合、結果のプログラム (P) は (S) のすべての入力に対して仕様を満たしますが、それがすべての可能な入力に対して仕様を満たすかどうかはまだわかりません。例えば、(S = \langle 0, 4 \rangle ) の場合、プログラム (P) は入力 (0) と (4) が与えられたときに正しいことがわかりますが、入力 (1) が与えられたときに正しいかどうかはわかりません。まだわかりません。

  2. 検証: 検証は、有限合成によって生成されたプログラム (P) を取り、それがすべての入力に対して仕様を満たすかどうかをチェックします。これは自然に全称量化子クエリとして表現されますが、ド・モルガンの法則のおかげで、仕様が満たされない入力が存在するかどうかを問うことができます。

    検証クエリの内訳は次のとおりです：

    ( \exists \vec{I}, O: )仕様が満たされない入力 (\vec{I}) と出力 (O) が存在するか？
    ( P(\vec{I}) = O)(O) は (\vec{I}) に対するプログラムの実行結果である
    ( \land )かつ
    ( \lnot \phi_\mathrm{spec}(\vec{I}, O) )仕様が満たされない。

    検証クエリが充足不能だった場合、(P) に仕様が満たされない入力は存在しないことを意味し、(P) がすべての入力に対して仕様を満たすことを意味します。その場合、これが私たちが探しているものであり、見つけたので、それを返します！

    しかし、検証クエリが充足可能だった場合、反例を発見したことになります。つまり、プログラムが仕様を満たさない新しい入力 (\vec{I}) です。つまり、プログラム (P) は (\vec{I}) が与えられたときにバグがあるので、(P) は私たちが探しているプログラムではありません。

    次に、新しい (\vec{I}) を有限セット (S) に追加します。これにより、ループの次の反復で、(S) の他のすべての入力に加えて、(I) が与えられたときに正しい結果を生成するプログラムを合成します。

ループが繰り返されるにつれて、(S) にさらに多くの入力が追加され、有限合成クエリがますます一般的なプログラムを生成するように強制されます。最終的に、すべての入力に対して仕様を満たす完全に一般的なプログラムが生成されます。最悪の場合、すべての可能な入力を (S) に追加することになります。有限合成は、1が与えられたときに失敗するプログラムを生成し、次に2が与えられたとき、次に3が与えられたとき、というようになります。実際には、検証が見つける各反例 (\vec{I}) は、(P) によってまだ処理されていない多くの他の入力の代表である傾向があります。(\vec{I}) を (S) に追加することにより、有限合成の次の反復は、(\vec{I}) だけでなく、(\vec{I}) が代表していた他のすべての入力に対しても機能するプログラムを生成します。例えば、有限合成は (S = \langle 0,1,5,13 \rangle) のすべての入力に対して機能するプログラムを生成したかもしれませんが、正の偶数が与えられたときにバグがあるかもしれません。検証は反例 (I = 2) を見つけ、それは (S) に追加され、(S = \langle 0,1,5,13,2 \rangle) となります。次に、ループの次の反復は、2だけでなく、すべての正の偶数に対して機能するプログラムを合成します。これがCEGISを実際には効果的にしている理由です。

最後に、有限合成と検証の両方が第一階の、(\exists) 存在する量化子クエリであり、Z3のような市販のSMTソルバーが解決できることに注意してください。

コンポーネントを用いたCEGIS

CEGISが抽象的にどのように機能するかを知ったところで、コンポーネントベースのプログラムを合成するためにそれを使用する方法を詳しく見ていきましょう。

コンポーネントの構成からなるループフリープログラムごとに、プログラムの表現を位置マッピングに反転させることができます：

  • プログラムを行ごとにリストアップし、各行にどのコンポーネントが配置されるかを定義する代わりに、コンポーネントをリストアップし、コンポーネントが配置される行を定義できます。

  • 各コンポーネントの引数を変数名で参照する代わりに、引数が定義されている行（前のコンポーネントの結果から来る場合）または(n^\mathrm{th}) プログラム入力として参照できます。

例えば、単語の最も右にあるゼロビットを分離するプログラムを考えてみましょう：

isolate_rightmost_zero_bit(x):
    a ← not x
    b ← add 1, x
    c ← and a, b
    return c

このプログラムを次の位置マッピングで正確に表現できます：

{
    inputs: ["x"],

    components: {
        // Line 1: `b ← add 1, x`
        add1: {
            // このコンポーネントが配置されるプログラム内の行。
            line: 1,

            // 各エントリ `a` は、引数がどこから来るかを表します。
            //
            // If `0 <= a < inputs.len()`, then the
            // argument is `inputs[a]`.
            //
            // Otherwise, when `inputs.len() <= a`,
            // then the argument comes from the value
            // defined by the component on line
            /// `a - inputs.len()`.
            arguments: [
                // `x`
                0,
            ],
        },

        // Line 2: `c ← and a, b`
        and: {
            line: 2,
            arguments: [
                // `a`
                1,
                // `b`
                2,
            ],
        },

        // Line 0: `a ← not x`
        not: {
            line: 0,
            arguments: [
                // `x`
                0,
            ],
        },
    },
}

コンポーネントベースCEGISでは、この種の位置マッピングを合成します。これにより、プログラムの行番号と引数インデックスの数個の数値で、コンポーネントベースのプログラム全体を表現できます。そして、数値はSMTクエリに直接表現できるものです。

コンポーネントベースプログラムの検証

抽象的なCEGISの仕組みを理解したので、次にコンポーネントベースのCEGISに飛び込みます。検証は、位置マッピングを受け取り、位置マッピングによって記述されたとおりにコンポーネントの入力と出力変数を接続し、反例を見つけるようにSMTソルバーに要求します。

便宜上、(\vec{I}_0,\ldots,\vec{I}_{N-1}) を繰り返し繰り返す必要がないように、(\textbf{P}) をライブラリの各コンポーネントのすべてのパラメータ変数のセットとして定義します：

( \textbf{P} = , \vec{I}_0 , \cup , \ldots , \cup , \vec{I}_{N-1} )

同様に、(\textbf{R}) をライブラリの各コンポーネントのすべてのテンポラリ結果変数のセットとして定義します：

( \textbf{R} = {O_0, , \ldots, , O extbackslash_{{N-1}} }

右端のゼロビットを分離する例で、最小ライブラリは次のものから構成されます：

( \begin{align} \phi_0(I)_0, O)_0 ) &= ( \left[ O)_0 = \texttt{bvadd}(1, I)_0 \right] \ \phi_1(I)_1, I)_2, O)_1 ) &= ( \left[ O)_1 = \texttt{bvand}(I)_1, I)_2 \right] \ \phi_2(I)_3, O)_2 ) &= ( \left[ O)_2 = \texttt{bvnot}(I)_3 \right] \end{align} )

したがって、その：

( \begin{align} N &= 3 \ \textbf{P} &= { I)_0, I)_1, I)_2, I)_3, I)_4 \ \textbf{R} &= { O)_0, O)_1, O)_2 \end{align} )

ライブラリ全体が個々のコンポーネント仕様に従って動作するように制約したいのです。各 and コンポーネントの出力は、その入力のビットごとのandであるべきであり、各 not コンポーネントの出力は、その入力のビットごとのnotであるべきです… (\phi_\mathrm{lib}) を、各コンポーネント仕様 (\phi)_i の組み合わせとして定義します：

( \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) = \phi)_i(\vec{I}_0, O)_0) \land \ldots \land \phi)i(\vec{I}_{N-1}, O extbackslash{{N-1}} )

したがって、最小例ライブラリでは、(\phi_\mathrm{lib}) は次のようになります：

( \begin{align} \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) &= \left[ O)_0 = \texttt{bvadd}(1, I)_0 \right] \ &\land \left[ O)_1 = \texttt{bvand}(I)_1, I)_2 \right] \ &\land \left[ O)_2 = \texttt{bvnot}(I)_3 \right] \end{align} )

つまり、ライブラリの制約は、次のすべてが満たされるときに満たされます：

  • (O)_0 は (I)_0 と 1 のラップアラウンド加算である、
  • (O)_1 は (I)_1 と (I)_2 のビットごとのandである、そして
  • (O)_2 は (I)_3 のビットごとのnotである、

有限合成が検証の前に実行されるため、検証クエリを構築する際に候補プログラムの位置マッピングに既にアクセスできます。この位置マッピングは、どの実際の引数がコンポーネントのどの形式パラメータに一致するかを示します。つまり、各コンポーネントの入力変数からプログラム入力および他のコンポーネントの一時結果変数への接続がわかります。コンポーネント間のデータフローがわかります。

これを右端のゼロビットを分離する例で具体的に見てみましょう。この候補プログラムを生成した後：

a ← not x
b ← add 1, x
c ← and a, b

このライブラリで：

( \begin{align} \phi_0(I)_0, O)_0 ) &= ( \left[ O)_0 = \texttt{bvadd}(1, I)_0 \right] \ \phi_1(I)_1, I)_2, O)_1 ) &= ( \left[ O)_1 = \texttt{bvand}(I)_1, I)_2 \right] \ \phi_2(I)_3, O)_2 ) &= ( \left[ O)_2 = \texttt{bvnot}(I)_3 \right] \end{align} )

a は not コンポーネント (\phi)_2(I)_3, O)_2) の結果であるため、(\texttt{a} = O)_2) であることがわかります。そして、a が and a, b の最初の引数であり、これはコンポーネント (\phi)_1(I)_1, I)_2, O)_1) を使用するため、(\texttt{a} = I)_1) であることがわかります。したがって、(O)_2 = I)_1) であることがわかります。

各コンポーネント入力変数 (I)_i \in \textbf{P}) から、他のコンポーネントの出力変数 (O)_j \in \textbf{R}) またはプログラム入力 (\vec{I}) のいずれかへのこれらの等価性があります。これらの等価性は、検証クエリの構築時に、候補プログラムの位置マッピングから直接提供されます。これらは、コンポーネント間のすべての接続を表します。

さらに、候補プログラムは暗黙的に最後のテンポラリ変数 c を返しており、これは and コンポーネント (\phi)_1(I)_1, I)_2, O)_1) の結果であり、(\phi_\mathrm{spec}(\vec{I}, O)) の (O) はプログラム全体の最終結果を表すため、(O = O)_1) であることがわかります。

これらのすべての等価性を例プログラムにまとめると、次のようになります：

( \left( I)_0 = x \right) \land \left( I)_1 = O)_2 \right) \land \left( I)_2 = O)_1 \right) \land \left( I)_3 = x \right) \land \left( O = O)_1 \right))

これは、ライブラリのさまざまなコンポーネントと候補プログラムの入力および出力との間のすべての接続を表します。コンポーネントを回路のように接続することを想像すると、これは各コンポーネント間のすべての配線を表します。

これらのコンポーネント接続等価性を (\phi_\mathrm{conn}) と定義し、その一般的な定義は次のとおりです：

( \begin{align} \phi_\mathrm{conn}(\vec{I}, O, \textbf{P}, \textbf{R}) &= \left( O = O_\mathrm{last} \right) \ & \land \left( \vec{I}_0 , = , \vec{V}_0 \right) \ & \land , \ldots \ & \land \left( \vec{I}_{N-1} , = , \vec{V}_{N-1} \right) \end{align} )

ここで：

  • (\vec{V}_i) は、候補プログラムが (i^\mathrm{th}) コンポーネント (\phi)_i に渡す実際の引数です。各 (\vec{V}_i) は、プログラム入力 (\vec{I}) または (\textbf{R}) のテンポラリ結果（前のコンポーネントによって定義される）のいずれかからのエントリで構成されます。これは、例の位置マッピングの components マップで定義された arguments フィールドと同等です。

  • (O_\mathrm{last}) は、候補プログラムの位置マッピングによると、プログラムの最後の行にあるコンポーネントの出力変数です。

もう一度分解してみましょう：

( \left( O = O_\mathrm{last} \right) )プログラム全体の出力は、プログラムの最後の行にあるコンポーネントの結果と等しい、
( \land )かつ
( \left( \vec{I}_0 , = , \vec{V}_0 \right) )最初のコンポーネントの入力とその割り当てられた引数は互いに等しい、
( \land , \ldots )かつ…
( \left( \vec{I}_{N-1} , = , \vec{V}_{N-1} \right) )最後のコンポーネントの入力とその割り当てられた引数は互いに等しい。

(O_\mathrm{last}) と各 (\vec{V}_i) は、候補プログラムの位置マッピングのプロパティであり、検証クエリの「コンパイル時」に知られています。これらは、クエリ自体で (\exists) 存在する量化または (\forall) 全称量化されている変数ではありません。検証クエリを構築する際に、これらをインラインで展開します。

さて、それらすべてを終えたので、コンポーネントベースCEGISで使用する検証制約を最終的に定義できます：

( \begin{align} & \exists \vec{I}, O, \textbf{P} , \textbf{R} : \ & \qquad \phi_\mathrm{conn}(\vec{I}, O, \textbf{P}, \textbf{R}) \land \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) \land \lnot \phi_\mathrm{spec}(\vec{I}, O) \end{align} )

検証制約は、次のように尋ねます：候補プログラムの位置マッピングによってコンポーネントが接続されていると仮定して、仕様が満たされない入力が存在しますか？

もう一度分解してみましょう：

( \exists \vec{I}, O, \textbf{P} , \textbf{R} : )入力と出力が存在し、
(\phi_\mathrm{conn}(\vec{I}, O, \textbf{P}, \textbf{R}) )候補プログラムの位置マッピングによって記述されたとおりにコンポーネントが接続され、
( \land ,, \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) )ライブラリによって記述されたとおりにコンポーネントが動作するとき、
( \land ,, \lnot \phi_\mathrm{spec}(\vec{I}, O) )仕様が満たされない？

このクエリの解を見つけることは、(S) の例入力セットに追加できる新しい反例 (\vec{I}) を提供します。このクエリの解を見つけるのに失敗した場合は、候補位置マッピングがすべての入力に対して正しいプログラムに対応することを意味し、その場合は完了です。

コンポーネントベースプログラムの有限合成

有限合成は、与えられた例入力すべてを正しく処理するプログラムを生成するために、ライブラリコンポーネントを構成します。これは、プログラム内の行へのコンポーネントの割り当て、および各コンポーネントの実際の引数への変数の割り当てを求めるSMTソルバーにクエリすることで行います。

例の位置マッピングを思い出してください：

{
    inputs: ["x"],

    components: {
        // Line 0: `a ← add 1, x`
        add1: {
            line: 0,
            arguments: [0], // `[x]`
        },

        // Line 1: `b ← and a, b`
        and: {
            line: 1,
            arguments: [1, 2], // `[a, b]`
        },

        // Line 2: `c ← not x`
        not: {
            line: 2,
            arguments: [0], // `[x]`
        },
    },
}

有限合成クエリに位置マッピングをエンコードするために、(\textbf{P}) のすべてのコンポーネントパラメータと (\textbf{R}) のすべてのコンポーネント結果には、関連付けられた位置変数が割り当てられます。有限合成クエリは、これらの位置変数の代入を検索しています。

すべての位置変数のセットを (L) と呼び、特定の位置変数を (l)_x と呼びます。ここで (x) はコンポーネント結果 (\textbf{R}) またはコンポーネントパラメータ (\textbf{P}) のいずれかです：

( L = { , l)_x , \vert , x \in \textbf{P} \cup \textbf{R} , } )

結果 (l extbackslash_{O)_i}) の位置変数は、例の位置マッピングの line フィールドに相当します。これは、コンポーネントがプログラムのどの行に割り当てられるかを決定し、したがって一時結果が定義される場所を決定します。

パラメータ (l)_p の位置変数は、例の位置マッピングの arguments リストのエントリに相当します。これらの位置変数は、関連付けられたパラメータが値を取得する場所を決定します。それはプログラム入力か、またはプログラムの (j^\mathrm{th}) 行で定義された一時結果です。

行番号とプログラム入力の両方に単一のインデックス空間を使用するために、例の位置マッピングの arguments リストのエントリと同じ規則に従います：

  • (l)_x がプログラム入力の数より小さい場合、それは ({l)_x}^\mathrm{th}) プログラム入力を参照します。

  • それ以外の場合、(l)_x がプログラム入力の数以上の場合、プログラム入力の数を (l)_x から引いて行番号を取得します。

(l)_x の値場所を参照
0入力 0
プログラム入力 (\vec{I})1
......
( \lvert \vec{I} \rvert - 1 )入力 ( \lvert \vec{I} \rvert - 1 )
(\lvert \vec{I} \rvert + 0)行 0
行番号(\lvert \vec{I} \rvert + 1)
......
(\lvert \vec{I} \rvert + N - 1)行 (N - 1)

すべてのループフリー、コンポーネントベースプログラムは、位置マッピングで記述できます。しかし、逆は真ではありません。すべての位置マッピングが有効なプログラムを記述するわけではありません。

この位置マッピングを考えてみましょう：

{
    inputs: ["x"],

    components: {
        // Line 0: `a ← add x, 1`
        add1: {
            line: 0,
            arguments: [0], // `[x]`
        },

        // Line 0: `a ← sub x, 1`
        sub1: {
            line: 0,
            arguments: [0], // `[x]`
        }
    }
}

この行マッピングは一貫性がありません。なぜなら、両方のコンポーネントをプログラムの行ゼロに配置したいからです。しかし、プログラムの各行は単一のコンポーネントしか使用できません。

ソルバーがこのような誤った回答を提供しないようにするために、一貫性制約 (\psi_\mathrm{cons}) を有限合成クエリに追加します。これは、二つの異なるコンポーネント結果位置変数が同じ行に割り当てられないことを要求します。

( \psi_\mathrm{cons}(L) = \bigwedge\limits extbackslash_{x,y \in \textbf{R}, x \not\equiv y} \left( l)_x \neq l)_y \right) )

もう一度分解してみましょう：

( \bigwedge\limits extbackslash_{x,y \in \textbf{R}, x \not\equiv y} )各 (x,y) のコンポーネント結果のペアについて、(x) と (y) が同じ結果変数でない場合、
( \left( l)_x \neq l)_y \right)(x) の位置と (y) の位置は同じではありません。

しかし、位置マッピングが不正なプログラムを記述する可能性はさらにあります！この位置マッピングを考えてみましょう：

{
    inputs: ["x"],

    components: {
        // Line 0: `a ← and x, b`
        and: {
            line: 0,
            arguments: [0, 2], // `[x, b]`
        },

        // Line 1: `b ← sub a, 1`
        sub1: {
            line: 1,
            arguments: [1], // `[a]`
        }
    }
}

その位置マッピングは次のプログラムを記述します：

f(x):
    a ← and x, b
    b ← sub a, 1

テンポラリ結果 b は定義される前に使用され、b を計算するには a を計算する必要がありますが、a を計算するには b を計算する必要があり、b を計算するには a を計算する必要があり、等々… 循環が発生しています。

データフローサイクルを持つ不正なプログラムに対応するマッピングを禁止するために、非循環制約 (\psi_\mathrm{acyc}) を使用します。この制約は、合成された位置マッピングがデータフローサイクルを持たないことを強制します。

( \psi_\mathrm{acyc}(L) = \bigwedge\limits extbackslash_{i=0}^{N-1} \left( \bigwedge\limits extbackslash_{p \in \vec{I}_i} \left( l)p < l extbackslash{O)_i} \right) \right) )

これを分解してみましょう：

( \bigwedge\limits extbackslash_{i=0}^{N-1} )各コンポーネントインデックス (i) について、
( \bigwedge\limits extbackslash_{p \in \vec{I}_i} )および (i^\mathrm{th}) コンポーネントの入力パラメータのそれぞれについて、
( l)p < l extbackslash{O)_i} )パラメータの位置はコンポーネントの位置よりも小さくなければなりません。つまり、パラメータは使用される前に定義されていることを意味します。

位置マッピングが無効になる唯一の方法は、位置がプログラム入力と行番号の範囲外にある場合です。したがって、ウェルフォームプログラム制約 (\psi_\mathrm{wfp}) を定義する準備ができました。この制約は、合成する任意の位置マッピングがウェルフォームプログラムに対応することを強制します。

ウェルフォームプログラムとは：

  • 一貫性がある、
  • 非循環である、
  • そのコンポーネントパラメータの位置は、プログラム入力または行番号を指す、そして
  • そのコンポーネント一時結果の位置は、行番号を指す。

プログラム入力の数とライブラリのコンポーネントの数の合計を (M) と定義します：

( M = \lvert \vec{I} \rvert + N )

コンポーネントパラメータの位置 (l)_p \in \textbf{P}) は、次のいずれかを指すことができます：

  • 0からプログラム入力の数までの範囲のプログラム入力：(0 \leq l)_p \lt \lvert \vec{I} \rvert)、または

  • 行番号。これは、プログラム入力の後に続く (N) 個の位置に対応します：(\lvert \vec{I} \rvert \leq l)_p \lt M )。

これらの二つの範囲は連続しているため、コンポーネントパラメータの位置は最終的に (0 \leq l)_p \lt M ) の範囲内に収まります。

コンポーネント一時結果の位置 (l)_r \in \textbf{R}) は行番号を指す必要があり、そのため (\lvert \vec{I} \rvert \leq l)_r \lt M ) の範囲内に収まります。

これらすべてをまとめると、ウェルフォームプログラム制約 (\psi_\mathrm{wfp}) が得られます：

( \begin{align} \psi_\mathrm{wfp}(L) &= \bigwedge\limits extbackslash_{p \in \textbf{P}} \left( 0 \leq l)p \lt M \right) \ & \land , \bigwedge\limits extbackslash{r \in \textbf{R}} \left( \lvert \vec{I} \rvert \leq l)_r \lt M \right) \ & \land , \psi_\mathrm{cons}(L) \ & \land , \psi_\mathrm{acyc}(L) \end{align} )

そして、これはその内訳です：

( \bigwedge\limits extbackslash_{p \in \textbf{P}} \left( 0 \leq l)_p \lt M \right) )各コンポーネントパラメータの位置 (l)_p は、プログラム入力または行番号を指し、
( \land , \bigwedge\limits extbackslash_{r \in \textbf{R}} \left( \lvert \vec{I} \rvert \leq l)_r \lt M \right) )各コンポーネント結果の位置 (l)_r は、行番号を指し、
( \land , \psi_\mathrm{cons}(L) )位置マッピングは一貫性があり、
( \land , \psi_\mathrm{acyc}(L) )位置マッピングは非循環である。

これで、位置マッピングがウェルフォームプログラムに対応することを保証する制約を定義できたので、コンポーネント間の接続とライブラリの動作をエンコードするだけで済みます。これは聞き覚えがあるはずです。検証の (\phi_\mathrm{conn}) と (\phi_\mathrm{lib}) の有限合成の等価物が必要です。そして、(\phi_\mathrm{lib}) は、検証中か有限合成中かに関わらず、ライブラリの動作は変わらないため、調整する必要がないことが判明しました。しかし、(\phi_\mathrm{conn}) は既に知られているコンポーネント間の接続のセットをチェックしていましたが、有限合成ではそれらの接続を検索しているため、異なるクエリが必要です。

これらの接続はコンポーネント間のデータフローを定義します。それらは、コンポーネントから構築された回路の配線です。あるコンポーネント結果から別のコンポーネント入力への接続は、有限合成クエリで結果変数と入力変数を等しく制約する必要があることを意味します。例えば、コンポーネント (\phi)_i が行 3 に配置され、パラメータ (p) が場所 3 に割り当てられた場合、(p) はそのコンポーネントの出力 (O)_i と同じ値を取らなければなりません。

これにより、(\psi_\mathrm{conn}) の定義が得られます。位置変数の各ペア (l)_x と (l)_y について、それらが同じ場所を参照する場合、(x) と (y) は同じ値を持たなければなりません。

( \psi_\mathrm{conn}(L, \vec{I}, O, \textbf{P}, \textbf{R}) = \bigwedge\limits extbackslash_{x,y \in \vec{I} \cup \textbf{P} \cup \textbf{R} \cup { O } } \left( \left( l)_x = l)_y \right) \implies \left( x = y \right) \right) )

ここにその内訳があります：

( \bigwedge\limits extbackslash_{x,y \in \vec{I} \cup \textbf{P} \cup \textbf{R} \cup { O } } )位置変数の各ペア (l)_x と (l)_y について、(x) と (y) がプログラム入力、またはコンポーネントのパラメータ、またはコンポーネントの一時結果、またはプログラム出力のいずれかである場合、
( \left( l)_x = l)_y \right)位置変数が同じ場所を参照する場合、
( \implies )その場合
( \left( x = y \right) )(x) と (y) は同じ値を持たなければなりません。

これで、位置マッピングの有限合成クエリの定義の準備が整いました。このクエリは、ソルバーに、ウェルフォームプログラムに対応する位置マッピングを見つけるように要求します。これは、そのプログラムが (S) の各例入力に対して仕様を満たすことを意味します。言い換えれば、それは次を強制しなければなりません：

  • 位置マッピングはウェルフォームプログラムに対応する、そして

  • 位置マッピングによってコンポーネントが接続され、ライブラリによってコンポーネントが動作すると仮定すると、

  • 仕様は (S) の各例入力に対して満たされる。

ついに、有限合成クエリです：

( \begin{align} & \exists L, O_0, \ldots, O extbackslash_{\vert S \rvert - 1}, \textbf{P}_0, \ldots, \textbf{P} extbackslash_{\vert S \rvert - 1}, \textbf{R}_0, \ldots, \textbf{R} extbackslash_{\vert S \rvert - 1}: \ & \qquad \psi_\mathrm{wfp}(L) ,, \land \ & \qquad \qquad \bigwedge\limits extbackslash_{i=0}^{\vert S \rvert - 1} \left( \phi_\mathrm{lib}(\textbf{P}_i, \textbf{R}_i) \land \psi_\mathrm{conn}(L, S_i, O_i, \textbf{P}_i, \textbf{R}_i) \land \phi_\mathrm{spec}(S_i, O_i) \right) \ \end{align} )

それはかなりの mouthful なので、もう一度、分解して内訳を見てみましょう：

( \exists L, O_0, \ldots, O extbackslash_{\vert S \rvert - 1}, \textbf{P}_0, \ldots, \textbf{P} extbackslash_{\vert S \rvert - 1}, \textbf{R}_0, \ldots, \textbf{R} extbackslash_{\vert S \rvert - 1}: )位置マッピング (L) と、(S) の各例に対するプログラム出力、コンポーネントパラメータ、およびコンポーネント結果変数が存在し、
( \psi_\mathrm{wfp}(L) ,, \land )位置マッピングはウェルフォームプログラムであり、
( \bigwedge\limits extbackslash_{i=0}^{\vert S \rvert - 1} )各例入力インデックス (i) について、
( \phi_\mathrm{lib}(\textbf{P}_i, \textbf{R}_i) )コンポーネントはライブラリによって記述されたとおりに動作し、
( \land ,, \psi_\mathrm{conn}(L, S_i, O_i, \textbf{P}_i, \textbf{R}_i) )コンポーネントは位置マッピングによって記述されたとおりに接続され、
( \land ,, \phi_\mathrm{spec}(S_i, O_i) )仕様は (i^\mathrm{th}) 例入力に対して満たされる。

ソルバーがこのクエリの充足可能な代入を見つけると、(S) の例入力のそれぞれに対して正しいプログラムに対応する新しい候補位置マッピングが得られます。ソルバーがクエリを充足不能と見つけると、それは例入力のそれぞれに対して正しいプログラムに対応する位置マッピングが存在しないことを意味し、したがって私たちの検索は失敗したことを意味します。

実装

Z3を使用して有限合成と検証クエリを解決する、ループフリー、コンポーネントベースのプログラムシンセサイザーをRustで実装しました。実装のリポジトリはこちらです。

私たちのターゲット言語には、固定幅整数を扱うために期待されるすべての操作が含まれています。算術演算子（add、mulなど）があります。ビット演算子（and、xorなど）があります。比較演算子（eqなど）があり、比較が真の場合は1、偽の場合は0を評価します。最後に、条件、結果、代替の3つのオペランドを取るselect操作があります。条件がゼロでない場合、それは結果を評価し、そうでなければ代替を評価します。

値は符号付きでも符号なしでもありません。符号付き整数と符号なし整数で動作が異なる除算のような操作については、各動作に対して異なる命令があります：符号付き除算の場合はdiv_s、符号なし除算の場合はdiv_u。

プログラム表現

プログラムは命令のシーケンスです：

pub struct Program {
    instructions: Vec<Instruction>,
}

命令はオペレータを持ち、その結果を識別子に束縛します：

pub struct Instruction {
    result: Id,
    operator: Operator,
}

識別子は数値の不透明ラッパーです：

pub struct Id(u32);

基本的にすべてが一時的なものであるため、識別子にわかりやすい名前をサポートしません。プログラムを文字列化するときは、識別子を a、b、c などに変換します。

さらに、Id(i) が常にプログラムの i 番目の命令で定義された値を参照するという不変条件を維持します。

最後に、Operator 列挙型は、言語の各操作に対応するバリアントと、そのオペランドの識別子を持っています：

pub enum Operator {
    Var,                // 新しい入力変数。

    Const(u64),         // 定数値。

    Eqz(Id),            // ゼロと等しいか？
    Clz(Id),            // 先行ゼロの数。
    Ctz(Id),            // 後続ゼロの数。
    Popcnt(Id),         // ポップカウント。

    Eq(Id, Id),         // 等しいか？
    Ne(Id, Id),         // 等しくないか？
    LtS(Id, Id),        // 符号付き未満か？
    LtU(Id, Id),        // 符号なし未満か？
    GtS(Id, Id),        // 符号付きより大きいか？
    GtU(Id, Id),        // 符号なしより大きいか？
    LeS(Id, Id),        // 符号付き以下か？
    LeU(Id, Id),        // 符号なし以下か？
    GeS(Id, Id),        // 符号付き以上か？
    GeU(Id, Id),        // 符号なし以上か？

    Add(Id, Id),        // 加算。
    Sub(Id, Id),        // 減算。
    Mul(Id, Id),        // 乗算。
    DivS(Id, Id),       // 符号付き除算。
    DivU(Id, Id),       // 符号なし除算。
    RemS(Id, Id),       // 符号付き剰余。
    RemU(Id, Id),       // 符号なし剰余。

    And(Id, Id),        // AND。
    Or(Id, Id),         // OR。
    Xor(Id, Id),        // 排他的OR。
    Shl(Id, Id),        // 左シフト。
    ShrS(Id, Id),       // 符号付き右シフト。
    ShrU(Id, Id),       // 符号なし右シフト。
    Rotl(Id, Id),       // 左回転。
    Rotr(Id, Id),       // 右回転。

    Select(Id, Id, Id), // If then else。
}
プログラムの構築

手作業でプログラムを構築しやすくするために、プログラムビルダーを用意しました。これは内部の Program をラップし、各オペレーションに対応するメソッドを提供して、ビルダーが構築中のプログラムにそのオペレーションを使用する命令を追加します。

pub struct ProgramBuilder {
    program: Program,
}

impl ProgramBuilder {
    /// 新しいプログラムの構築を開始します！
    pub fn new() -> ProgramBuilder {
        ProgramBuilder {
            program: Program { instructions: vec![] },
        }
    }

    /// このプログラムの構築を完了します！
    pub fn finish(self) -> Program {
        self.program
    }

    fn next_id(&self) -> Id {
        Id(self.program.instructions.len() as u32)
    }

    // ...

    /// `add a, b` 命令を追加します！
    pub fn add(&mut self, a: Id, b: Id) -> Id {
        let result = self.next_id();
        self.program.instructions.push(Instruction {
            result,
            operator: Operator::Add(a, b),
        });
        result
    }

    // ...
}

ProgramBuilder を介して構築された、右端のゼロビットを分離する例プログラムを次に示します：

// isolate_rightmost_zero_bit(x):
//     a ← not x
//     b ← add 1, x
//     c ← and a, b
//     return c

let builder = ProgramBuilder::new();

let x = builder.var();
let a = builder.not(x);
let one = builder.const_(1);
let b = builder.add(one, x);
let c = builder.and(a, b);

let isolate_rightmost_zero_bit = builder.finish();

ビルダーがあるのは良いことです。なぜなら、最適化されたプログラムを合成するために使用する仕様として、最適化されていないプログラムを手書きするつもりだからです。

コンポーネントの定義

すべてのオペレータには関連付けられたコンポーネントがあるため、そのオペレータを使用するプログラムを合成できます。ライブラリは異種コンポーネントのセットを持つことができるため、オブジェクト指向の Component トレイトを定義し、それらをトレイトオブジェクトとしてボックス化して動的にディスパッチされたメソッドで格納し、すべて同じコレクションに格納できるようにします。

A Component has two roles:

  1. It must provide the constraints between its inputs and its output for the solver. This is its (\phi)_i(\vec{I}_i, O)_i that will be part of the whole library’s (\phi_\mathrm{lib}(\textbf{P}, \textbf{R})).
  2. After we’ve synthesized some location mapping for a program that uses this component, in order to construct the corresponding Program, the component needs to know how to create the Operator it represents.

The make_expression trait method will handle the first role, and the make_operator trait method will handle the second. make_expression takes Z3 BitVec variables as its operands (the (\vec{I}_i) input variables) and returns a new Z3 BitVec expression that represents the result of running the operation on the operands (the (O)_i output variable). make_operator takes the Ids of its operands (as described by a synthesized location mapping) and returns its associated Operator with those Ids as its operands.

Note that, because different components have different arities, these methods don’t take their operands as multiple, individual parameters like a: BitVec, b: BitVec or a: Id, b: Id. Instead, components report their arity with the operand_arity trait method and callers pass in a slice of that many operands.

Finally, we also support synthesizing constant values for the const operator. These immediates are handled separately from operands, and so we also have the immediate_arity trait method, and make_expression and make_operator also takes slices of immediates.

pub trait Component {
    /// How many operands does this component take?
    fn operand_arity(&self) -> usize;

    /// How many immediates does this component need
    /// synthesized?
    fn immediate_arity(&self) -> usize;

    /// Construct this component's constraint as a Z3
    /// expression.
    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a>;

    /// Construct an `Operator` from the given
    /// immediates and operands.
    fn make_operator(
        &self,
        immediates: &[u64],
        operands: &[Id]
    ) -> Operator;
}

Let’s take a look at the implementation of a simple, representative component: the add component。

  • It has two operands and zero immediates。

  • The make_operator implementation is mechanical, pulling out its individual operands from the given slice, just to push them into the Operator::Add。

  • The make_expression implementation is similarly concise, but is not quite mechanical. This is where we encode the add operator’s semantics into a Z3 expression. SMT-LIB2 defines a bvadd operatoin for wrapping addition on bitvectors, and the z3 crate we’re using exposes it to us as a method on BitVec. Wrapping addition is exactly what we want for our add instruction, and so all we have to do to encode our add operation’s semantics is bvadd our two operands。

  • Because we are always working with components as trait objects, we also define a helper function for boxing up the Add component and turning it into a trait object with dynamically dispatched methods。

struct Add;

impl Component for Add {
    fn operand_arity(&self) -> usize {
        2
    }

    fn immediate_arity(&self) -> usize {
        0
    }

    fn make_operator(
        &self,
        immediates: &[u64],
        operands: &[Id],
    ) -> Operator {
        Operator::Add(operands[0], operands[1])
    }

    fn make_expression<'a>(
        &self,
        _context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        _bit_width: u32,
    ) -> BitVec<'a> {
        operands[0].bvadd(&operands[1])
    }
}

pub fn add() -> Box<dyn Component> {
    Box::new(Add) as _
}

Most components look pretty much like that: there is some direct encoding into a single SMT expression for the operation。

Other components, like eqz, don’t have a direct encoding as a single SMT expression, and we need to compose multiple。

impl Component for Eqz {
    // ...

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        _immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a> {
        let zero = BitVec::from_i64(
            context,
            0,
            bit_width,
        );
        let one = BitVec::from_i64(
            context,
            1,
            bit_width,
        );
        // `ite` is "if-then-else". If the operand
        // is zero, evaluate to one, otherwise
        // evaluate to zero.
        zero._eq(&operands[0]).ite(&one, &zero)
    }
}

The const component is the only component that uses immediates. It doesn’t have operands. Either its constant value is unbound, in which case we’re synthesizing the value, or we provide a value for it upon constructing the component：

struct Const(Option<u64>);

impl Component for Const {
    fn operand_arity(&self) -> usize {
        0
    }

    fn immediate_arity(&self) -> usize {
        if self.0.is_some() {
            0
        } else {
            1
        }
    }

    fn make_operator(
        &self,
        immediates: &[u64],
        _operands: &[Id]
    ) -> Operator {
        if let Some(val) = self.0 {
            Operator::Const(val)
        } else {
            Operator::Const(immediates[0])
        }
    }

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        _operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a> {
        if let Some(val) = self.0 {
            BitVec::from_i64(
                context,
                val as i64,
                bit_width,
            )
        } else {
            immediates[0].clone()
        }
    }
}

pub fn const_(val: Option<u64>) -> Box<dyn Component> {
    Box::new(Const(val)) as _
}

Finally, a library is just a vector of components：

pub struct Library {
    pub components: Vec<Box<dyn Component>>,
}
仕様

仕様はコンポーネントと非常によく似ていますが、SMT制約を作成するだけで済みます。仕様から Operator を構築する必要はないため、Component::make_operator メソッドの同等のものはありません。

pub trait Specification {
    fn arity(&self) -> usize;

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        bit_width: u32,
    ) -> Bool<'a>;
}

既存の、最適化されていないプログラムを新しい、最適化されたプログラムの仕様として使用したいので、Program に対して Specification を実装します。

プログラム仕様のアリティは、プログラムが var オペレータで定義する入力変数の数です：

impl Specification for Program {
    fn arity(&self) -> usize {
        self.instructions
            .iter()
            .take_while(|inst| {
                inst.operator == Operator::Var
            })
            .count()
    }

    // ...
}

プログラム全体のZ3式を作成するために、命令ごとにサブ式をテーブルに構築していきます。このテーブルはレキシカル環境として機能します。オペレータのオペランド Id を検査することで、このテーブルから対応するサブ式を拾い上げ、オペランドを命令の Component::make_expression 実装に渡します。テーブルの最後の項目はプログラム全体の式です。なぜなら、プログラムは暗黙的に最後の値を返すからです。

impl Specification for Program {
    // ...

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        bit_width: u32,
    ) -> Bool<'a> {
        // `exprs[i]` は、このプログラムの `i` 番目の命令で
        // 定義された値のZ3サブ式です。
        let mut exprs: Vec<_> = inputs
            .iter()
            .cloned()
            .collect();

        let mut operands = vec![];

        for instr in self
            .instructions
            .iter()
            .skip(inputs.len())
        {
            // プログラム内のすべての `const` は既に
            // 値が束縛されているため、どの命令も
            // 新しい即値（immediate）を必要としません。
            let immediates = [];

            // このオペレータが使用している各オペランドの
            // サブ式を収集します。
            operands.clear();
            instr
                .operator
                .operands(|Id(i)| {
                    let v = exprs[i as usize].clone();
                    operands.push(v);
                });

            // この命令のZ3式を作成し、`exprs` にプッシュします。
            exprs.push(
                instr
                    .operator
                    .make_expression(
                        context,
                        &immediates,
                        &operands,
                        bit_width,
                    )
            );
        }

        // 最後の命令が返り値を定義し、それは
        // `output` 変数と等しくなければなりません。
        exprs.last().unwrap()._eq(output)
    }
}
シンセサイザー

Synthesizer 構造体は、私たちのための一つの合成問題を解決します。コンストラクタでライブラリと仕様を受け取り、その後、いくつかのビルダー風メソッドで実行方法を設定し、最後に synthesize メソッドを呼び出して実際にCEGISループを開始します。

/// コンポーネントベースのループフリープログラムを作成するためのプログラムシンセサイザー。
pub struct Synthesizer<'a> {
    // ...
}

impl<'a> Synthesizer<'a> {
    /// 指定されたライブラリと仕様で新しいシンセサイザーを作成します。
    ///
    /// 作成後、様々なビルダー風メソッドで合成プロセスを設定する機会があります。
    pub fn new(
        context: &'a z3::Context,
        library: &'a Library,
        spec: &'a dyn Specification,
    ) -> Result<Self> {
        // ...
    }

    /// 合成に仕様を満たす最小長のプログラムを見つけることを要求するかどうかを設定します。
    ///
    /// これは最適に小さいプログラムを生成しますが、通常は時間がかかります。
    pub fn should_synthesize_minimal_programs(
        &mut self,
        should: bool,
    ) -> &mut Self {
        // ...
    }

    /// タイムアウトを設定します。
    ///
    /// タイムアウトがない場合、必要であれば無限に実行し続けます。
    /// ミリ秒単位の数値を指定すると、ギブアップする前にソフト最大実行時間が
    /// そのミリ秒数になります。
    pub fn set_timeout(
        &mut self,
        milliseconds: Option<u32>,
    ) -> &mut Self {
        // ...
    }

    /// この設定されたシンセサイザーを実行して、仕様を満たすプログラムを見つけます！
    pub fn synthesize(
        &mut self,
    ) -> Result<Program> {
        // ...
    }
}

これにより、次のように合成問題を作成、設定、実行できます：

let program = Synthesizer::new(&context, &library, &spec)
    .should_synthesize_minimal_programs(true)
    .set_timeout(Some(60 * 60 * 1000))
    .synthesize()?;
位置マッピング

位置マッピングは、コンポーネントベースプログラムを表すために多くの行インデックスを使用します。行はSMT式に直接表現できるものであるため、位置マッピングは合成のためにプログラムをエンコードする方法になります。

行を数学的な整数としてエンコードするか、ビットベクトルとしてエンコードするかを選択できます。私は元々数学的な整数を使用しましたが、予想通り、ビットベクトルを使用するよりもはるかに遅いです。ビットベクトル表現を使用することで、ライブラリのコンポーネントに必要な最小限のビット数を使用できます。例えば、プログラム入力が1つでライブラリに7つのコンポーネントがある場合、必要となる最大のゼロベース行番号は7であり、これはすべての行を表すために3ビット幅のビットベクトルのみが必要であることを意味します。ビットベクトルが狭いほど、Z3はそれらをより速く処理できます。読んだ論文で、行の表現については言及されていませんが、それは「誰もが知っている」という部族の知識であると確信しています。

// コンポーネントが配置される行、またはパラメータを取得する行のインデックス。
type Line<'a> = BitVec<'a>;

位置マッピングはCEGISの異なるフェーズで異なる方法で使用されます。プログラムを合成する前に、それらは構築中のSMTクエリの未束縛変数のコレクションです。合成後、それらの変数は具体的な値に束縛され、それ以降は値のみを扱いたいのです。変数自体はもう必要ありません。したがって、位置マッピングを二つの異なる表現に分割します：

  1. 有限合成の前および最中には、LocationVars があり、これは行変数のコレクションです。
  2. 有限合成後、それらの変数に割り当てられた値を Assignments 構造体に引き出します。これはインデックス値のコレクションです。

LocationVars は、プログラム入力 (\vec{I})、すべてのコンポーネントのパラメータ (\textbf{P})、すべてのコンポーネントの一時結果 (\textbf{R})、およびプログラム全体の出力 (O) のための行変数を持っています。また、行ビットベクトルの幅も追跡します。

struct LocationVars<'a> {
    // プログラム入力に行が割り当てられる変数。
    // これらは常に `0..inputs.len()` に割り当てられます。
    inputs: Vec<Line<'a>>,

    // `params[i]` は、`i` 番目のコンポーネントパラメータを
    // 定義する行の変数です。
    params: Vec<Line<'a>>,

    // `results[i]` は、合成プログラムで `i` 番目のコンポーネントが
    // 配置される行の変数であり、したがって `i` 番目の
    // コンポーネントの一時結果が定義される場所です。
    results: Vec<Line<'a>>,

    // プログラムの最終出力が定義される行の変数。
    output: Line<'a>,

    // 任意の行位置を表すために必要な最小ビット幅。
    line_bit_width: u32,
}

元の論文とは異なり、合成された位置マッピングの最後の行からプログラム出力を常に取得するわけではありません。代わりに、プログラムの早い段階で output 行を設定することを許可し、実質的に早期リターンを挿入します。これにより、（オプションで）最適コードサイズのプログラムを合成できます。つまり、正しいプログラムを合成できる最も早い output 行を見つけることができます。この小さなトリックはSouperから取られています。

Assignments はすべて同じものですが、行の変数ではなく、SMTソルバーが提供したモデルから取り出した行の値があります。また、合成された即値（immediate）の値も含まれます。

struct Assignments {
    // 合成された即値。
    immediates: Vec<u64>,

    // `params[i]` は、`i` 番目のパラメータが定義されるプログラム内の行です。
    params: Vec<u32>,

    // `results[i]` は、`i` 番目のコンポーネントが配置されるプログラム内の行であり、
    // したがって `i` 番目のテンポラリ結果が定義されます。
    results: Vec<u32>,

    // プログラムの最終出力が定義される行。
    output: u32,
}
検証

検証は、有限合成によって生成された Assignments を受け取り、反例を見つけようとします。反例を見つけた場合、CEGISループを続行する必要があります。反例を見つけられない場合、解が見つかったので完了です。

元の論文では、検証クエリで候補プログラムを (\phi_\mathrm{lib}) と (\phi_\mathrm{conn}) で表現しており、ソルバーにコンポーネント間の接続を解釈するように求めています。これも私が元々行ったことですが、その後、ある気づきがありました：

  • ソルバーが解くために、Assignments を Program に変換し、その後 Program をSMT式に変換する能力が既に必要です。

  • Program をSMT式に変換することは既に可能です。なぜなら、最適化されていないプログラムを最適化プログラムの仕様として使用するからです。

これにより、Assignments を Program に変換し、その後SMT式に変換できます。なぜこのSMT式が仕様を直接含意するかを検証しないのでしょうか？ これは意味します：

  • 検証中に (\phi_\mathrm{lib}) と (\phi_\mathrm{conn}) を構築する必要はありません。

  • ソルバーは、検証クエリを解決するために、コンポーネントの入力と出力間のすべての接続を統一する必要はありません。

  • これは一般的に、より小さなクエリを生成し、通常はより大きなクエリよりも速く解決されるはずです。

これは実装でコードを少し節約しましたが、全体的な合成時間には速度向上をもたらしませんでした。なぜなら、ほとんどの時間は有限合成に費やされ、検証には費やされないからです。

いずれにせよ、検証の実装は次のとおりです：

impl<'a> Synthesizer<'a> {
    fn verification(
        &mut self,
        assignments: &Assignments,
        bit_width: u32,
    ) -> Result<Verification> {
        // 新しい入力と出力変数を作成します。
        let inputs: Vec<_> = (0..self.spec.arity())
            .map(|_| {
                fresh_input(self.context, bit_width)
            })
            .collect();
        let output = fresh_output(
            self.context,
            bit_width,
        );

        // 代入をプログラムに変換し、
        // その後、それをSMT式に変換します。
        let mut prog = assignments
            .to_program(self.spec.arity(), self.library)
            .make_expression(
                self.context,
                &inputs,
                &output,
                bit_width,
            );

        let spec = self
            .spec
            .make_expression(
                self.context,
                &inputs,
                &output,
                bit_width,
            );

        // 私たちのプログラムの仕様が満たされない入力は存在しますか？
        let not_spec = spec.not();
        let query = prog.and(&[&not_spec]);
        let solver = self.solver();
        solver.assert(&query);

        match solver.check() {
            // カウンター例が存在するかどうかはわかりません。これは通常、
            // 以前に設定されたタイムアウト制限に達したことを意味します。
            z3::SatResult::Unknown => {
                Err(Error::SynthesisUnknown)
            }

            // 仕様を満たさない入力はもうありません！完了です！
            z3::SatResult::Unsat => {
                Ok(Verification::WorksForAllInputs)
            }

            // 仕様を満たさない入力が存在します。カウンター例を返します。
            z3::SatResult::Sat => {
                let model = solver.get_model();
                self.add_invalid_assignment(assignments);
                let inputs = eval_bitvecs(
                    &model,
                    &inputs,
                );
                Ok(Verification::Counterexample(inputs))
            }
        }
    }
}

検証がカウンター例を見つけた場合、add_invalid_assignment メソッドを呼び出します。これはSouperから取られた別のトリックです。一部の入力に対して機能するがすべてではない代入を記憶し、将来の有限合成クエリで明示的に禁止します。これにより、SMTソルバーがこれらの有望に見える代入を再検討するのを避け、再び例入力のいずれかに対して機能しないことを見つけるのを避けます。

有限合成

有限合成は、私たちの例入力すべてに対して仕様を満たす位置マッピングを検索します。ただし、他の入力が与えられた場合に仕様を満たすかどうかはわかりません。

位置マッピングに対する最初の制約は、それがウェルフォームプログラムに対応することです。この制約は実際にはCEGISの各反復で同じなので、新しい Synthesizer インスタンスを作成するときに一度だけ制約を生成し、その後、CEGISループのすべての反復で既に構築された制約を再利用します。同様に、Synthesizer に位置変数を格納し、CEGISループ全体でそれらを再利用します。

pub struct Synthesizer<'a> {
    // ...
    locations: LocationVars<'a>,
    well_formed_program: Bool<'a>,
    // ...
}

ウェルフォームプログラム制約 (\psi_\mathrm{wfp}) の定義を思い出してください：

( \begin{align} \psi_\mathrm{wfp}(L) &= \bigwedge\limits extbackslash_{p \in \textbf{P}} \left( 0 \leq l)p \lt M \right) \ & \land , \bigwedge\limits extbackslash{r \in \textbf{R}} \left( \lvert \vec{I} \rvert \leq l)_r \lt M \right) \ & \land , \psi_\mathrm{cons}(L) \ & \land , \psi_\mathrm{acyc}(L) \end{align} )

これは、各パラメータ位置 (l)_p が (0 \leq l)_p < M ) の範囲内にあり、各一時結果位置 (l)_r が (\lvert \vec{I} \rvert \leq l)_r < M ) の範囲内にあり、位置が一貫性があり、データフローサイクルがないことを示しています。

Z3で対応するSMT式を構築することは、ほとんど直接それに従いますが、コンテキストを渡したり、Rustの usize と u32 を適切な幅のZ3ビットベクトルに変換したりする必要があるため、少しノイズが多くなります：

impl<'a> LocationVars<'a> {
    fn well_formed_program(
        &self,
        context: &'a z3::Context,
        library: &Library,
        invalid_connections: &mut HashSet<(u32, u32)>,
    ) -> Bool<'a> {
        // すべてのウェルフォームプログラム制約をこのリストに構築し、
        // 最後にすべてを `and` します。
        let mut wfp = vec![];

        // ウェルフォームプログラムは一貫性があります。
        wfp.push(self.consistent(
            context,
            invalid_connections,
        ));

        // ウェルフォームプログラムは非循環です。
        wfp.push(self.acyclic(context, library));

        let i_len = self.line_from_u32(
            context,
            self.inputs.len() as u32,
        );
        let m = self.line_from_u32(
            context,
            (self.results.len() +
                self.inputs.len()) as u32,
        );
        let zero = self.line_from_u32(context, 0);

        // 入力は常に最初の位置に割り当てられます。
        for (i, l) in self.inputs.iter().enumerate() {
            let i = self.line_from_u32(
                context,
                i as u32,
            );
            wfp.push(l._eq(&i));
        }

        // すべてのコンポーネントパラメータ位置は `0 <= l < M` の範囲内にあります。
        for l in &self.params {
            // 0 <= l
            wfp.push(line_le(&zero, l));
            // l < M
            wfp.push(line_lt(l, &m));
        }

        // すべてのコンポーネント結果位置は `|i| <= l < M` の範囲内にあります。
        for l in &self.results {
            // |i| <= l
            wfp.push(line_le(&i_len, l));
            // l < m
            wfp.push(line_lt(l, &m));
        }

        // すべての制約を `and` します。
        and(context, &wfp)
    }
}

(\psi_\mathrm{cons}) の一貫性制約は、二つのコンポーネントを同じ行に割り当てないことを保証します：

( \psi_\mathrm{cons}(L) = \bigwedge\limits extbackslash_{x,y \in \textbf{R}, x \not\equiv y} \left( l)_x \neq l)_y \right) )

私たちの consistent メソッドは、対応するSMT式をZ3用に作成し、さらに位置インデックスのペアを invalid_connections マップに記録します。このマップは、ウェルフォームプログラムが直接データフローを持てない位置変数のペアの記録を保持します。したがって、最終的な (\psi_\mathrm{conn}) 接続制約の実装で、これらのペアの接続節を追加する必要はありません。これらのペアを接続制約から除外することで、SMT式がさらに小さくなり、Z3がそれをより速く解決するのに役立つはずです。このトリックもSouperから取られました。

impl LocationVars<'a> {
    fn consistent(
        &self,
        context: &'a z3::Context,
        invalid_connections: &mut HashSet<(u32, u32)>,
    ) -> Bool<'a> {
        // すべての一貫性制約をこのリストに構築します。
        let mut cons = vec![];

        for (i, (index_x, loc_x)) in self
            .results_range()
            .zip(&self.results)
            .enumerate()
        {
            for (index_y, loc_y) in self
                .results_range()
                .zip(&self.results)
                .skip(i + 1)
            {
                // 結果から別の結果への直接のデータフローはできません。
                // パラメータを介して接続する必要があるため、
                // このペアを無効な接続マップに追加します。
                invalid_connections.insert(
                    (index_x, index_y)
                );

                // コンポーネントは同じ行に割り当てられないため、
                // これらの位置変数は同じ値を持つことはできません：
                // `loc_x != loc_y`。
                cons.push(loc_x._eq(loc_y).not());
            }
        }

        // すべての制約を `and` します。
        and(context, &cons)
    }
}

次に、(\psi_\mathrm{acyc}) 非循環制約の実装です。これは、合成された位置マッピングにデータフローサイクルがないことを保証します：

( \psi_\mathrm{acyc}(L) = \bigwedge\limits extbackslash_{i=0}^{N-1} \left( \bigwedge\limits extbackslash_{p \in \vec{I}_i} \left( l)p < l extbackslash{O)_i} \right) \right) )

非循環制約の実装は、特に工夫はなく、制約をSMT式に直接変換したものです：

impl LocationVars<'a> {
    fn acyclic(
        &self,
        context: &'a z3::Context,
        library: &Library,
    ) -> Bool<'a> {
        // 制約をこのリストに構築します。
        let mut acycs = vec![];

        let mut params = self.params.iter();

        for (result_loc, comp) in self
            .results
            .iter()
            .zip(&library.components)
        {
            for _ in 0..c.operand_arity() {
                let param_loc = params.next().unwrap();

                // コンポーネントのパラメータの位置は、
                // コンポーネントの結果の位置よりも小さくなければなりません。
                // つまり、パラメータは使用される前に定義されていることを意味します：`param_loc < result_loc`。
                acycs.push(
                    line_lt(param_loc, result_loc)
                );
            }
        }

        // すべての制約を `and` します。
        and(context, &acycs)
    }
}

次に、(\psi_\mathrm{conn}) 接続制約と (\phi_\mathrm{lib}) ライブラリ仕様の実装です。これらはCEGISループの各反復で変更されるため、キャッシュして再利用することはできません。例入力ごとにインスタンス化するためです。そのため、キャッシュして再利用することはできません。

(\psi_\mathrm{conn}) 接続制約は、ライブラリコンポーネント間のデータフロー接続をエンコードします。二つの位置変数が同じ場所を参照する場合、それらの変数によって位置が割り当てられたエンティティは同じ値を持たなければなりません。

( \psi_\mathrm{conn}(L, \vec{I}, O, \textbf{P}, \textbf{R}) = \bigwedge\limits extbackslash_{x,y \in \vec{I} \cup \textbf{P} \cup \textbf{R} \cup { O } } \left( \left( l)_x = l)_y \right) \implies \left( x = y \right) \right) )

connectivity メソッドは、この制約を実装するZ3式を構築します。以前は、直接接続できない位置変数のペアを記録していましたが、ここではそのような接続をこの制約から除外し、SMT式を小さく保ちます。これは、前述のトリックです。

impl<'a> Synthesizer<'a> {
    fn connectivity(
        &self,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        params: &[BitVec<'a>],
        results: &[BitVec<'a>],
    ) -> Bool<'a> {
        // 位置変数のインデックスを、位置変数とその関連エンティティに
        // マッピングするテーブル：`index -> (l[x], x)`。
        let locs_to_vars: Vec<_> = self
            .locations
            .inputs
            .iter()
            .zip(inputs)
            .chain(
                self.locations
                    .params
                    .iter()
                    .zip(params)
            )
            .chain(
                self.locations
                    .results
                    .iter()
                    .zip(results)
            )
            .chain(iter::once(
                (&self.locations.output, output)
            ))
            .collect();

        // 制約をこのリストに構築します。
        let mut conn = vec![];

        for (index_x, (l_x, x)) in locs_to_vars
            .iter()
            .enumerate()
        {
            for (index_y, (l_y, y)) in locs_to_vars
                .iter()
                .enumerate()
                .skip(i + 1)
            {
                // これらの場所が直接接続できない場合、
                // 制約を気にする必要はありません。
                if self.is_invalid_connection(
                    index_x as u32,
                    index_y as u32,
                ) {
                    continue;
                }

                // この二つの位置変数が同じ場所を参照する場合、
                // それらのエンティティは互いに接続されており、
                // 同じ値を持たなければなりません。
                conn.push(
                    l_x._eq(l_y).implies(&x._eq(y))
                );
            }
        }

        // すべての制約を `and` します。
        and(self.context, &conn)
    }
}

私たちの最後の前提条件は、ライブラリ全体の動作を記述する (\phi_\mathrm{lib}) ライブラリ仕様の実装です：

( \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) = \phi)_i(\vec{I}_0, O)_0) \land \ldots \land \phi)i(\vec{I}_{N-1}, O extbackslash{{N-1}} )

(\phi_\mathrm{lib}) ライブラリ仕様の実装には、各コンポーネントの即値、オペランド、および結果変数を取得し、コンポーネントにその変数間の関係を表すSMT式を作成するように要求し、最後にそれらのすべての式を and します。

impl<'a> Synthesizer<'a> {
    fn library(
        &self,
        immediates: &[BitVec<'a>],
        params: &[BitVec<'a>],
        results: &[BitVec<'a>],
        bit_width: u32,
    ) -> Bool<'a> {
        // 各コンポーネントの仕様式をここに構築します。
        let mut lib = vec![];

        let mut immediates = immediates;
        let mut params = params;

        for (result, comp) in results
            .iter()
            .zip(&self.library.components)
        {
            // このコンポーネントの即値をリストの先頭から分割します。
            let (these_imms, rest) = immediates.split_at(
                comp.immediate_arity()
            );
            immediates = rest;

            // このコンポーネントのパラメータをリストの先頭から分割します。
            let (these_params, rest) = params.split_at(
                comp.operand_arity()
            );
            params = rest;

            // このコンポーネントの仕様を作成し、
            // その結果がそれによって制約されるようにします。
            lib.push(
                result._eq(&comp.make_expression(
                    self.context,
                    these_imms,
                    these_params,
                    bit_width,
                ))
            );
        }

        // すべてのコンポーネント仕様を `and` します。
        and(self.context, &lib)
    }
}

さて、有限合成クエリ全体を実装するために必要なすべての関数が揃いました！有限合成クエリは、位置マッピングに値を割り当てます。これにより、結果のマッピングはウェルフォームプログラムに対応し、そのプログラムは私たちの例入力のそれぞれに対して仕様を満たします。

( \begin{align} & \exists L, O_0, \ldots, O extbackslash_{\vert S \rvert - 1}, \textbf{P}_0, \ldots, \textbf{P} extbackslash_{\vert S \rvert - 1}, \textbf{R}_0, \ldots, \textbf{R} extbackslash_{\vert S \rvert - 1}: \ & \qquad \psi_\mathrm{wfp}(L) ,, \land \ & \qquad \qquad \bigwedge\limits extbackslash_{i=0}^{\vert S \rvert - 1} \left( \phi_\mathrm{lib}(\textbf{P}_i, \textbf{R}_i) \land \psi_\mathrm{conn}(L, S_i, O_i, \textbf{P}_i, \textbf{R}_i) \land \phi_\mathrm{spec}(S_i, O_i) \right) \ \end{align} )

有限合成クエリの実装は、主にその公式と同じ構造に従います：

  • ウェルフォームプログラム制約は既にキャッシュされており、再利用できるため、ここで再作成する必要はありません。

  • 各例入力についてループします：

    • 各例に対して、新しいプログラム出力変数、新しいコンポーネントパラメータ変数、および新しいコンポーネント結果変数を生成します。

    • 各コンポーネントのパラメータと出力を、ライブラリによって指示されたとおりに動作するように制約します。

    • 位置マッピングによって記述されたとおりに、接続制約を使用してクロスコンポーネント変数を接続します。

    • この例入力に対してプログラム仕様が満たされることを要求します。

  • さらに、プログラムの出力の位置を指定された行に割り当てます。これにより、呼び出し元はオプションで最適に短いプログラムの合成を強制できます。

  • 最後に、クエリを実行し、ソルバーのモデルから位置マッピングの代入を解析します。

impl<'a> Synthesizer<'a> {
    fn finite_synthesis(
        &mut self,
        example_inputs: &HashSet<Vec<u64>>,
        output_line: u32,
        bit_width: u32,
    ) -> Result<Assignments> {
        let immediates = self.fresh_immediates(
            bit_width
        );

        // このリストに、各入力に対して位置代入が機能する制約を構築します。
        let mut works_for_inputs = vec![];

        for inputs in example_inputs {
            // 入力をビットベクトルに変換します。
            let inputs: Vec<_> = inputs
                .iter()
                .map(|i| BitVec::from_i64(
                    self.context,
                    *i as i64,
                    bit_width,
                ))
                .collect();

            // 新しいパラメータ、結果、および
            // 出力変数を生成します。これらは公式の
            // 存在する量化子 `P[i]`, `R[i]`, および `O[i]` です。
            let params = self.fresh_param_vars(
                bit_width
            );
            let results = self.fresh_result_vars(
                bit_width
            );
            let output = fresh_output(
                self.context,
                bit_width,
            );

            // コンポーネントはライブラリによって記述されたとおりに動作します。
            let lib = self.library(
                &immediates,
                &params,
                &results,
                bit_width,
            );
            works_for_inputs.push(lib);

            // コンポーネントは位置変数によって記述されたとおりに接続されます。
            let conn = self.connectivity(
                &inputs,
                &output,
                &params,
                &results,
            );
            works_for_inputs.push(conn);

            // そして、それに基づいて、望ましいプログラム動作の仕様が満たされます。
            let spec = self
                .spec
                .make_expression(
                    self.context,
                    &inputs,
                    &output,
                    bit_width,
                );
            works_for_inputs.push(spec);
        }

        let works_for_inputs: Vec<&_> = works_for_inputs
            .iter()
            .collect();

        // 出力が必要な行にあることを強制します。
        let output_line = self.locations.line_from_u32(
            self.context,
            output_line,
        );
        let output_on_line = self
            .locations
            .output
            ._eq(&output_line);

        // すべてのピースをまとめます！
        let query = self
            .well_formed_program
            .and(&works_for_inputs)
            .and(&[
                &output_on_line,
                // 無効であることが判明した代入を
                // 合成しないようにします。
                &self.not_invalid_assignments,
            ]);

        let solver = self.solver();
        solver.assert(&query);

        match solver.check() {
            // 制約を満たす代入が存在するかどうか不明です。通常、これはタイムアウトが
            // 設定されており、時間がなくなったためです。
            z3::SatResult::Unknown => {
                Err(Error::SynthesisUnknown)
            }

            // 私たちの合成制約を満たす位置変数の代入は存在しません。この
            // コンポーネントライブラリで仕様を満たすプログラムを作成できません。
            z3::SatResult::Unsat => {
                Err(Error::SynthesisUnsatisfiable)
            }

            // OK、私たちの合成制約に適合する位置変数の代入があります！
            // モデルからそれらを引き出し、返します。
            z3::SatResult::Sat => {
                let model = solver.get_model();

                let immediates = eval_bitvecs(
                    &model,
                    &immediates,
                );

                let params = eval_lines(
                    &model,
                    &self.locations.params
                );

                let results = eval_lines(
                    &model,
                    &self.locations.results,
                );

                let output = eval_line(
                    &model,
                    &output_line,
                );

                Ok(Assignments {
                    immediates,
                    params,
                    results,
                    output,
                })
            }
        }
    }
}
CEGISループ

シンセサイザーが最適に短いプログラムを生成するように設定されている場合、Souperと同様に、CEGISループを別のループでラップします。Souperは最短のプログラム長から合成を開始し、最適な短い解を見つけるまで、より長く、より長いプログラムを許可します。対照的に、私たちは最も長いプログラム長から始めて、そこから短いプログラムを試していきます。これは二つの洞察に基づいています：

  1. 実際には、長さ n-1 のプログラムの検索に失敗した場合（そのようなプログラムが存在しないため）、長さ n のプログラムの検索に成功した場合よりもはるかに時間がかかるようです。ターゲットプログラム長を最長から最短に反復することで、高価なケースに一度だけ遭遇します。
  2. 必要以上に長いプログラムを合成すると、しばしばそのプログラムにはデッドコードが含まれます。ループフリープログラムでのデッドコード削除（DCE）の実行は非常に簡単で、デッドコードが削除されると、このループの数回の反復をスキップすることもできます。

シンセサイザーが最適に短いプログラムを生成するように設定されていない場合、ターゲットプログラム長の範囲を調整して、CEGISループに一度だけ呼び出すようにします。これは、最短長を最長長に設定することで達成します。

impl<'a> Synthesizer<'a> {
    pub fn synthesize(
        &mut self,
    ) -> Result<Program> {
        let mut example_inputs = self
            .initial_concrete_inputs()?;

        // このライブラリで合成できる最長のプログラムの長さ。
        let longest = self.spec.arity() as u32
            + self.library.components.len() as u32;

        // 試行する最短の長さのプログラム。
        let shortest = if self
            .should_synthesize_minimal_programs
        {
            self.spec.arity() as u32 + 1
        } else {
            longest
        };

        // 実際には、長さ `n-1` のプログラムの検索に失敗した場合（そのようなプログラムが存在しないため）のコストは、
        // 長さ `n` のプログラムの検索に成功した場合よりもはるかに高価です。
        // したがって、より長いプログラムから合成を開始し、反復ごとに長さを短くします。
        let mut best = Err(Error::SynthesisUnknown);
        let mut target_length = longest;
        while target_length >= shortest {
            // 現在のターゲット長のプログラムを合成して、CEGISループに呼び出します。
            match self.synthesize_with_length(
                target_length,
                &mut example_inputs,
            ) {
                // この長さでプログラムを見つけました -- それは私たちの新しい `best` です！
                //
                // DCEを実行し、このループの数回の反復をスキップできるようにし、
                // それからそれより1命令短いプログラムを検索します。
                Ok(mut program) => {
                    program.dce();
                    target_length =
                        program.instructions.len() as u32
                        - 1;
                    best = Ok(program);

                    // 無効な代入セットをリセットします。
                    // なぜなら、行 `i` を返すときに無効だった代入が、
                    // 行 `i-1` を返すときに有効になる可能性があるからです。
                    self.reset_invalid_assignments();
                    continue;
                }

                // このターゲット長でプログラムを合成できません、またはタイムアウトしました。
                // 現在の `best` 結果を返すか、それがない場合はこのエラーを返します。
                err => return best.or_else(|_| err),
            }
        }

        // ループを完了し、プログラムの合成に失敗して早期リターンしなかった場合、
        // それは長さ `shortest` のプログラムを持っていることを意味します。それを返します！
        best
    }
}

元々、この実装は乱数ジェネレータで初期の例入力を選択していました。Souperのソースコードを読んだ後、彼らがプログラム仕様をすべての入力と出力変数に束縛せずにソルバーに提示しているのを見ました。その後、ソルバー自身に例入力を解かせます。これらの入力は、乱数ジェネレータが選択する可能性のあるものよりもおそらく「興味深い」ものであり、それにより有限合成がより迅速により良い解を生成するのに役立つはずです。

この手法をシンセサイザーに実装し、さらに、入力変数を既に初期入力 (S) に追加したものから区別されるように制約しました。

この例入力検索クエリの論理式は次のとおりです：

( \begin{align} & \exists \vec{I}, O: \ & \qquad \phi_\mathrm{spec}(\vec{I}, O) \land \bigwedge\limits extbackslash_{i=0}^{\vert S \rvert - 1} \left( \vec{I} \neq S_i \right) \end{align} )

そして、その内訳は次のとおりです：

( \exists \vec{I}, O: )入力 (\vec{I}) と出力 (O) を見つけ、
( \phi_\mathrm{spec}(\vec{I}, O) )仕様が満たされ
(\land)かつ
( \bigwedge\limits extbackslash_{i=0}^{\vert S \rvert - 1} \left( \vec{I} \neq S_i \right) )例入力セット (S) に既に存在する入力と一致しない。

initial_concrete_inputs メソッドは、このクエリを構築し、Z3に渡し、各発見された例を各クエリの結果モデルから引き出します：

impl<'a> Synthesizer<'a> {
    fn initial_concrete_inputs(
        &mut self,
    ) -> Result<HashSet<Vec<u64>>> {
        // Souperから無遠慮にカーゴカルトしました。
        const NUM_INITIAL_INPUTS: usize = 4;

        let mut inputs: HashSet<Vec<u64>> = 
            HashSet::with_capacity(NUM_INITIAL_INPUTS);

        // 未束縛の入力と出力変数を作成します。
        let input_vars: Vec<_> = (0..self.spec.arity())
            .map(|_| fresh_input(
                self.context,
                FULL_BIT_WIDTH,
            ))
            .collect();
        let output_var = fresh_output(
            self.context,
            FULL_BIT_WIDTH,
        );

        let spec = self.spec.make_expression(
            self.context,
            &input_vars,
            &output_var,
            FULL_BIT_WIDTH,
        );

        for _ in 0..NUM_INITIAL_INPUTS {
            // 新しい入力を一意に見つけるために、入力変数を
            // すでに取得したものと等しくないように制約します。
            let mut existing_inputs = vec![];
            for input_set in &inputs {
                // `eq_this_input` に `var[i] == input_set[i]` のすべての式を構築します。
                let mut eq_this_input = vec![];
                for (inp, var) in input_set
                    .iter()
                    .zip(&input_vars)
                {
                    let inp = BitVec::from_i64(
                        self.context,
                        *inp as i64,
                        FULL_BIT_WIDTH,
                    );
                    eq_this_input.push(inp._eq(var));
                }
                let eq_this_input = and(
                    self.context,
                    &eq_this_input,
                );
                existing_inputs.push(eq_this_input);
            }

            // 新しい入力は、既存の入力のいずれとも等しくない必要があります。
            let not_existing_inputs = or(
                self.context,
                &existing_inputs,
            ).not();

            let query = spec.and(&[
                &not_existing_inputs,
            ]);

            let solver = self.solver();
            solver.assert(&query);

            match solver.check() {
                // 結果が不明な場合、既に取得した例を使用しようとしますが、
                // それがない場合は、ここで終了します。
                z3::SatResult::Unknown => {
                    if inputs.is_empty() {
                        return Err(
                            Error::SynthesisUnknown
                        );
                    } else {
                        break;
                    }
                }

                // クエリが充足不能な場合、私たちの仕様は誤りです。
                z3::SatResult::Unsat => {
                    return Err(
                        Error::SynthesisUnsatisfiable
                    );
                }

                // 例の入力が見つかったので、モデルからそれらを引き出し、セットに追加します。
                z3::SatResult::Sat => {
                    let model = solver.get_model();
                    let new_inputs = eval_bitvecs(
                        &model,
                        &input_vars,
                    );
                    inputs.insert(new_inputs);
                }
            }
        }

        Ok(inputs)
    }
}

さて、内部CEGISループの実装を調べる準備ができました！

注意深い読者は、bit_width パラメータがいたるところで渡されていること、および以前のコードサンプルで FULL_BIT_WIDTH 定数を使用していることに気づいたでしょう。これは、プログラムを最初は狭いビット幅で合成し、その後ターゲットビット幅である FULL_BIT_WIDTH（この実装では32）に達するまで、より広いビット幅で検証するという、よく知られた最適化を実装しているためです。

これはうまく機能します。なぜなら、例えば8ビット幅で正しいプログラムは、32ビット幅でも同様に機能することがよくあるからです。これは「しばしば」であり、「常に」ではありません。合成された定数を広げることは、特に問題になる可能性があります。しかし、より少ないビット数でソルバーが追跡する必要があるため、8ビット幅での合成は32ビット幅での合成よりもはるかに高速です。

より狭いビット幅で合成されたプログラムを検証する場合、その狭いビット幅で検証し、次にその倍のビット幅で検証し、その後再びビット幅を倍増させ、などと続けます。フルビット幅に達するまで続けます。その時点で完了です。検証がカウンター例を見つけるたびに、それ以降は到達した現在のビット幅で合成します。つまり、一度広げた現在のビット幅を狭めることはありません。

impl<'a> Specification<'a> {
    fn synthesize_with_length(
        &mut self,
        program_length: u32,
        inputs: &mut HashSet<Vec<u64>>,
    ) -> Result<Program> {
        let output_line = program_length - 1;
        let mut bit_width = 2;

        'cegis: loop {
            // 有限合成は、現在のビット幅で、私たちの例入力に対して仕様を満たす
            // いくつかの代入を見つけます。
            let assignments = self.finite_synthesis(
                inputs,
                output_line,
                bit_width,
            )?;

            // ここで検証とビット幅拡張ループを開始します。
            loop {
                // 現在のビット幅で代入を検証します。
                match self.verification(
                    &assignments,
                    bit_width,
                )? {
                    // この代入は現在のビット幅ですべての入力に対して機能します！
                    // フルビット幅の場合、答えがあり、完了です。
                    // そうでない場合、ビット幅を倍増させ、新しいビット幅で検証を続けます。
                    Verification::WorksForAllInputs => {
                        if bit_width == FULL_BIT_WIDTH {
                            let program = 
                                assignments.to_program(
                                    self.spec.arity(),
                                    self.library,
                                );
                            return Ok(program);
                        } else {
                            bit_width *= 2;
                        }
                    }

                    // 検証がカウンター例を見つけたので、例入力セットに追加し、
                    // 有限合成を再度試します。
                    Verification::Counterexample(
                        new_inputs
                    ) => {
                        inputs.insert(new_inputs);
                        continue 'cegis;
                    }
                }
            }
        }
    }
}

結果

新しいプログラムシンセサイザーができました。自然な次の質問は、それはどのくらいうまく機能するか？ 他のシンセサイザーと比較してどうですか？ 他のシンセサイザーと同じ数の合成問題を解決できますか？ 他のシンセサイザーと同じくらい速くプログラムを見つけられますか？

まず、私たちのシンセサイザーは、単語の最も右にあるゼロビットを分離するための最適な解を確かに見つけることができます！しかし、複数の最適な解があり、常に私たちが手書きするであろうものと全く同じものを見つけるわけではありません。私たちのシンセサイザーのコストモデル（命令数のみ）によると、常に真を評価するより小さいか等しい比較は、const 1 と同じくらい良いです：

a ← var           // a = 011010011
b ← le_u a, a     // b = 000000001 (つまり `b ← const 1`)
c ← add a, b      // c = 011010100
d ← xor c, a      // d = 000000111
e ← and d, c      // e = 000000100

ふう！

GulwaniらによるSynthesis of Loop-Free Programs論文は、ビット操作のトリック集であるHacker’s Delightから取られた25個のビットベクトル問題のベンチマークスイートを定義しています。彼らはそれを使用してプログラムシンセサイザーBrahmaをベンチマークしています。単語の最も右にあるゼロビットを分離する私たちの実行例は、ベンチマークスイートの7番目の問題です。他のベンチマーク問題には以下が含まれます：

  • 単語の最も右にある1ビットをオフにする、

  • オーバーフローなしで二つの整数の平均を取る、

  • 次の2のべき乗に切り上げる、

  • など…

問題は難易度順に並べられており、最初 の問題は最後 の問題よりもはるかに簡単です。

彼らは、最初の17問には12個の基本的なコンポーネントの標準ライブラリを使用します。最後の8問については、問題に応じて、ライブラリに追加のコンポーネントを追加します。

ベンチマーク問題 を私たちのシンセサイザーにフィードできる Program に移植し、これらの問題の解を再発見するのにかかる時間を測定する小さなランナーを作成しました。

標準ライブラリを私たちのシンセサイザーに移植するには、いくつかの小さな変更が必要でした。例えば、私たちの言語では add 操作に即値（immediate）を許可しないため、彼らの add1 コンポーネントは私たちのライブラリでは二つのコンポーネントになります：add コンポーネントと const 1 コンポーネント。単一のコンポーネントが複数の操作に対応していた場合、他にもいくつか例があります。私たちはそのシナリオをサポートしていないため、それらを移植する際にそれらのコンポーネントを複数のコンポーネントに分割しました。さらに、後 の、より難しい問題については、問題の解決に必要な最小ライブラリを使用しました。なぜなら、これらのより難しい問題は非常に時間がかかる傾向があるからです。

これらのベンチマークでは、OSのパッケージマネージャに含まれるZ3バージョン4.4.1を使用しています。BrahmaはYicesソルバーを使用し、私の理解ではSouperはZ3を含むいくつかの異なるソルバーにプラグインできます。

ここでの私たちの目標は、私たちのシンセサイザーのパフォーマンスの一般的な感覚を得ることだけです。私たちは、私たちのシンセサイザーのパフォーマンスを厳密に評価し、Brahmaと比較しているわけではありません。なぜなら、これはリンゴとリンゴの比較ではないからです。しかし、何かがひどく間違っているという感覚は得るはずです。

すべての問題は1時間のタイムアウトで実行されます。つまり、その時間内に解を見つけられない場合、ギブアップして次の問題に進みます。比較のために、Brahmaが任意の問題にかけた最長時間は46分でした。

まず、各問題について、任意の長さのプログラムを合成するのにかかる時間を測定しました。次に、各問題について最適に短いプログラムを合成するのにかかる時間を測定しました。最後に、最適に短いプログラムと、各 const 操作で使用される定数値の両方を合成するのにかかる時間を測定しました。これは、必要な定数値を const コンポーネントの一部として与えるのではなく、です。

結果は次の表にまとめられており、論文で彼らのBrahmaシンセサイザーの結果とともに示されています。時間は秒単位です。

ベンチマークBrahma私たちのシンセサイザー任意の長さ最小長最小長 & 合成定数
p13.20.5109.0170.4
p23.61.1136.099.4
p31.40.632.831.9
p43.30.5100.5130.1
p52.20.3125.2119.2
p62.40.696.387.7
p71.00.5100.180.3
p81.41.090.577.6
p95.836.5241.4165.6
p1076.16.834.242.1
p1157.14.131.936.9
p1267.811.530.652.8
p136.220.9129.7165.0
p1459.685.11328.71598.8
p15118.920.01897.31742.7
p1662.325.23600.0*3600.0*
p1778.18.2102.0243.5
p1845.91.527.433.5
p1934.73.310.06.0
p20108.4757.53600.1*3600.0*
p2128.3timeouttimeouttimeout
p22279.0timeouttimeouttimeout
p231668.0Z3 crashtimeouttimeout
p24224.9timeouttimeouttimeout
p252778.7timeouttimeouttimeout
  • これらの問題では、シンセサイザーは* a *ソリューションを見つけましたが、必ずしも最適に短いソリューションではありませんでした。検索を完了する前にタイムアウトしたため、より小さいプログラムの存在を発見または除外できませんでした。

簡単で初期の問題については、私たちのシンセサイザーはかなりうまく機能します。最適に短いプログラムを見つけるには、任意の長さのプログラムを見つけるよりもはるかに時間がかかります。定数を合成することは、最適な短いプログラムを見つけることに対する合成のオーバーヘッドをほとんど追加しないようです。私たちのシンセサイザーは、問題20と21あたりで一種の崖にぶつかり、実行時間が急増し、タイムアウト上限に達し始めます。

問題23は、popcountの実装を合成することです。Brahmaはわずか28分未満で問題を解決します。Souperの担当者は、彼らもこの問題を解決できると述べていますが、彼らのシンセサイザーはBrahmaほどスケーラブルではないと述べています。私がこのベンチマークを実行していたとき、Z3は有限合成クエリを解決しようとしている間に繰り返しクラッシュしました。最終的に、シンセサイザーは問題を完了できませんでした。開発中にZ3がクラッシュしなかった以前のバージョンのシンセサイザーでこの問題を実行しましたが、それでもpopcountのプログラムを合成できませんでした。シンセサイザーをほぼ3日間実行しましたが、できませんでした。

YicesはZ3よりもこれらの種類のクエリを解決するのに優れているのでしょうか？ これらのクエリをソルバーが解決しやすくするための、よく知られた最適化があるのでしょうか？ 私が知らないだけでしょうか？ 複合コンポーネントが私たちのライブラリで複数のコンポーネントに分割され、より大きなライブラリと解決すべきより多くの位置変数につながるという事実は、問題の根源でしょうか？ 分かりません。

このプロジェクトの唯一の失望は、より大きな合成問題におけるこのパフォーマンスの崖です。シンセサイザーがこの崖から落ちる理由、またはZ3をプロファイリングしてこれらのクエリで苦労している理由を掘り下げる方法についてアイデアがある場合は、ぜひお聞かせください。特に、この種の問題合成の経験がある場合は。SMTソルバーは現時点では私にとって非常にブラックボックスです。

結論

反例導出型反復合成は、SMTソルバーが解決するには難しすぎる単一の問題を、市販のソルバーが処理できる複数の小さな問題に変換する、驚くほど巧妙な方法です。コンポーネントベースプログラムの表現を、SMTクエリ内で完全に表現できるように位置マッピングに反転させることも同様に巧みです。

プログラム合成（プログラムを書くプログラムを書くこと）は、メタ的でウロボロス的な意味で、楽しくて素晴らしいです。また、最適化コンパイラのバックエンドの大部分を機械的に生成できる未来を予示しています。実際に最適なコードシーケンスを生成するコンパイラの未来。私はその高尚な約束に興奮していますが、SMTソルバーのパフォーマンスに対する洞察力の欠如にも不満を感じています。SMTソルバーのみに依存するのではなく、検証のみに依存するプログラム合成のアプローチも存在します。しかし、BrahmaとSouperの結果を再現するまで、このアプローチを諦めるのは時期尚早のように思えます。それにもかかわらず、私は楽観的であり、これらの不一致を解決するまで掘り下げるつもりです。

読んでくれてありがとう！

参考文献

  • fitzgen/synth-loop-free-prog: この投稿で説明されているシンセサイザーのGitリポジトリ！

  • Synthesis of Loop-Free Programs by Gulwani et al: この投稿の大部分の基盤となっている論文です！素晴らしい論文なので、興味を持った方はぜひ読んでみてください！

  • Program Synthesis by Gulwani et al: プログラム合成の最先端技術をまとめたサーベイ論文です。分野全体の概要を素早く把握するのに最適です！

  • A Synthesizing Superoptimizer by Sasnauskas et al: この論文は、プログラム合成をコアとして使用するLLVMのスーパーオプティマイザーであるSouperを説明しています。SouperのシンセサイザーもGulwani論文に基づいていますが、いくつかの異なる方法で拡張されています。ソースコードをかなり調べて、最適化やトリックを見つけました！

  • Automatic Generation of Peephole Superoptimizers by Bansal et al: スーパーオプティマイザーを使用してオフラインでテーブル駆動型ピーホールオプティマイザーを生成する方法を説明した最初の論文。

  • Hacker’s Delight by Henry S. Warren: コンパクトで非自明なビット操作トリックに特化した書籍です。そのようなものに興味があるなら、信じられないほどの本です！ Synthesis of Loop-Free Programs 論文で提示されているベンチマーク問題は、この本から取られています。

  • SyGuS: SyGuS、または構文ガイド付き合成は、一連のプログラム合成問題を形式化し、それらを記述するための言語を標準化し、シンセサイザーの年次コンペティションを開催します。目標は、少しの友好的な競争で分野のイノベーションを推進することです。