程序综合的在线提示选择

大型语言模型（Large Language Model, LLM）在程序综合领域展现出惊人的能力。然而，这种性能并非在所有任务、所有LLM和所有提示样式下都通用。许多情况下，一个LLM占主导，一个提示样式占主导，或者调用符号求解器比LLM更合适。用户的关键挑战在于，既要识别LLM何时是正确求解器选择，又要确定针对给定综合任务的最佳LLM及其调用方式。非专业用户若做出错误选择，将在结果（解决任务数量和解决时间）和财务成本（若使用商业API）方面受到影响。我们将此问题建模为在线学习问题。我们采用多臂老虎机算法（multi-armed bandit algorithm）来选择调用哪个符号求解器、LLM及其提示组合，以最大化给定奖励函数（可能优先考虑解决时间、解决任务数量或财务成本）。我们实现了一个名为CYANEA的实例，并在来自文献的排序函数综合、来自语法引导综合竞赛的查询，以及从SMT问题生成的 fresh、未见查询中进行评估。CYANEA解决的查询数量比最佳单一求解器高出37.2%，并在距离虚拟最佳求解器仅4%的范围内取得好结果。