Synthesis Benchmarks for Automated Reasoning
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918124772655104 |
|---|---|
| author | Hajdu, Márton Hozzová, Petra Kovács, Laura Voronkov, Andrei Wagner, Eva Maria Žilinčík, Richard Steven |
| author_facet | Hajdu, Márton Hozzová, Petra Kovács, Laura Voronkov, Andrei Wagner, Eva Maria Žilinčík, Richard Steven |
| contents | Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $\forall\exists$-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19827 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Synthesis Benchmarks for Automated Reasoning Hajdu, Márton Hozzová, Petra Kovács, Laura Voronkov, Andrei Wagner, Eva Maria Žilinčík, Richard Steven Logic in Computer Science Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $\forall\exists$-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis. |
| title | Synthesis Benchmarks for Automated Reasoning |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.19827 |