核心概念
LLMと列挙アルゴリズムの統合により、形式的プログラム合成の性能向上が可能である。
要約
大規模言語モデル(LLMs)を使用して形式的プログラム合成問題を解決する方法に焦点を当てた研究。LLMsは自然言語仕様や入出力例に基づいたベンチマークで印象的な結果を達成しており、この研究ではその有効性を評価。提案手法は、LLMが正しい解決策を提案できない場合、列挙型シンセサイザーを導入し、解決領域を重点的に探索することで性能向上を実現。さらに、LLMから得られた情報を用いて列挙アルゴリズムの性能向上も図っている。
統計
LLMが49%のベンチマーク問題を解決(平均4回の試行)
pCFG-synthは30%の追加問題を解決
iLLM-synthはcvc5と同等のパフォーマンス
引用
"Enumerative synthesis is not yet obsolete!"
"Our results demonstrate that, whilst large language models do have the potential to make significant contributions in the domain of formal program synthesis, this can currently only be achieved by combining these techniques with existing algorithms in the literature."