在程序合成的浩瀚领域中，如何高效地选择合适的工具和方法来解决问题，一直是一个令人头疼的挑战。面对多样化的合成任务、不同的语言模型（LLMs）以及各种提示风格，研究者们提出了一个创新的解决方案——CYANEA。这一方法不仅在性能上超越了单一求解器，还通过多臂老虎机（Multi-Armed Bandit, MAB）算法实现了动态的求解器和提示选择。本文将带您深入 CYANEA 的算法核心，揭示其实现细节与独特魅力。 --- ## 🌟 **程序合成的背景与挑战** 程序合成是一项看似简单却极具挑战的任务：根据给定的规范，自动生成满足条件的代码或表达式。形式化地说，程序合成问题可以表示为一个三元组 [imath:0]\langle \tau, f, \phi \rangle[/imath:0]，其中 [imath:0]\tau[/imath:0] 是背景理论，[imath:0]f[/imath:0] 是待合成的函数，而 [imath:0]\phi[/imath:0] 是一个无量词公式。目标是找到一个函数体，使得公式 [imath:0]\forall x. \phi(f)[/imath:0] 成立。然而，现实中的合成任务往往复杂多样。即使是当前表现优异的大型语言模型（LLMs），在面对不同任务时的表现也参差不齐。用户不仅需要选择合适的 LLM，还需要设计高效的提示（Prompt）。此外，调用 LLM 的成本（计算成本和经济成本）也不容忽视。因此，如何在多种选择中找到最优解，成为了一个亟待解决的问题。 --- ## 🤖 **CYANEA 的核心：多臂老虎机算法** CYANEA 的核心思想是将求解器选择问题建模为一个 **多臂老虎机问题**（Multi-Armed Bandit, MAB）。在这个问题中，每个求解器（包括 LLM-提示组合和符号求解器）被视为一个老虎机臂，目标是通过试探和利用，找到能够最大化奖励的选择。 ### **单层多臂老虎机** CYANEA 的第一种实现方式是单层多臂老虎机（Single-Layer MAB）。在这种结构中，所有的求解器（包括符号求解器和 LLM-提示组合）被统一建模为一个选择集合。每次选择时，算法根据上下文特征预测各求解器的表现，并按照奖励函数对它们进行排序。 **算法流程：** 1. **特征化（Featurize）** 输入一个合成任务 [imath:0]q[/imath:0]，将其转化为特征向量 [imath:0]\vec{f}[/imath:0]。特征包括 SMT-LIB 关键字的频率、约束长度、常量数量、逻辑类型等。 2. **求解器预测（Solver Predictor）** 使用 k-最近邻（k-NN）算法，根据特征向量 [imath:0]\vec{f}[/imath:0]，预测求解器的排名。k-NN 的核心思想是通过计算特征向量之间的欧几里得距离，找到最相似的历史任务，并根据这些任务的求解器表现进行预测。 3. **时间与成本分配（Time and Cost Allocation）** 根据预测的排名，为每个求解器分配时间和成本预算。分配策略基于指数分布的最大似然估计（MLE），确保大部分预算用于最有可能成功的求解器。 4. **求解器部署（Deploy Solvers）** 按照分配的预算顺序调用求解器，直到任务被解决或预算耗尽。 --- ### **多层多臂老虎机** 为了进一步优化提示选择，CYANEA 提出了多层多臂老虎机（Multi-Layer MAB）。在这种结构中，第一层老虎机负责选择求解器（符号求解器或 LLM），而第二层老虎机则专注于为选定的 LLM 选择最佳提示风格。 **算法流程：** 1. **第一层选择：求解器类型** 第一层多臂老虎机根据特征向量 [imath:0]\vec{f}[/imath:0]，在符号求解器和 LLM 之间进行选择。 2. **第二层选择：提示风格** 如果第一层选择了 LLM，则进入第二层多臂老虎机。第二层根据特征向量，为选定的 LLM 选择最合适的提示风格。 3. **反馈与更新** 每次任务完成后，算法会记录求解器的表现（包括是否成功、所需时间和成本），并将这些数据反馈给对应的多臂老虎机，用于更新其预测模型。 --- ## 🔍 **提示风格的多样性** CYANEA 的成功离不开对提示风格的精心设计。研究者们总结了文献中常见的提示策略，并将其整合为一个提示库。以下是几种关键提示风格： 1. **自然语言提示（Natural Language Prompts）** 将逻辑约束转化为自然语言描述，例如“请合成一个函数，使其满足以下约束……”。 2. **少样本提示（Few-Shot Prompting）** 提供 3 个已解决任务的示例，帮助 LLM 理解任务模式。 3. **高资源语言提示（Higher Resource Language Prompts）** 使用 Lisp 等高资源语言生成初始解，然后将其翻译为目标语言（如 SyGuS-IF）。 4. **角色提示（Role-Based Prompts）** 在提示中加入角色描述，例如“你是一位优秀的程序合成专家”。 5. **情感刺激（Emotional Stimuli）** 在提示中加入情感化语言，例如“请不要让我失望”。 --- ## 📊 **时间与成本分配的优化** CYANEA 的另一个亮点是其动态的时间与成本分配策略。研究者假设求解器的运行时间和成本服从指数分布，并通过最大似然估计（MLE）计算分布参数。具体公式如下： - 时间分配： [math:0]t_i = -\frac{\ln(\delta + e^{-\lambda^* T})}{\lambda^*}[/math:0] 其中，[imath:0]\lambda^*[/imath:0] 是基于历史数据估计的分布参数，[imath:0]T[/imath:0] 是总时间预算。 - 成本分配： [math:0]c_i = -\frac{\ln(\delta + e^{-\lambda^* C})}{\lambda^*}[/math:0] 其中，[imath:0]C[/imath:0] 是总成本预算。通过这种方法，CYANEA 能够在有限的预算内最大化求解器的表现。 --- ## 🎯 **实验与性能分析** 研究者使用 CYANEA 对 1269 个合成任务进行了测试，任务来源包括 Syntax-Guided Synthesis 竞赛、排名函数合成文献以及 SMT 竞赛生成的任务。实验结果表明： - CYANEA 在解决任务数量上比最佳单一求解器提升了 **37.2%**。 - CYANEA 的表现接近虚拟最佳求解器（Virtual Best Solver），仅差 **4%**。 - 在时间和成本预算的优化上，CYANEA 的 Par-2 分数（越低越好）显著优于单一求解器。 --- ## 🧠 **总结与展望** CYANEA 的提出为程序合成领域带来了全新的视角。通过多臂老虎机算法，CYANEA 实现了动态的求解器和提示选择，在性能和成本之间找到了平衡。未来，CYANEA 的框架可以进一步扩展，例如引入更多类型的求解器或优化特征提取方法。在程序合成的旅途中，CYANEA 无疑是一位值得信赖的智囊团。它不仅让复杂的选择问题变得简单，还为我们展示了算法与实践结合的无限可能。 --- ## 📚 **参考文献** 1. Li, Y., Frampton, L., Mora, F., & Polgreen, E. (2025). Online Prompt and Solver Selection for Program Synthesis. *Proceedings of AAAI*. 2. Alur, R., et al. (2024). Syntax-Guided Synthesis Competition. 3. Giacobbe, M., Kroening, D., & Parsert, N. (2022). Ranking Function Synthesis. 4. Solar-Lezama, A., et al. (2006). CounterExample Guided Inductive Synthesis (CEGIS). 5. Lee, C., et al. (2018). Euphony: A Sound and Complete Enumerative Solver.

