Online Prompt and Solver Selection for Program Synthesis

要約

大規模言語モデル (LLM) は、プログラム合成の領域で優れた機能を実証します。
ただし、このレベルのパフォーマンスは、すべてのタスク、すべての LLM、すべてのプロンプト スタイルに共通するものではありません。
1 つの LLM が優勢である領域、1 つのプロンプト スタイルが優勢な領域、または LLM よりもシンボリック ソルバーを呼び出す方が良い選択肢である領域は数多くあります。
ユーザーにとっての重要な課題は、LLM がソルバーの正しい選択であるかどうか、特定の合成タスクを呼び出すのに適切な LLM だけでなく、それを呼び出す正しい方法も特定することです。
非専門家ユーザーが間違った選択をすると、商用 API を介してクローズドソース言語モデルを使用する場合、結果 (解決されたタスクの数と解決にかかる時間) と金銭的コストの両方の面でコストが発生します。
。
私たちはこの選択をオンライン学習の問題として組み立てます。
マルチアーム バンディット アルゴリズムを使用して、特定の報酬関数 (解決時間、解決された合成タスクの数、または解決の財務コストを優先する場合があります) を最大化するために展開するシンボリック ソルバー、つまり LLM とプロンプトの組み合わせを選択します。
私たちは、CYANNEA と呼ばれるこのアプローチのインスタンスを実装し、ランキング関数合成の文献からの合成クエリ、構文ガイド付き合成競合からの合成クエリ、および SMT 問題から生成された新しい未知のクエリに対して評価します。
CYANNEA は、最高の単一ソルバーよりも 37.2\% 多くのクエリを解決し、仮想最高のソルバーの 4\% 以内の結果を達成します。

要約(オリジナル)

Large Language Models (LLMs) demonstrate impressive capabilities in the domain of program synthesis. This level of performance is not, however, universal across all tasks, all LLMs and all prompting styles. There are many areas where one LLM dominates, one prompting style dominates, or where calling a symbolic solver is a better choice than an LLM. A key challenge for the user then, is to identify not only when an LLM is the right choice of solver, and the appropriate LLM to call for a given synthesis task, but also the right way to call it. A non-expert user who makes the wrong choice, incurs a cost both in terms of results (number of tasks solved, and the time it takes to solve them) and financial cost, if using a closed-source language model via a commercial API. We frame this choice as an online learning problem. We use a multi-armed bandit algorithm to select which symbolic solver, or LLM and prompt combination to deploy in order to maximize a given reward function (which may prioritize solving time, number of synthesis tasks solved, or financial cost of solving). We implement an instance of this approach, called CYANEA, and evaluate it on synthesis queries from the literature in ranking function synthesis, from the syntax-guided synthesis competition, and fresh, unseen queries generated from SMT problems. CYANEA solves 37.2\% more queries than the best single solver and achieves results within 4\% of the virtual best solver.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google