e4exp
commented
3 years ago 結論
我々は、ニューラルネットワークをグレイボックスとして用いて論理式を合成する新しい手法を提案した。 我々の重要な洞察は、NNが抽出を念頭に置いて適切に設計されていれば、訓練されたNNから有用な情報を抽出することができるはずだということである。 私たちの予備実験の結果は非常に有望です。 また、我々のNNガイド付き合成を、（CHCの解法による）プログラム検証や（オラクルベースのプログラミングという概念による）プログラム合成に応用する可能性についても議論しました。 我々は予備的な実験を行いましたが、これらのアプリケーションにおける我々の合成ツールの完全な統合は、将来の課題として残されています。 プログラムの検証と合成は、学習データを自動的に収集することができるため、ニューラルネットワーク（および一般的な機械学習）の魅力的な応用分野であると考えています。 今後は、NNガイド付き合成ツールを拡張し、 (i)非ブール値（整数など）を返す関数、 (ii)再帰的データ構造上の述語・関数、 (iii)ループを含むプログラム式の合成を可能にする予定です。
ii）と（iii）については、リカレント・ニューラル・ネットワークの導入を予定しています。 また、オラクルベースのプログラミングでは、NNの学習に強化学習を採用することを予定しています。
本研究では、プログラムと不変量を合成するための新しいフレームワーク「Neural Network-guided Synthesis」を提案する。 まず、ニューラルネットワークを適切に設計・学習することで、学習したニューラルネットワークの重みやバイアスから整数に対する論理式を抽出できることを示す。 このアイデアに基づいて、正負の例と含意制約から数式を合成するツールを実装し、有望な実験結果を得た。 また、我々の合成方法の2つの応用例についても述べる。 一つは、ICE学習に基づくCHC解法の枠組みの中で、我々のツールを修飾子発見のために使用することであり、これは、プログラム検証や帰納的不変量合成にも応用できる。 もう一つの応用は、オラクルベースのプログラミングと呼ばれる新しいプログラム開発のフレームワークであり、Solar-Lezamaのスケッチによるプログラム合成をニューラルネットワークで誘導したものである。