程序合成的智囊团：CYANEA 的诞生与算法揭秘

步子哥

在程序合成的浩瀚领域中，如何高效地选择合适的工具和方法来解决问题，一直是一个令人头疼的挑战。面对多样化的合成任务、不同的语言模型（LLMs）以及各种提示风格，研究者们提出了一个创新的解决方案——CYANEA。这一方法不仅在性能上超越了单一求解器，还通过多臂老虎机（Multi-Armed Bandit, MAB）算法实现了动态的求解器和提示选择。本文将带您深入 CYANEA 的算法核心，揭示其实现细节与独特魅力。

🌟 程序合成的背景与挑战

程序合成是一项看似简单却极具挑战的任务：根据给定的规范，自动生成满足条件的代码或表达式。形式化地说，程序合成问题可以表示为一个三元组 \langle \tau, f, \phi \rangle，其中 \tau 是背景理论，f 是待合成的函数，而 \phi 是一个无量词公式。目标是找到一个函数体，使得公式 \forall x. \phi(f) 成立。

然而，现实中的合成任务往往复杂多样。即使是当前表现优异的大型语言模型（LLMs），在面对不同任务时的表现也参差不齐。用户不仅需要选择合适的 LLM，还需要设计高效的提示（Prompt）。此外，调用 LLM 的成本（计算成本和经济成本）也不容忽视。因此，如何在多种选择中找到最优解，成为了一个亟待解决的问题。

🤖 CYANEA 的核心：多臂老虎机算法

CYANEA 的核心思想是将求解器选择问题建模为一个 多臂老虎机问题（Multi-Armed Bandit, MAB）。在这个问题中，每个求解器（包括 LLM-提示组合和符号求解器）被视为一个老虎机臂，目标是通过试探和利用，找到能够最大化奖励的选择。

单层多臂老虎机

CYANEA 的第一种实现方式是单层多臂老虎机（Single-Layer MAB）。在这种结构中，所有的求解器（包括符号求解器和 LLM-提示组合）被统一建模为一个选择集合。每次选择时，算法根据上下文特征预测各求解器的表现，并按照奖励函数对它们进行排序。

