Yixuan Li, Julian Parsert, Elizabeth Polgreen
Computer Aided Verification – 36th International Conference (CAV), Lecture Notes in Computer Science 14682, pp. 280-301, 2024.
pdf 
doi:10.1007/978-3-031-65630-9_15
Abstract
Pre-trained Large Language Models (LLMs) are beginning to dominate the discourse around automatic code generation with natural language specifications. In contrast, the best-performing synthesizers in the domain of formal synthesis with precise logical specifications are still based on enumerative algorithms. In this paper, we evaluate the abilities of LLMs to solve formal synthesis benchmarks by carefully crafting a library of prompts for the domain. When one-shot synthesis fails, we propose a novel enumerative synthesis algorithm, which integrates calls to an LLM into a weighted probabilistic search. This allows the synthesizer to provide the LLM with information about the progress of the enumerator, and the LLM to provide the enumerator with syntactic guidance in an iterative loop. We evaluate our techniques on benchmarks from the Syntax-Guided Synthesis (SyGuS) competition. We find that GPT-3.5 as a stand-alone tool for formal synthesis is easily outperformed by state-of-the-art formal synthesis algorithms, but our approach integrating the LLM into an enumerative synthesis algorithm shows significant performance gains over both the LLM and the enumerative synthesizer alone and the winning SyGuS competition tool.
BibTex
@inproceedings{DBLP:conf/cav/LiPP24, author = {Yixuan Li and Julian Parsert and Elizabeth Polgreen}, editor = {Arie Gurfinkel and Vijay Ganesh}, title = {Guiding Enumerative Program Synthesis with Large Language Models}, booktitle = {Computer Aided Verification - 36th International Conference, {CAV} 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {14682}, pages = {280--301}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-65630-9\_15}, doi = {10.1007/978-3-031-65630-9\_15}, timestamp = {Thu, 22 Aug 2024 20:23:18 +0200}, biburl = {https://dblp.org/rec/conf/cav/LiPP24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}}
- Details
- Category: Publications 2024
Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Lecture Notes in Artificial Intelligence 14740, pp. 298-316, 2024.
Abstract
We show that (local) confluence of terminating logically constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that criticalx pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.
pdf doi:10.1007/978-3-031-63501-4_16
BibTeX
@inproceedings{JSFMAM-IJCAR24, author = "Jonas Sch\"{o}pf and Fabian Mitterwallner and Aart Middeldorp", title = "Confluence of Logically Constrained Rewrite Systems Revisited", booktitle = "Proceedings of the 12th International Joint Conference on Automated Reasoning", editor = "Christoph Benzm\"{u}ller and Marijn J. H. Heule and Renate A. Schmidt", series = "Lecture Notes in Artificial Intelligence", volume = 14740, pages = "298--316", year = 2024, doi = "10.1007/978-3-031-63501-4\_16"}
- Details
- Category: Publications 2024
Takahito Aoto, Naoki Nishida, Jonas Schöpf
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Leibniz International Proceedings in Informatics (LIPIcs) 299, pp. 31:1-31:21, 2024.
Abstract
Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories.
pdf doi:10.4230/LIPIcs.FSCD.2024.31
BibTeX
@inproceedings{TANNJS-FSCD24, author = "Takahito Aoto and Naoki Nishida and Jonas Sch\"{o}pf", editor = "Jakob Rehof", title = "Equational Theories and Validity for Logically Constrained Term Rewriting", booktitle = "Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction", series = "Leibniz International Proceedings in Informatics (LIPIcs)", volume = 299, pages = "31:1--31:21", year = 2024, doi = "10.4230/LIPIcs.FSCD.2024.31"}
- Details
- Category: Publications 2024
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), ACM pp. 57:1-57:12, 2024.
pdf doi:10.1145/3661814.3662081
Abstract
By means of a simple reduction from Hilbert’s 10th problem we prove the somewhat surprising result that termination of one-rule rewrite systems by a linear interpretation in the natural numbers is undecidable. The very same reduction also shows the undecidability of termination of one-rule rewrite systems using the Knuth—Bendix order with subterm coefficients. The linear termination problem remains undecidable for one-rule rewrite systems that can be shown terminating by a (non-linear) polynomial
interpretation. We further show the undecidability of the problem whether a one-rule rewrite system can be shown terminating by a polynomial interpretation with rational or real coefficients. Several of our results have been formally verified in the Isabelle/HOL proof assistant.
BibTex
@inproceedings{FMAMRT-LICS24, author = "Fabian Mitterwallner and Aart Middeldorp and Ren{\'e} Thiemann", title = "Linear Termination is Undecidable", booktitle = "Proceedings of the 39th Annual {ACM/IEEE} Symposium on Logic in Computer Science", editor = "Pawel Sobocinski and Ugo Dal Lago and Javier Esparza", publisher = "{ACM}", pages = "57:1--57:12", year = 2024, doi = "10.1145/3661814.3662081"}
- Details
- Category: Publications 2024