Sygu S Comp 15 Eval

---
name: sygu-s-comp-15-eval
description: Evaluates the capability of program synthesis solvers to generate correct functions or expressions that satisfy given logical constraints or specifications. It probes how well solvers handle different grammar restrictions, specification completeness, and problem structures like linear arithmetic or invariant generation. Use when the user wants to benchmark on SyGuS-Comp'15, or asks about evaluating this task. Reports number of benchmarks solved.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 1602.01170
  bibtex_key: alur2016resultsofsygu
  confidence: high
---

# sygu-s-comp-15-eval

> Results and Analysis of SyGuS-Comp'15 — Alur et al. (2016) (arXiv:1602.01170, 2016)

## What this evaluates

Evaluates the capability of program synthesis solvers to generate correct functions or expressions that satisfy given logical constraints or specifications. It probes how well solvers handle different grammar restrictions, specification completeness, and problem structures like linear arithmetic or invariant generation.

## Datasets

- **SyGuS-Comp'15** — total ?; splits: INV (67), LIA (73), general (309)

## Metrics

- `number of benchmarks solved` **(primary)** — range: other
  - Counts the total number of benchmarks for which a solver produces a correct program within the competition time limit.
- `time to solve` — range: other
  - Wall-clock time in seconds required by a solver to produce a correct solution. Capped at 3600 seconds; unsolved benchmarks are recorded as infinity.
- `expression size` — range: other
  - Number of nodes in the parse tree of the synthesized expression. Capped at 1000 nodes; larger sizes are recorded as infinity.

## Input / output format

**Input**: SyGuS-IF specification containing a logic declaration, grammar definition for the unknown function(s), and a constraint formula (or input-output examples) that the synthesized function must satisfy.

**Output**: A synthesized function/expression (program) that satisfies the given specification constraints.

## Scoring recipe

```python
solved_count = 0
times = []
sizes = []
for benchmark in benchmarks:
    solution = solver.run(benchmark.spec, time_limit=3600)
    if solution is correct(benchmark.spec):
        solved_count += 1
        times.append(solution.time)
        sizes.append(count_nodes(solution.parse_tree))
return solved_count, times, sizes
```

## Common pitfalls

- Time limit is strictly 3600 seconds; solvers that terminate early without a solution or exceed the limit are not counted as solved.
- Expression size is measured by parse tree nodes, not character count, and is capped at 1000 (recorded as infinity if exceeded).
- Partial specifications allow multiple semantic solutions, so correctness is checked against the constraint rather than a single gold function.

## Evidence (verbatim from paper)

> Figure 2 on the top shows for each track and category the number of benchmarks solved by each of the solvers. ... The black number above the black bar indicates the exact number of seconds (floor-rounded to the nearest second) it took the slowest solver to solve a benchmark (and ∞ if at least one solver exceeded the time bound). ... The white number at the lower part of the bar indicates the time of the fastest solver to solve that benchmark. ... The gray bars indicate the range of expression sizes in psuedo logarithmic scales ... where the size of an expression is determined by the number of nodes in its parse tree.

## Citation

```bibtex
@misc{alur2016resultsofsygu,
  title={Results and Analysis of SyGuS-Comp'15},
  author={Alur et al. (2016)},
  year={2016},
  note={arXiv:1602.01170}
}
```

- arXiv: 1602.01170