Sygus Comp 2018 Eval

sygus-comp-2018-eval

SyGuS-Comp 2018: Results and Analysis — Alur et al. (2019) (arXiv:1904.07146, 2019)

What this evaluates

Evaluates syntax-guided synthesis solvers on their ability to generate correct programs or specifications across multiple domains, including general synthesis, conditional linear integer arithmetic, invariant generation, and programming by examples.

Datasets

• SyGuS-Comp 2018 — total 1600; splits: test (-1)

Metrics

• correctness (primary) — range: [0, 1]
  • Fraction of benchmarks for which the solver produces a solution that passes both syntactic grammar validation and semantic SMT verification within resource limits.

Input / output format

Input: A benchmark instance specifying a target function, a grammar (or input/output examples/constraints), and semantic requirements.

Output: A synthesized expression or program that must conform to the specified grammar and satisfy all semantic constraints.

Scoring recipe

solved = 0
for bench in benchmarks:
    sol = solver.run(bench, time_limit=3600, mem_limit=128e9)
    if sol is None:
        continue
    if check_syntax(sol, bench.grammar) and check_semantics(sol, bench.constraints):
        solved += 1
return solved / len(benchmarks)

Common pitfalls

• Solvers must pass both syntactic grammar checks and semantic SMT verification; failing either counts as incorrect.
• Resource limits are strict: 3600s wall-clock time and 128GB memory per run; exceeding either results in a timeout/oom failure.
• Benchmarks are divided into specialized tracks (CLIA, Inv, PBE, General); solvers often specialize, so cross-track comparison requires normalization.

Evidence (verbatim from paper)

The memory usage limit for each solver run was set to 128 GB, and the wall-clock time limit is set to 3600 seconds (thus, a solver that used all 4 cores could consume at most 14400 seconds of CPU time). The solutions that the solvers produced were checked for both syntactic and semantic correctness. That is, a first postprocessor checked that the produced expression adhered to the grammar specified in the given benchmark, and if this check passes, a second postprocessor checked that the solution adhered to semantic constraints given in the benchmark (by invoking an SMT solver).

Citation

@misc{alur2019syguscomp2018,
  title={SyGuS-Comp 2018: Results and Analysis},
  author={Alur et al. (2019)},
  year={2019},
  note={arXiv:1904.07146}
}

• arXiv: 1904.07146