算法流程：

特征化（Featurize）
输入一个合成任务 q，将其转化为特征向量 \vec{f}。特征包括 SMT-LIB 关键字的频率、约束长度、常量数量、逻辑类型等。
求解器预测（Solver Predictor）
使用 k-最近邻（k-NN）算法，根据特征向量 \vec{f}，预测求解器的排名。k-NN 的核心思想是通过计算特征向量之间的欧几里得距离，找到最相似的历史任务，并根据这些任务的求解器表现进行预测。
时间与成本分配（Time and Cost Allocation）
根据预测的排名，为每个求解器分配时间和成本预算。分配策略基于指数分布的最大似然估计（MLE），确保大部分预算用于最有可能成功的求解器。
求解器部署（Deploy Solvers）
按照分配的预算顺序调用求解器，直到任务被解决或预算耗尽。

多层多臂老虎机

为了进一步优化提示选择，CYANEA 提出了多层多臂老虎机（Multi-Layer MAB）。在这种结构中，第一层老虎机负责选择求解器（符号求解器或 LLM），而第二层老虎机则专注于为选定的 LLM 选择最佳提示风格。

算法流程：

第一层选择：求解器类型
第一层多臂老虎机根据特征向量 \vec{f}，在符号求解器和 LLM 之间进行选择。
第二层选择：提示风格
如果第一层选择了 LLM，则进入第二层多臂老虎机。第二层根据特征向量，为选定的 LLM 选择最合适的提示风格。
反馈与更新
每次任务完成后，算法会记录求解器的表现（包括是否成功、所需时间和成本），并将这些数据反馈给对应的多臂老虎机，用于更新其预测模型。

🔍 提示风格的多样性

CYANEA 的成功离不开对提示风格的精心设计。研究者们总结了文献中常见的提示策略，并将其整合为一个提示库。以下是几种关键提示风格：

自然语言提示（Natural Language Prompts）
将逻辑约束转化为自然语言描述，例如“请合成一个函数，使其满足以下约束……”。
少样本提示（Few-Shot Prompting）
提供 3 个已解决任务的示例，帮助 LLM 理解任务模式。
高资源语言提示（Higher Resource Language Prompts）
使用 Lisp 等高资源语言生成初始解，然后将其翻译为目标语言（如 SyGuS-IF）。
角色提示（Role-Based Prompts）
在提示中加入角色描述，例如“你是一位优秀的程序合成专家”。
情感刺激（Emotional Stimuli）
在提示中加入情感化语言，例如“请不要让我失望”。

📊 时间与成本分配的优化

CYANEA 的另一个亮点是其动态的时间与成本分配策略。研究者假设求解器的运行时间和成本服从指数分布，并通过最大似然估计（MLE）计算分布参数。具体公式如下：

时间分配：
t_i = -\frac{\ln(\delta + e^{-\lambda^* T})}{\lambda^*}
其中，\lambda^* 是基于历史数据估计的分布参数，T 是总时间预算。
成本分配：
c_i = -\frac{\ln(\delta + e^{-\lambda^* C})}{\lambda^*}
其中，C 是总成本预算。

通过这种方法，CYANEA 能够在有限的预算内最大化求解器的表现。

🎯 实验与性能分析

研究者使用 CYANEA 对 1269 个合成任务进行了测试，任务来源包括 Syntax-Guided Synthesis 竞赛、排名函数合成文献以及 SMT 竞赛生成的任务。实验结果表明：

CYANEA 在解决任务数量上比最佳单一求解器提升了 37.2%。
CYANEA 的表现接近虚拟最佳求解器（Virtual Best Solver），仅差 4%。
在时间和成本预算的优化上，CYANEA 的 Par-2 分数（越低越好）显著优于单一求解器。

🧠 总结与展望

CYANEA 的提出为程序合成领域带来了全新的视角。通过多臂老虎机算法，CYANEA 实现了动态的求解器和提示选择，在性能和成本之间找到了平衡。未来，CYANEA 的框架可以进一步扩展，例如引入更多类型的求解器或优化特征提取方法。

在程序合成的旅途中，CYANEA 无疑是一位值得信赖的智囊团。它不仅让复杂的选择问题变得简单，还为我们展示了算法与实践结合的无限可能。

📚 参考文献

Li, Y., Frampton, L., Mora, F., & Polgreen, E. (2025). Online Prompt and Solver Selection for Program Synthesis. Proceedings of AAAI.
Alur, R., et al. (2024). Syntax-Guided Synthesis Competition.
Giacobbe, M., Kroening, D., & Parsert, N. (2022). Ranking Function Synthesis.
Solar-Lezama, A., et al. (2006). CounterExample Guided Inductive Synthesis (CEGIS).
Lee, C., et al. (2018). Euphony: A Sound and Complete Enumerative Solver.