Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis

要約

プログラム合成とは、仕様に基づいてコードを自動生成する作業です。
構文ガイド付き合成 (SyGuS) では、この仕様は構文テンプレートと論理式の組み合わせであり、結果が両方を満たすことが保証されます。
モンテカルロ木探索 (MCTS) を使用して候補解の空間を検索する、SyGuS の強化学習ガイド付きアルゴリズムを紹介します。
私たちのアルゴリズムはポリシーと価値関数を学習し、ツリーの信頼限界と組み合わせることで、探索と活用のバランスをとることができます。
機械学習アプローチを構文誘導合成に適用する際の共通の課題は、トレーニング データの不足です。
これに対処するために、MCTS ポリシーのトレーニングに使用する、既存の一次充足可能性問題の反統一に基づいて SyGuS のトレーニング データを自動的に生成する方法を紹介します。
この設定を実装して評価し、学習したポリシーと値により、トレーニング セットとテスト セットでベースラインよりも 26 パーセント以上合成パフォーマンスが向上することを実証します。
私たちのツールは、トレーニング セットで最先端のツール cvc5 を上回り、テスト セットで解決された問題の総数という点では同等のパフォーマンスを示しました (cvc5 が失敗するベンチマークの 23% を解決しました)。
SyGuS 問題への機械学習手法のさらなる適用を可能にするために、データセットを公開します。

要約(オリジナル)

Program synthesis is the task of automatically generating code based on a specification. In Syntax-Guided Synthesis (SyGuS) this specification is a combination of a syntactic template and a logical formula, and the result is guaranteed to satisfy both. We present a reinforcement-learning guided algorithm for SyGuS which uses Monte-Carlo Tree Search (MCTS) to search the space of candidate solutions. Our algorithm learns policy and value functions which, combined with the upper confidence bound for trees, allow it to balance exploration and exploitation. A common challenge in applying machine learning approaches to syntax-guided synthesis is the scarcity of training data. To address this, we present a method for automatically generating training data for SyGuS based on anti-unification of existing first-order satisfiability problems, which we use to train our MCTS policy. We implement and evaluate this setup and demonstrate that learned policy and value improve the synthesis performance over a baseline by over 26 percentage points in the training and testing sets. Our tool outperforms state-of-the-art tool cvc5 on the training set and performs comparably in terms of the total number of problems solved on the testing set (solving 23% of the benchmarks on which cvc5 fails). We make our data set publicly available, to enable further application of machine learning methods to the SyGuS problem.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google