Sygus Comp 2017 Eval

sygus-comp-2017-eval

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

What this evaluates

Evaluates the ability of synthesis solvers to generate correct programs or expressions that satisfy given grammatical and semantic constraints across multiple domain-specific tracks.

Datasets

• SyGuS-Comp 2017 — total ?; splits: test (-1)

Metrics

• correctness (primary) — range: [0, 1]
  • Fraction of benchmarks for which the solver produces a solution that passes both syntactic grammar checks and semantic equivalence checks via an SMT solver.

Input / output format

Input: Benchmark specification containing a target grammar and a logical/semantic constraint.

Output: A synthesized expression or program that must conform to the target grammar and satisfy the semantic constraint.

Scoring recipe

def evaluate(predictions, benchmarks):
    solved = 0
    for pred, bench in zip(predictions, benchmarks):
        if check_syntax(pred, bench.grammar) and check_semantics(pred, bench.constraints, smt_solver):
            solved += 1
    return solved / len(benchmarks)

Common pitfalls

• Solvers may produce syntactically valid but semantically incorrect expressions if the SMT check is skipped or misconfigured.
• Time limits are wallclock (3600s), not CPU time, so multi-threaded solvers can consume up to 14400 CPU seconds before timing out.
• Grammar constraints are strict; any deviation from the specified terminal/non-terminal structure results in immediate rejection.

Evidence (verbatim from paper)

The solutions that the solvers produce are being checked for both syntactic and semantic correctness. That is, a first post-processor checks that the produced expression adheres to the grammar specified in the given benchmark, and if this check passes, a second post-processor checks that the solution adheres to semantic constraints given in the benchmark (by invoking an SMT solver).

Citation

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

• arXiv: 1711.11438