Sygus Comp 2017 Eval

---
name: sygus-comp-2017-eval
description: Evaluates the ability of synthesis solvers to generate correct programs or expressions that satisfy given grammatical and semantic constraints across multiple domain-specific tracks. Use when the user wants to benchmark on SyGuS-Comp 2017, or asks about evaluating this task. Reports correctness.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 1711.11438
  bibtex_key: [REDACTED]
  confidence: high
---

# 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

```python
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

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

- arXiv: 1711.11438