Sygus Comp 2016 Eval

sygus-comp-2016-eval

SyGuS-Comp 2016: Results and Analysis — Alur et al. (2016) (arXiv:1611.07627, 2016)

What this evaluates

Evaluates syntax-guided program synthesis solvers on their ability to generate correct programs from logical constraints and grammars. It probes capabilities in conditional linear integer arithmetic, invariant generation, and programming-by-example with bit-vectors and strings.

Datasets

• SyGuS-Comp 2016 — total 1307; splits: General (309), Conditional Linear Integer Arithmetic (73), Invariant Synthesis (67), Programming By Example (858)

Metrics

• number_of_benchmarks_solved (primary) — range: percent
  • Count of benchmarks for which the solver produces a correct program within the time limit, divided by the total number of benchmarks in the track, expressed as a percentage.
• time_to_solve — range: other
  • Wall-clock time to solve a benchmark, classified into pseudo-logarithmic buckets: [0,1), [1,3), [3,10), [10,30), [30,100), [100,300), [300,1000), [1000,3600), >3600 seconds.
• expression_size — range: other
  • Number of nodes in the SyGuS parse-tree of the generated expression, classified into pseudo-logarithmic buckets: [1,10), [10,30), [30,100), [100,300), [300,1000), >1000.

Input / output format

Input: Logical constraints (e.g., pre/post conditions, invariants, or input-output examples) and a function grammar defining the valid program structure.

Output: A synthesized program/expression that satisfies the constraints, represented as a SyGuS parse tree.

Scoring recipe

def compute_metrics(predictions, gold_specs, times, parse_trees, time_limit=3600):
    solved = 0
    for pred, spec, t, tree in zip(predictions, gold_specs, times, parse_trees):
        if pred is not None and verify(pred, spec) and t <= time_limit:
            solved += 1
    solve_rate = (solved / len(gold_specs)) * 100
    time_bucket = classify_pseudo_log(t, [0,1,3,10,30,100,300,1000,3600])
    size_bucket = classify_pseudo_log(len(tree.nodes), [1,10,30,100,300,1000])
    return solve_rate, time_bucket, size_bucket

Common pitfalls

• Time comparisons use pseudo-logarithmic buckets rather than absolute seconds, which can mask performance differences within the same bucket.
• Expression size is measured by parse-tree node count, which may not reflect actual runtime efficiency or code quality.
• Solvers may terminate without producing a result or produce incorrect results; the evaluation counts these as unsolved, but the time bound may still be reported as the termination time.

Evidence (verbatim from paper)

The primary criterion for winning a track was the number of benchmarks solved, but we also analyzed the time to solve and the the size of the generated expressions. Both where classified using a pseudo-logarithmic scale as follows.

Citation

@misc{alur2016syguscomp,
  title={SyGuS-Comp 2016: Results and Analysis},
  author={Alur et al. (2016)},
  year={2016},
  note={arXiv:1611.07627}
}

• arXiv: 1611.07627