{"id":"0efe14a0-8e59-44cf-95fd-59f176c4e50e","arxiv_id":"2504.14480","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"From logs that record only side-effecting API calls, Syren synthesizes programs with hidden pure functions and control flow, and guarantees they reproduce the input traces.","lead":"This paper introduces Syren, a program synthesizer that builds scripts from partial execution logs that record only API calls with side effects. It combines rewriting and example-based synthesis to infer hidden pure functions and control flow, with applications to cloud automation.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Correctness guarantee relies on an unformalized initial global state: Eq. (1) omits it, so 'reproduce the input traces' is either per-trace replay or false for multi-state trace sets.","rationale":"The reader's weakest assumption identifies time-dependence as the core limitation; I agree, but I would sharpen it: the issue is not merely a practical caveat but an omission in the formal correctness predicate. Eq. (1) quantifies only over local input state σ, while trace generation also depends on the external global state G that is updated by visible calls. This makes the central correctness claim ambiguous: if G is intended to be common to all traces, the motivating trace set is already unsatisfiable; if G is existential per trace, the guarantee reduces to historical replay and is vacuously satisfied by the trivial br-branched program. The paper's own §3.3 limitation statement supports this reading. I do not see this as a reason to reject the paper. The synthesis technique is novel, the artifact is released, the evaluation is substantial, and the LLM comparison is honest about manual verification. But the 'correct by construction' claim needs to be restated with an explicit global-state quantifier, or restricted to APIs whose responses are deterministic functions of call order. This is consistent with the reader's CONDITIONAL verdict; I would keep that verdict while requiring the formal definitions to be repaired.","tokens_in":38592,"tokens_out":13402,"duration_ms":134472,"concrete_test":"Build a small interpreter of the §3.3 semantics with the starting global state made explicit, and feed it the two-trace EC2 example from §2 (identical first two visible calls, different DescribeInstanceStatus responses). Verify whether the initial replay program satisfies Eq. (1) under (a) one common starting global state and (b) a per-trace existential over starting global states. If (a) fails and only (b) holds, the formal correctness statement must be amended to quantify the initial global state per trace, and the abstract's 'reproduce the input traces' claim should be qualified as historical replay under the trace's original API state rather than a guarantee about execution from an arbitrary current state.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's headline guarantee is that the synthesized program is 'correct by construction' and 'will always be able to reproduce the input traces' (Abstract, §1). The formal backbone is Ψ(P,T_in) ≡ ∀τ_i∈T_in·∃σ·P(σ)=τ_i (Eq. 1, §4.1). But §3.3 defines P(σ)=τ only 'given a starting global state': the Visible rule is A(G,v)↓e, with G implicitly updated by each visible call. Eq. (1) never quantifies or fixes G. Under the natural single-global-state reading, the paper's own motivating trace pair is unrealizable: after the same first two visible calls (StopInstances(force=false), DescribeInstanceStatus), one trace observes 'stopping' and the other observes 'stopped'. No deterministic order-only transition function can produce both from one initial global state. Under the alternative per-trace-global-state reading, the guarantee is much weaker than advertised: it says each historical trace can be replayed if the API is reset to that trace's original state, not that the script run from a user's current state will reproduce those traces. The paper explicitly concedes the underlying idealization in §3.3: 'our approach will be unsound in situations where responses implicitly depend on time as opposed to ordering.' EC2 instance status is precisely such a time-dependent API, so this is not a remote edge case. Because Lemma 1 and every rewrite-correctness argument are stated in terms of this underspecified P(σ)=τ, the formal correctness claim is either uninterpreted or much weaker than the abstract suggests.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Syren, a synthesis technique that takes a set of partial execution traces -- records of only the visible side-effecting calls -- and produces a program that composes those visible calls with hidden pure functions and control-flow constructs such as conditionals and retry loops. The technical approach starts from a trivially correct program that branches over the input traces and repeatedly applies two kinds of rewrite rules: refinement rules that preserve trace subsumption, and synthesis rules that introduce hidden functions whose implementations are obtained from an off-the-shelf syntax-guided synthesizer. Correctness is formalized as trace subsumption: a program is correct if it can reproduce the input traces for some input state. The paper reports an implementation and evaluates it on 54 benchmarks from custom cloud-automation tasks, AWS runbooks, Blink automations, and ApiPhany-derived examples, finding that the main algorithm synthesizes the target-quality program for 39 of 54 benchmarks under the syntactic cost function. The claimed contributions are the first partial-trace synthesis formulation, the combining of optimizing rewrites with SyGuS, and the benchmark evaluation.","tokens_in":38924,"tokens_out":4457,"duration_ms":45521,"significance":"If the formal correctness claim is stated precisely, the paper describes a practically motivated and technically interesting synthesis problem that has not been addressed as a whole before. The combination of optimizing program rewrites with programming-by-example synthesis of hidden functions is a sensible decomposition of a hard search problem, and the evaluation on 54 benchmarks, with reproducible code and data, gives useful evidence about scalability. The paper also honestly documents several limitations, including unsupported date/string operations, inability to handle empty traces that terminate before any visible call, and timeouts on complex control flow. However, the headline 'correct by construction' guarantee is currently tied to an under-specified notion of global state, which affects the central formal claim rather than only the presentation.","major_comments":[{"comment":"The correctness predicate Ψ in Eq. (1) quantifies only over a local state σ, but Definition 3.2 and the Visible rule in Figure 5 define program evaluation relative to an initial global state G that is implicitly updated by each visible call. As written, P(σ)=τ is not a well-defined two-argument predicate, and the headline claim that the synthesized program 'will always be able to reproduce the input traces' is not entailed by Ψ. The motivating EC2 example in §2 illustrates the difficulty: the first two traces share the visible prefix StopInstances(force=false); DescribeInstanceStatus but observe 'stopping' in one trace and 'stopped' in the other, so no deterministic order-only transition from a single global state can produce both. The paper's own caveat in §3.3 -- that the approach is unsound when responses depend on time as opposed to ordering -- applies directly to this example. I recommend making the global state explicit in Definition 3.2 and Eq. (1), for instance by quantifying existentially over an initial global state per input trace, and then restating the correctness claim as per-trace replay under a matching initial state, or by substantially extending the semantics to model time dependence.","section":"§3.3, Definition 3.2, and §4.1, Eq. (1)"},{"comment":"The formal framework for rewrite correctness is stated as a single implication below the definition of the trace valuation transformation, but that implication is not a complete theorem: it does not specify the quantifier structure over global states, does not state whether the conclusion must hold for the same global state as the hypothesis, and no proof is provided that the transformation t always produces a trace valuation satisfying the invariant. Since this implication is what justifies 'correct by construction' for every synthesis rewrite, the paper needs a rigorous statement and proof, or at minimum a precise invariant that is shown to be preserved by each rewrite rule.","section":"§5.1, trace-valuation correctness implication"},{"comment":"The evaluation defines success as syntactic equivalence, modulo variable renaming, to a target program that the authors themselves wrote, and the input traces are generated by simulating those same target programs. Consequently, the 39/54 'optimal' result measures agreement with the authors' hand-written targets under the authors' cost functions, rather than an independent measure of whether the synthesized program is the correct generalization of the observed behavior. This limitation should appear in the main text, not only implicitly in the benchmark description, and the manual inspection step used to decide when enough traces had been collected should be documented more transparently.","section":"§7.2, Table 1"}],"minor_comments":[{"comment":"The trace definition in §3.2 records a visible call as (A(v), e), while the Visible rule in Figure 5 produces (A(G, v), e); the global-state parameter in the trace record should either be removed or explained.","section":"§3.2 and Figure 5"},{"comment":"The benchmark WaitForInputThenSendEmail uses the variable `_r` in the retry body but later refers to `payload`, and the SendEmail call passes `userId=isNonEmpty` rather than a value; if this is the actual benchmark code, it should be corrected or clarified.","section":"Appendix D.1.18"},{"comment":"The row for Report Long Running Instances reports '#Hidden-f' as -1 and '#If' as '??'; these placeholders should be replaced with concrete values or an explicit explanation of why they are not available.","section":"Table 1"},{"comment":"The LLM prompt explicitly instructs the model not to add loops when the traces do not show a need for them; this design choice can bias the comparison in favor of simpler programs and should be disclosed when interpreting the LLM results.","section":"Appendix C"},{"comment":"The k-bounded search uses a fixed k=6, and the text notes that increasing k leads to an intractable search space; a short sensitivity statement about how the results depend on k would make the comparison more interpretable.","section":"§6.1 and §7.4"}],"recommendation":"major_revision","confidential_remarks":"The paper is a good fit for PLDI and the core idea is publishable, but the formal correctness guarantee needs to be repaired: either the semantics and Eq. (1) must quantify over global states explicitly, or the claims must be weakened to per-trace replay. The evaluation is honest but relies on self-created ground truth, so the main text should acknowledge this. I would not reject on novelty grounds; the limitations section already shows the authors are aware of several boundary conditions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a read. The setting is real: logs of side-effecting calls, hidden pure functions, control flow, no negative examples. Prior PBD and API-synthesis work doesn't cover this combination, so the problem alone is a contribution. The rewrite-plus-PBE decomposition is a credible way to make it tractable, and the rewrite rules with trace valuations are carefully designed. They ship code and data on Zenodo, which counts for something.\n\nThe formal backbone is coherent as far as it goes. Trace subsumption and Lemma 1 are right, and reducing hidden-function synthesis to input-output examples extracted from trace valuations is clean. The evaluation on 54 benchmarks is useful context: 39/54 optimal for the main algorithm, 29/54 for Claude 3.5, with honest discussion of timeouts and DSL limits.\n\nSoft spots. The correctness guarantee is narrower than the abstract suggests. Eq. (1) quantifies a local input sigma, but the semantics in Fig. 5 depends on an unmentioned initial global state. The paper itself says we must assume the initial global state is the same as in the traces. So \"reproduce the input traces\" means replaying each trace from its own original state, not \"this script will work when run from a user's current state.\" The EC2 motivating example is exactly a time/state-dependent API, and Section 3.3 concedes the ordering model is unsound when responses depend on time. This is a scope caveat, not a collapse: the trace-replay guarantee is still meaningful for automation once you accept the model, but the abstract overstates it.\n\nThe evaluation also leans on hand-written target programs and manually augmented traces, which is honest but limits independent evidence. More concerning, the appendix tables contain impossible entries: SyGuS SAT counts larger than total calls, e.g. Table 2 has 2(3), 12(263), and Table 1 reports -1 hidden functions. That suggests the tables were assembled by hand and not checked. The artifact may reproduce the headline numbers, but the raw data needs a pass before publication.\n\nBottom line: deserves a serious referee. The problem is new, the method is plausible, and the artifact exists. I would ask the authors to state the global-state caveat in the correctness claim and fix the appendix tables. I'd cite it if I worked on trace-based synthesis.","headline":"Genuinely new synthesis problem with a sensible rewrite-plus-PBE decomposition, but the correctness guarantee is narrower than the abstract suggests and the appendix has data errors that should be fixed.","tokens_in":39448,"tokens_out":3000,"would_cite":true,"duration_ms":31438,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Syren synthesizes complete API scripts from partial call logs, hidden steps included.","keywords":["program synthesis","partial traces","syntax-guided synthesis","program rewriting","API composition","programming by example","trace subsumption","cloud automation"],"falsifier":"Take one API resource whose state changes with time, call the same sequence of visible functions twice with a long pause between the runs, and record the two traces; if the only difference is the response to a later status call, the ordering-only semantics predicts that no synthesized program can reproduce both traces, so either Syren fails or it must abandon the exact-reproduction guarantee.","tokens_in":38380,"feed_emoji":"🧩","tokens_out":8545,"duration_ms":74143,"temperature":0.7,"pith_summary":"The paper introduces Syren, a synthesis technique that takes only partial traces—recorded sequences of side-effecting API calls, with no record of the pure computations between them—and produces a script that composes those calls with the missing pure functions and control flow. The central claim is that this problem is solvable without negative examples or extra user input, and Syren is presented as the first method to do so. The algorithm generalizes over the positive traces, using a user-defined cost metric to pick among generalizations, and the output is correct by construction in the paper's sense: it provably reproduces every input trace. A sympathetic reader should care because the same machinery applies wherever traces are already being recorded—API automation logs, system-call logs, document-editing logs—so synthesis costs no extra specification effort.","feed_headline":"Syren fills the hidden steps between logged API calls","feed_subtitle":"Rewrites plus syntax-guided synthesis recover control flow and pure functions, then prove trace reproduction.","key_machinery":"The load-bearing mechanism is a pair of rewrite systems over a small domain-specific language: refinement rules, which factor identical visible calls out of conditionals and eliminate unused parameters while preserving trace subsumption, and synthesis rules, which replace an expression or branch condition with a call to a to-be-synthesized pure function. Correctness of the latter is tracked by a trace valuation, an augmented state that records, for every input trace, the concrete value each program variable must take. From that valuation the synthesizer extracts input-output pairs for the hidden function, such as a condition that reads the response of a status call and decides whether to retry, and discharges them to a programming-by-example solver; a rewrite is admitted only when such an implementation exists. The whole search is steered by a user-supplied cost function, so the final program minimizes that cost among all programs that still reproduce the traces.","core_discovery":"On its own terms, the discovery is that a program can be synthesized from a partial trace by starting from a trivially correct program that replays each trace on its own branch, then repeatedly rewriting that program to hoist shared calls, replace constants with parameters, and replace branch conditions with calls to newly synthesized pure functions. Each rewrite is proved to preserve trace subsumption, meaning the new program can still generate every input trace; the hidden functions are obtained by converting the current trace valuation into input-output examples and solving them with an off-the-shelf syntax-guided synthesizer. This is the first approach, the authors argue, to infer both control flow and non-trivial hidden pure function calls from records of only the side-effecting functions. The paper further claims that the approach scales to 54 real-world benchmarks drawn from cloud automation, filesystem, and document-edition scripts, with 39 of them synthesized optimally in under five minutes.","pith_inferences":["If the ordering-only assumption is relaxed, the same rewrite machinery could target timeout-driven retries and rate-limit responses, which are visible-call sequences whose outputs depend on elapsed time; the paper's own limitation note identifies exactly this boundary.","A practical extension would be to let a large language model propose hidden-function implementations and then run Syren's trace-subsumption check as a verifier, converting silent failures into detectable ones.","Because the cost function is user-defined, the framework could optimize for operational properties beyond readability, such as fewest distinct API endpoints or least-privilege permission sets, which would matter for security-sensitive automation.","The benchmark suite is built by simulating traces that exercise all program paths; a natural next experiment is to measure how few traces are needed per control-flow structure, since the paper reports 2 to 10 traces per benchmark."],"forward_implications":["Programs synthesized this way can include conditionals, retry loops, and hidden pure functions that never appear in the traces, yet each synthesized program is guaranteed to reproduce every input trace.","A user needs to supply only positive traces; no negative examples are required, because the cost function, not counterexamples, prevents over-generalization.","Swapping the cost function changes the notion of best program: the paper demonstrates syntactic-complexity and trace-reuse metrics, and both are usable within the same rewrite framework.","The correctness guarantee is conditional: it holds when visible-function responses are a function of the ordered sequence of prior calls, as the paper states in its semantics section.","The main bottleneck is the underlying programming-by-example solver, so any improvement in JSONPath, string, or arithmetic synthesis would directly extend Syren's reach."],"supporting_citations":[{"why":"supplies the solver-aided synthesis backend used to realize hidden-function implementations from input-output constraints.","marker":"[34]"},{"why":"provides the underlying SMT solver on which that synthesis backend relies.","marker":"[12]"},{"why":"supplies REST-API composition benchmarks adapted for the evaluation and a type-directed synthesis approach to contrast with.","marker":"[18]"},{"why":"is the source of real-world cloud-automation scripts whose API calls form part of the benchmark traces.","marker":"[3]"},{"why":"is the source of security-automation tasks used as another benchmark category.","marker":"[7]"}],"fun_headline_variants":["Synth fills gaps in partial API call logs","From partial traces to complete programs","Rewrites synthesize hidden functions from logs","Recovering control flow from trace snippets","Turning partial traces into executable scripts"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole guarantee rests on the assumption that a visible function's response is determined by the ordered sequence of earlier visible calls, not by how much wall-clock time has passed; real APIs whose replies change over time are outside the model.","fun_headline_variants_meta":{"raw":{"variants":["Synth fills gaps in partial API call logs","From partial traces to complete programs","Rewrites synthesize hidden functions from logs","Recovering control flow from trace snippets","Turning partial traces into executable scripts"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000366,"raw_usage":{"total_tokens":1938,"prompt_tokens":885,"completion_tokens":1053,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":501,"completion_tokens_details":{"reasoning_tokens":991}},"tokens_in":501,"tokens_out":1053,"duration_ms":6989,"temperature":1.0,"reasoning_tokens":991,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T11:47:47.423571+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take one API resource whose state changes with time, call the same sequence of visible functions twice with a long pause between the runs, and record the two traces; if the only difference is the response to a later status call, the ordering-only semantics predicts that no synthesized program can reproduce both traces, so either Syren fails or it must abandon the exact-reproduction guarantee.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"is the source of security-automation tasks used as another benchmark category."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"is the source of real-world cloud-automation scripts whose API calls form part of the benchmark traces."}],"review_version":1}