{"id":"c846a5b3-a180-4f84-9a87-bcbe88009405","arxiv_id":"2501.05247","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"An online multi-armed bandit that selects among symbolic solvers and LLM-prompt combinations for program synthesis solves 37.2% more queries than the best single solver and reaches 96% of the virtual best solver's performance.","lead":"The paper presents CYANEA, a system that automatically decides, for each program-synthesis query, whether to call a symbolic solver or an LLM and which prompt style to use, treating the choice as an online learning problem. In tests on 1,269 synthesis problems, it solved 37% more queries than the best single solver and came within 4% of an oracle that always picks the perfect solver.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Missing context-free baseline leaves open that CYANEA's gains come from portfolio diversity and budget allocation, not the learned online prompt selection.","rationale":"The paper's numbers are internally consistent (Par-2 values match solve counts and times), and the 20-run average with standard deviation is a reasonable attempt to control for query order. The main claim is a comparative empirical statement, and the comparison to the best single solver is a strong baseline. However, the evaluation misses the one control needed to attribute the result to the proposed method: a non-contextual or fixed-order portfolio that uses the same solver library and budget allocator. Without this, the 37.2% improvement over the best single solver could be simply the benefit of running a diverse set of solvers sequentially within the same budget, which is a known portfolio effect. The 'linear' variant in Table 2 is still contextual, so it does not control for the k-NN ranking. This is particularly important because the paper's contribution is framed as online learning and prompt selection, not as a static portfolio. Additionally, the feature vector is too loosely specified to be reimplemented; the 'cartesian distance' over raw keyword counts, query length, constants, and query logic is not well-defined without the exact encoding and normalization. If the distance is dominated by query length, the k-NN's nearest neighbours may not be semantically similar, and the good performance would be brittle. A concrete test that adds a fixed-order baseline, a UCB1 baseline, and a normalized-feature run would settle both the attribution and the feature-robustness questions. Given these gaps, the CONDITIONAL verdict remains appropriate; the paper should be asked to supply these controls and a precise feature specification before the central claim is fully supported.","tokens_in":11977,"tokens_out":15421,"duration_ms":147743,"concrete_test":"Implement two additional baselines using the same 13 solvers, T=100s, C=100,000, and the same exponential budget allocator: (a) a fixed order sorted by each solver's overall solve rate on the full benchmark, and (b) a non-contextual UCB1 bandit updated online over the solver set. Run both on the same 20 shuffled orders and compare solved-query counts to the reported 88.3% (1120.6). If either baseline reaches at least 87% (1104), the contextual k-NN ranking is not the driver of the gain; if they fall below roughly 80% (1015), the mechanism is validated. Also rerun the k-NN with z-scored features to test whether Euclidean distance on raw counts is dominated by query length; if normalized-feature results differ materially, the published feature definition is insufficient.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that CYANEA's online, contextual selection of solvers and prompts solves 37.2% more queries than the best single solver and reaches within 4% of the virtual best (Section 7, Table 2). The evaluation compares CYANEA to individual solvers, a virtual best, and a 'linear' budget-allocation variant that still uses the k-NN ranking. There is no baseline that removes the learned context: no fixed solver order, no non-contextual bandit, no random ordering. Without such a baseline, the observed solve rate could be driven by (i) the diversity of the 13-solver portfolio and (ii) the exponential budget allocator, rather than by the k-NN feature-based ranking. Indeed, single k-NN with linear budgets still solves 87.0% (Table 2), only 1.3 points below the reported best, which suggests ranking quality alone contributes little. Furthermore, the feature vector is underspecified: 'Keywords: Frequencies of specific SMT-LIB keywords (e.g., +, −, ∗, div, etc.)' with no list of keywords, no encoding for 'Query logic', and no mention of normalization; Euclidean ('cartesian') distance over such heterogeneous raw counts is likely dominated by query length. If so, the 'nearest neighbours' are nearest in length, not in problem structure, and the contextual mechanism's success on this benchmark may not transfer. The absence of code or a precise feature specification makes these concerns untestable from the paper alone. The load-bearing assumption is that the contextual k-NN ranking materially outperforms a non-contextual or fixed-order portfolio; this is currently unsupported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes CYANEA, a system that frames solver and prompt selection for program synthesis as an online contextual multi-armed bandit problem. Given a set of synthesis queries, CYANEA featurizes each SyGuS-IF query, uses k-NN with hand-designed features to rank a portfolio of 13 solvers (12 LLM-prompt pairs plus an enumerative solver), and allocates time and token budgets across the ranked solvers before deploying them sequentially. The evaluation on 1,269 queries from SyGuS, ranking-function synthesis, and SMT-derived benchmarks reports that the best CYANEA instance solves 88.3% of queries, versus 64.3% for the best single solver and 91.8% for a virtual best solver, with results averaged over 20 randomly shuffled runs. The paper also compares single-layer versus double-layer bandit architectures and reward functions for time, cost, and binary solve success.","tokens_in":12237,"tokens_out":7716,"duration_ms":76867,"significance":"If the result holds, the paper addresses a practical and timely problem: non-expert users of LLM-based synthesis must choose not only between symbolic solvers and LLMs but also among LLMs and prompting styles. The evaluation is substantial for an empirical systems paper: 1,269 queries, 20 shuffled runs, reported standard deviations, a virtual-best upper bound, and a parameter sweep showing stability for k in 10-15. The framing as an online learning problem is appropriate, and the paper does not overclaim the ability of any single LLM. However, the central attribution of the gains to the learned contextual ranking is not established, because no baseline removes the learned context while keeping the same portfolio and budget allocator, and the feature representation is too underspecified to support the claimed transferability.","major_comments":[{"comment":"The evaluation lacks a baseline that removes the learned contextual ranking. The 'Single k-NN linear' rows solve 87.0% of queries (1104±0), while the exponential-allocation 'Single k-NN' rows solve about 88.1-88.3%; the difference is only about 1.3 percentage points, yet both variants use the same k-NN ranking. The zero standard deviation of the linear rows is consistent with a regime in which most or all solvers are attempted on every query, making the learned ordering almost irrelevant. To support the paper's central claim that online contextual selection drives the improvement, please add a fixed-order baseline, a random-order baseline, and a non-contextual bandit (e.g., UCB without features) using the same budget allocator, and report the resulting solve rates and scores.","section":"Section 5, Features"},{"comment":"The feature vector is underspecified and its predictive power is not demonstrated. The paper lists 'Keywords: Frequencies of specific SMT-LIB keywords (e.g., +, -, *, div, etc.)', 'Query length', 'Constants', and 'Query logic', but does not give the actual keyword list, the encoding of 'Query logic', or any normalization scheme. Euclidean ('cartesian') distance over raw counts of heterogeneous features is likely dominated by query length, in which case the 'nearest neighbours' are nearest in length rather than in problem structure. Please provide the exact feature construction and add an ablation comparing full features against length-only or random features to show that the contextual mechanism, rather than the budget allocator or portfolio composition, is responsible for the reported gains.","section":"Section 5, k-Nearest Neighbor"},{"comment":"The ranking procedure is incompletely specified. The text states that the score for a solver is the sum of rewards over the k nearest previously solved queries, but it does not state how ties are broken or how the final ordering is made deterministic; it says only that solvers absent from the k-neighbor set are randomly shuffled and appended. With 13 solvers and k=15, many solvers may receive zero score on a given query, so the random component could be substantial. Please specify the exact tie-breaking and shuffling procedure, and report the variance attributable to this randomness separately from the variance due to query order.","section":"Section 5, Time and Token Budget Allocation"}],"minor_comments":[{"comment":"The sentence claiming that 'the highest number of queries solved is achieved using rb' is contradicted by Table 2, where Single k-NN (rc) solves 1120.6 queries and Single k-NN (rb) solves 1117.5; likewise, the claim that rt gives the best Par-2 score is contradicted by rc's Par-2 score of 37636.3 versus rt's 37813.7.","section":"Section 7, Reproducibility"},{"comment":"No code, complete prompt templates, or feature-extraction code are released. Given that the paper is an empirical systems paper and that the feature and prompt definitions are not fully specified, this severely limits independent verification of the reported 20-run results.","section":"Section 5, Time and Token Budget Allocation"},{"comment":"The parameters δ1 and δ2 are introduced in the budget-allocation derivation but no numeric values are reported, and the formula for c_i appears to use δ rather than δ2. Please state the values used in the experiments and clarify the notation.","section":"Section 5, Reward functions"},{"comment":"Several constants that could affect the results are not swept or otherwise justified: the reward exponent 4, the output-token cost multiplier 3, the enumerative solver fixed cost 0.4, the 'up to 16 attempts' limit, and the total budgets T=100 and C=100,000. At minimum, a sensitivity analysis for the reward exponent and the cost multiplier would help establish that the headline solve rate is not an artifact of these choices.","section":"Table 2"}],"recommendation":"major_revision","confidential_remarks":"The main technical reservation is attribution: the 37.2% improvement over the best single solver may be driven largely by portfolio diversity and the budget allocator rather than by the learned contextual ranking, since the linear-budget k-NN variant already solves 87.0% and uses the same learned ranking. I would require the additional non-contextual baselines and the feature ablation before accepting the central claim. The paper is not circular; the reported solve rates are empirical and the k sweep is reported. The internal inconsistency about which reward function maximizes solved queries should also be corrected. The lack of code release is a significant practical limitation for this kind of empirical work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague, here is my take on the CYANEA paper.\n\nThe genuine novelty is framing the joint choice of symbolic solver, LLM, and prompt template as a contextual multi-armed bandit, with a layered variant and cost-aware budget allocation. That is a natural but previously unexplored extension of portfolio-solver ideas to LLM-based synthesis, and the paper executes it cleanly. The evaluation is above average for this area: 1,269 queries across three sources, 20 shuffled runs, standard deviations on the headline solve counts, and a comparison to a linear-budget variant. The main empirical claim holds up as reported: the best CYANEA instance solves 88.3% of queries versus 64.3% for the best single solver and within 4% of the virtual best.\n\nWhere the paper is soft: first, there is no fixed-order or random-ordering baseline that removes the bandit context entirely. The stress-test is right that single k-NN with linear budgets still solves 87.0%, only 1.3 points below the best full system, so the budget allocator is not doing much and we cannot isolate how much the learned ranking contributes. That matters because the title and framing put the online selection front and center. Second, the feature vector is underspecified: no keyword list, no normalization, no handling of the heterogeneous feature scales. The concern that Euclidean distance is dominated by query length is plausible and untested. Third, no code is released, the exponential-distribution MLE assumption is unvalidated, and Par-2 scores lack variance. These are all legitimate but moderate issues, not fatal.\n\nI think the reader's conditional verdict is right. The paper deserves peer review because the system works, the comparison is honest, and the missing baselines are fixable rather than load-bearing. I'd want the authors to add a fixed-order/random baseline, release code or at least a precise feature spec, and report variance on Par-2 before acceptance. The central result is not fraudulent or broken; the gaps are in attribution and reproducibility.","headline":"CYANEA is a solid, honest empirical paper on contextual bandit selection of LLM/prompt/solver portfolios for synthesis; the missing no-context baseline and underspecified features are the main soft spots, not the central result.","tokens_in":12867,"tokens_out":2796,"would_cite":true,"duration_ms":25335,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"An online multi-armed bandit, CYANEA, chooses per query between a symbolic solver and LLM-prompt pairs, and this selection solves 37.2% more synthesis queries than the best single solver while staying within 4% of a perfect selector.","keywords":["program synthesis","multi-armed bandit","prompt selection","LLM prompting","portfolio solver","SyGuS","online learning","k-nearest neighbors"],"falsifier":"Take the same 1,269-query benchmark, the same budgets, reward functions, and one configuration of CYANEA, but replace the hand-designed features with random feature vectors; if the percentage of solved queries does not drop substantially below 88.3% toward the 64.3% of the best single solver, the feature-similarity assumption is falsified. A second test is to train the bandit on the SyGuS and ranking-function queries and evaluate only on the fresh SMT-derived queries; if the improvement over the best single solver vanishes, the learned similarity does not generalize across distributions.","tokens_in":11708,"feed_emoji":"🎯","tokens_out":7110,"duration_ms":62656,"temperature":0.7,"pith_summary":"The paper asks how a non-expert user should decide, for each program-synthesis query, whether to call a symbolic solver, an LLM, and which prompt style to use. It treats this choice as an online learning problem and builds CYANEA, which uses a contextual multi-armed bandit to rank solver-prompt pairs per query and to allocate time and token budgets. On 1,269 queries spanning ranking-function synthesis, SyGuS competition problems, and fresh SMT-derived queries, the best CYANEA instance solves 88.3% of queries, versus 64.3% for the best single solver and 91.8% for a virtual best selector that always picks the optimal arm. The central claim is that per-query online selection, not any individual solver or prompt, is what delivers the gain. If this is right, users can get near-oracle portfolio performance without knowing in advance which LLM, prompt, or solver will work.","feed_headline":"Bandit picks the right prompt per query, solving 88 percent","feed_subtitle":"CYANEA beats the best fixed solver by 37.2% and trails an all-knowing selector by only 4%.","key_machinery":"The engine is a contextual k-nearest-neighbor multi-armed bandit. For each new query, it computes a feature vector (frequencies of SMT-LIB keywords, query length, constants, and logic type), finds the k previously solved queries closest in that feature space, and ranks each solver by the sum of rewards those neighbors earned. A second mechanism handles budgets: for each ranked arm, the cost needed per query is estimated by fitting an exponential distribution via maximum likelihood to the observed costs of nearby queries, and the total per-query token and time budgets are divided greedily along the ranking. The paper tests three reward functions—time-based, cost-based, and binary solve/not-solve—and two topologies: one bandit over all arms, and a layered set of bandits that first chooses the model and then chooses the prompt.","core_discovery":"The paper's central claim is that per-query solver-and-prompt selection can be learned online well enough to make a portfolio behave like a near-oracle. Concretely, CYANEA treats each symbolic solver and each LLM-prompt pair as an arm; after each query it receives a reward based on solving success, time, and token cost. A k-nearest-neighbor contextual bandit ranks the arms for the next query using the rewards of the k most similar previously solved queries, and a budget allocator spends the per-query time and token budget across the ranked arms. On 1,269 queries drawn from SyGuS, ranking-function, and SMT-derived benchmarks, the best run solved 88.3% of queries, compared with 64.3% for the best fixed solver and 91.8% for a virtual best selector that always makes the optimal choice. The authors conclude that the learning, not any individual solver, is what delivers the improvement.","pith_inferences":["An untested extension: replace the hand-designed features with random feature vectors on the same 1,269 queries; if the solved-query rate stays near 88%, the k-NN similarity is not the active ingredient, and if it falls toward the 64.3% of the best single solver, the features carry the result.","Because the rewards and bandit are agnostic to query syntax, the same machinery should transfer to other synthesis or code-generation settings, such as invariant synthesis, patch generation, or SMT solver selection, whenever a feature extractor can be defined.","A tighter time or token budget would stress the budget allocator more than the current setting, in which the system can often afford to run all arms on one query; testing under budgets small enough that only a few arms can be tried would separate the value of ranking from the value of allocation.","The remaining gap to the virtual best suggests headroom is in prediction rather than in the solver library, so a richer feature space or a bandit that models uncertainty could close more of the gap; this conjecture is not tested in the paper."],"forward_implications":["A non-expert with a batch of synthesis queries can deploy a portfolio of solvers and prompts without knowing which one will work, and still solve far more queries than using any single solver.","Because the reward function is plug-in, the same system can optimize for wall-clock time, API cost, or raw solve count depending on user priorities.","The per-query budget allocation lets the system recover when its top-ranked solver fails, by saving enough time and tokens to try lower-ranked arms.","The layered bandit variant shows a trade-off: decomposing model choice from prompt choice reduces the data available to each learner and increases variance, so the single-layer design is the more stable configuration.","Any new solver or prompting style can be added as another arm without retraining the feature extractor or the bandit, so the portfolio can grow over time."],"supporting_citations":[{"why":"Supplies the SyGuS competition benchmark queries and the running example used in the evaluation.","marker":"Alur et al. 2024"},{"why":"Supplies the nonstochastic multi-armed bandit formalism that frames online solver selection.","marker":"Auer et al. 2002"},{"why":"Provides CEGIS, the algorithm underlying the enumerative solver arm.","marker":"Solar-Lezama et al. 2006"},{"why":"Provides the A* search approach used as the synthesis phase of the enumerative solver.","marker":"Lee et al. 2018"},{"why":"Provides cvc5, the SMT solver used to validate whether candidate answers satisfy the specification, making the rewards trustworthy.","marker":"Barbosa et al. 2022"},{"why":"Supplies ranking-function synthesis queries used in the evaluation.","marker":"Giacobbe, Kroening, and Parsert 2022"},{"why":"Supplies termination and ranking-function benchmark queries used in the evaluation.","marker":"Giesl et al. 2019"},{"why":"Supplies automatically generated fresh SMT-derived synthesis queries and a related data-generation approach.","marker":"Parsert and Polgreen 2024"},{"why":"Provides the LLM-guided enumerative solver context and the prior solver the paper's enumerator builds on.","marker":"Li, Parsert, and Polgreen 2024"},{"why":"Provides MedleySolver, the closest sequential solver-portfolio approach, used as a comparison point for sequential deployment.","marker":"Pimpalkhare et al. 2021"}],"fun_headline_variants":["Bandit picks per-query solver and prompt, solves 88%","CYANEA bandit: 88% solved, near 92% oracle","Per-query prompt selection: bandit beats fixed solver by 24 points"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole gain rests on the assumption that the hand-built features describing a synthesis query (keyword frequencies, length, constants, logic type) make queries that look similar behave similarly under each solver, so past rewards on nearby queries predict which solver will win next.","fun_headline_variants_meta":{"raw":{"variants":["Bandit picks per-query solver and prompt, solves 88%","CYANEA bandit: 88% solved, near 92% oracle","Per-query prompt selection: bandit beats fixed solver by 24 points"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001307,"raw_usage":{"total_tokens":5361,"prompt_tokens":1009,"completion_tokens":4352,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":625,"completion_tokens_details":{"reasoning_tokens":4287}},"tokens_in":625,"tokens_out":4352,"duration_ms":30319,"temperature":1.0,"reasoning_tokens":4287,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:12:38.525172+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the same 1,269-query benchmark, the same budgets, reward functions, and one configuration of CYANEA, but replace the hand-designed features with random feature vectors; if the percentage of solved queries does not drop substantially below 88.3% toward the 64.3% of the best single solver, the feature-similarity assumption is falsified. A second test is to train the bandit on the SyGuS and ranking-function queries and evaluate only on the fresh SMT-derived queries; if the improvement over the best single solver vanishes, the learned similarity does not generalize across distributions.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the SyGuS competition benchmark queries and the running example used in the evaluation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the nonstochastic multi-armed bandit formalism that frames online solver selection."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides CEGIS, the algorithm underlying the enumerative solver arm."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the A* search approach used as the synthesis phase of the enumerative solver."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides cvc5, the SMT solver used to validate whether candidate answers satisfy the specification, making the rewards trustworthy."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies ranking-function synthesis queries used in the evaluation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies termination and ranking-function benchmark queries used in the evaluation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies automatically generated fresh SMT-derived synthesis queries and a related data-generation approach."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the LLM-guided enumerative solver context and the prior solver the paper's enumerator builds on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides MedleySolver, the closest sequential solver-portfolio approach, used as a comparison point for sequential deployment."}],"review_version":1}