Sygu S Comp 15 Eval

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

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

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

• arXiv: 1602.01170