Relational program synthesis

Relish significantly outperforms EUSolver, a general-purpose synthesis tool that won the General Track of the most recent SyGuS competition for syntax-guided synthesis.

“Our evaluation also shows that Relish significantly outperforms EUSolver, a general-purpose synthesis tool that won the General Track of the most recent SyGuS competition for syntax-guided synthesis.”

The proposed technique can solve almost all of the benchmarks.

“Our experimental results show that the proposed technique can solve almost all of these benchmarks and that it significantly outperforms EUSolver, a generic synthesis framework that won the general track of the most recent SyGuS competition.”

Relish can automatically synthesize the correct Base64 encoder and decoder from the given specification using a DSL targeted for this domain.

“Relish can automatically synthesize the correct Base64 encoder and decoder from this specification using a DSL targeted for this domain (see Section 6.2).”

The proposed technique significantly outperforms EUSolver, a generic synthesis framework that won the general track of the most recent SyGuS competition.

“Our experimental results show that the proposed technique can solve almost all of these benchmarks and that it significantly outperforms EUSolver, a generic synthesis framework that won the general track of the most recent SyGuS competition.”

Relish can efficiently solve interesting benchmarks taken from previous literature and online forums.

“Our evaluation shows that Relish can efficiently solve interesting benchmarks taken from previous literature and online forums.”

Relish takes an average of 17.9 seconds per benchmark on the ten encoder/decoder benchmarks.

“As shown in Table 1, Relish can correctly solve all of these benchmarks 9 and takes an average of 17.9 seconds per benchmark.”

Relish's memory usage on encoder/decoder benchmarks varies between 284MB and 1843MB, with an average of 685MB.

“Here, the memory usage varies between 284MB and 1843MB, with the average being 685MB.”

The comparator-20 benchmark is not expressible in the current DSL because it requires comparing integers obtained by concatenating all substrings that represent integers in the input strings.

“we found this benchmark is not expressible in our current DSL because it requires comparing integers that are obtained by concatenating all substrings that represent integers in the input strings.”

On comparator benchmarks, Relish requires fewer CEGIS iterations than EUSolver (7.0 vs. 9.9 on average).

“Relish requires fewer CEGIS iterations (7.0 vs. 9.9 on average)”

• AssumptionRests on an assumption: The relational specifications constructed for each benchmark correctly capture the intended sorting or encoding/decoding task.

For the five encoder/decoder benchmarks solved by both Relish and EUSolver, Relish's average speed-up over EUSolver is 46.5x.

“For the five benchmarks that can be solved by both tools, the average speed-up of Relish over EUSolver is 46.5x.”

Relish outperforms EUSolver by 26x in running time on the common comparator benchmarks solved by both techniques.

“outperforms EUSolver by 26x (in terms of running time) on the common benchmarks that can be solved by both techniques.”

• AssumptionRests on an assumption: The relational specifications constructed for each benchmark correctly capture the intended sorting or encoding/decoding task.

Relish successfully solves 95% of the comparator benchmarks within the 24 hour time limit.

“Relish can successfully solve 95% of the benchmarks within the 24 hour time limit.”

• AssumptionRests on an assumption: The relational specifications constructed for each benchmark correctly capture the intended sorting or encoding/decoding task.

The HFTA can be constructed in O(km) time, where k is the size of the ground relational specification and m is the size of the largest FTA in the HFTA.

“Since the HFTA may contain at most k FTAs, it can be constructed in O(km) time, where m is the size of largest FTA in the HFTA.”

FindProgs has worst-case complexity O(m bn), where n is the number of functions to synthesize and b is the bound of AST size for all programs under consideration.

“Observe that FindProgs is a backtracking search procedure, its worst case complexity is O(m bn ) where n is the number of functions to synthesize, and b is the bound of AST size for all programs under consideration.”

Relish's memory usage on comparator benchmarks varies between 12 MB and 18367MB, with an average of 3382MB.

“memory usage varies between 12 MB and 18367MB, with an average memory consumption of 3382MB.”

Memory usage is higher for comparator benchmarks than for encoder/decoder benchmarks.

“we see that memory usage is higher for comparators than the encoder/decoder benchmarks.”

Relish is more efficient than EUSolver per CEGIS iteration on comparator benchmarks (12 seconds vs. 492 seconds).

“Relish is also more efficient than EUSolver per CEGIS iteration (12 seconds vs. 492 seconds).”

• AssumptionRests on an assumption: The relational specifications constructed for each benchmark correctly capture the intended sorting or encoding/decoding task.

The ground relational specification can be relaxed in linear time O(k), where k is the size of the ground relational specification.

“Specifically, the ground relational specification can be relaxed in linear time O(k), where k is the size of ground relational specification.”

EUSolver solves half of the ten encoder/decoder benchmarks within the 24 hour time limit.

“In contrast, EUSolver solves half of the benchmarks within the 24 hour time limit and takes an average of approximately 12 minutes per benchmark that it is able to solve.”

Relish solves 75% of the comparator benchmarks within 2 minutes.

“and 75% of the benchmarks within 2 minutes.”

If there exist a set of programs that satisfy Φ and can be implemented using the DSLs given by G, then invoking FindProgs on H and M will eventually return programs P satisfying Φ.

“If there exist a set of programs that (a) satisfy Φ and (b) can be implemented using the DSLs given by G, then invoking FindProgs on H and M will eventually return programs P satisfying Φ.”

For a ground formula Φ where every function symbol f1,...,fn occurs exactly once, if G,M ⊢ Φ H and there are implementations Pi of fi conforming to grammar G(M^{-1}(fi)), then there exists a hierarchical tree T accepted by H such that Υ(v_fi)=Pi for all i.

“If there are implementations P i of f i where P i conforms to grammar G(M -1 (f i )), then there exists a hierarchical tree T = (V , ϒ, v r , E) accepted by H such that ϒ(v f i ) = P i for all i ∈ [1, n]”

The overall complexity of the inductive synthesis algorithm is O(km + m bn).

“Therefore, the overall complexity is O(km + m bn ).”

Relish solves 46% more comparator benchmarks than EUSolver (19 vs. 13).

“Relish solves 46% more benchmarks than EUSolver (19 vs. 13)”

• AssumptionRests on an assumption: The relational specifications constructed for each benchmark correctly capture the intended sorting or encoding/decoding task.

EUSolver takes an average of approximately 12 minutes per benchmark it solves among the encoder/decoder benchmarks.

“In contrast, EUSolver solves half of the benchmarks within the 24 hour time limit and takes an average of approximately 12 minutes per benchmark that it is able to solve.”

Relish has been used to build relational synthesizers to automatically generate string encoders/decoders as well as comparators.

“We have used the Relish framework to build relational synthesizers to automatically generate string encoders/decoders as well as comparators, and we evaluate our tool on several benchmarks taken from prior work and online forums.”

Among the 19 solved comparator benchmarks, Relish takes an average of 94.7 seconds per benchmark.

“Among these 19 benchmarks, Relish takes an average of 94.7 seconds per benchmark”

Relish solves 55% of the comparator benchmarks within 1 minute.

“it solves 55% of the benchmarks within 1 minute”

Relish can be instantiated to different application domains by providing a suitable domain-specific language and the relevant relational specification.

“We have implemented the proposed technique in a framework called Relish, which can be instantiated to different application domains by providing a suitable domain-specific language and the relevant relational specification.”

The relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space.

“However, this relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space.”

• Also stated in: § Abstract · plain

  “Solving the relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space.”

Our method constructs the HFTA in such a way that tuples of programs that do not satisfy the examples are rejected and therefore excluded from the search space.

“Furthermore, our method constructs the HFTA in such a way that tuples of programs that do not satisfy the examples are rejected and therefore excluded from the search space.”

The proposed technique combines the counterexample-guided inductive synthesis framework with a novel inductive synthesis algorithm based on relational version space learning.

“As a first step towards solving this problem, this paper presents a synthesis technique that combines the counterexample-guided inductive synthesis framework with a novel inductive synthesis algorithm that is based on relational version space learning.”

Our relational version space learning algorithm is based on the novel concept of hierarchical finite tree automata (HFTA).

“In more detail, our relational version space learning algorithm is based on the novel concept of hierarchical finite tree automata (HFTA).”

Relational synthesis can be used to solve the program inversion problem where the goal is to generate a program P' that is an inverse of another program P.

“As another example, we can use relational synthesis to solve the program inversion problem where the goal is to generate a program P ′ that is an inverse of another program P [Hu and D'Antoni 2017;Srivastava et al. 2011].”

• cites Hu and D'Antoni 2017;Srivastava et al. 2011Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Relational synthesis can be used to automatically generate comparators that provably satisfy correctness requirements such as transitivity and anti-symmetry.

“For example, we can use relational synthesis to automatically generate comparators that provably satisfy certain correctness requirements such as transitivity and anti-symmetry.”

Because relational counterexamples can refer to compositions of functions, the HFTA representation allows us to compose different FTAs according to the hierarchical structure of subterms in the relational counterexamples.

“Because relational counterexamples can refer to compositions of functions (e.g., f (д(1), д(2))), the HFTA representation allows us to compose different FTAs according to the hierarchical structure of subterms in the relational counterexamples.”

The HFTA representation allows us to compactly represent those programs that are consistent with the relational examples.

“Thus, the HFTA representation allows us to compactly represent those programs that are consistent with the relational examples.”

A naive algorithm that simply enumerates combinations of programs and then checks their correctness with respect to the relational specification is unlikely to scale.

“In particular, a naive algorithm that simply enumerates combinations of programs and then checks their correctness with respect to the relational specification is unlikely to scale.”

The solution returned by FindProgs is guaranteed to be a valid solution for the original relational synthesis problem.

“Since the resulting mapping P res maps each function symbol in the original specification to a single program, the solution returned by FindProgs is guaranteed to be a valid solution for the original relational synthesis problem.”

Lemma A.1: For any tree t accepted by FTA A built with grammar G and initial states using rules from Figure 8, the accepting run of t with x_i = c_i, where q^{c_i}_{x_i} ∈ Q_i, is rooted with final state q^c_s and c = t(c_1,...,c_m).

“(2) The accepting run of t with x i = c i , where q c i x i ∈ Q i , is rooted with final state q c s and c = t(c 1 , . . ., c m ) .”

Lemma A.2: Given G,M ⊢ t H, for any hierarchical tree T accepted by H, Υ(v_{f_i}) is a program that conforms to grammar G(M^{-1}(f_i)).

“(1) ϒ(v f i ) is a program that conforms to grammar G(M -1 (f i ))”

Lemma A.3: Given G,M ⊢ Φ H, for any hierarchical tree T accepted by H, Υ(v_{f_i}) is a program that conforms to grammar G(M^{-1}(f_i)).

“(1) ϒ(v f i ) is a program that conforms to grammar G(M -1 (f i ))”

Lemma A.3: Given G,M ⊢ Φ H, if the run of Υ(v_r) on Ω(v_r) is rooted with final state q^⊥_{s0}, then Υ(v_{f1}),...,Υ(v_{fn}) ̸|= Φ.

“(3) If the run of ϒ(v r ) on Ω(v r ) is rooted with final state q ⊥ s 0 , then ϒ(v f 1 ), . . . , ϒ(v f n ) ̸ |= Φ”

Relish's memory usage on encoder/decoder benchmarks mainly depends on the number of CEGIS iterations and the size of programs to be synthesized.

“the memory usage mainly depends on (1) the number of CEGIS iterations and (2) the size of programs to be synthesized.”

The HFTA-based method might have better generalization power compared to enumerative search.

“This discrepancy suggests that our HFTA-based method might have better generalization power compared to enumerative search.”

The HFTA-based approach has advantages over enumerative search for synthesizing string encoders and decoders.

“To summarize, these results clearly indicate the advantages of our approach compared to enumerative search when synthesizing string encoders and decoders.”

• AssumptionRests on an assumption: The 24-hour time limit is a fair and meaningful criterion for comparing Relish and EUSolver.
• AssumptionRests on an assumption: EUSolver is a state-of-the-art enumerative solver and a fair baseline for evaluating Relish.

Lemma A.4: If there is a program P conforming to grammar G such that P(a_1,...,a_m)=a where q^{a_i}_{s_i} ∈ Q_i, then there exists a tree accepted by A and the run is rooted with final state q^a_s from initial states q^{a_1}_{x_1},...,q^{a_m}_{x_m}.

“If there is a program P that conforms to grammar G such that P (a 1 , . . ., a m ) = a where q a i s i ∈ Q i for i ∈ [1, m], then there exists a tree accepted by A and the run is rooted with final state q a s from initial states q a 1 x 1 , . . ., q a m x m .”

The method only allows relational specifications of the form ∀x.φ(x) where φ is quantifier-free.

“we only allow relational specifications of the form ∀ì x .ϕ(ìx) where ϕ is quantifier-free.”

The enumeration-based approach performs considerably worse than Relish on comparator synthesis because it does not use the relational (k-safety) specification to prune its search space.

“the enumerationbased approach performs considerably worse than Relish because it does not use the relational (i.e., k-safety) specification to prune its search space.”

Constructing an FTA for a function symbol f ∈ F requires knowledge about the possible values of its arguments, which can introduce circular dependencies if we have multiple occurrences of f.

“In particular, constructing an FTA for a function symbol f ∈ F requires knowledge about the possible values of its arguments, which can introduce circular dependencies if we have multiple occurrences of f (e.g., f (f (1))).”

Lemma A.5: If t is a term where every function symbol f_1,...,f_n occurs exactly once, G,M ⊢ t H, and there are implementations P_i of f_i such that t=a where P_i conforms to G(M^{-1}(f_i)), then there exists a hierarchical tree T accepted by H such that Υ(v_{f_i})=P_i for all i and the run of Υ(v_r) on Ω(v_r) is rooted with final state q^a_s.

“If there are implementations P i of f i such that t = a, where P i conforms to grammar G(M -1 (f i )), then there exists a hierarchical tree T = (V , ϒ, v r , E) accepted by H such that ϒ(v f i ) = P i for all i ∈ [1, n], and the run of ϒ(v r ) on Ω(v r ) is rooted with final state q a s .”

The technique is implemented in Relish, which can be instantiated in different application domains by providing a suitable DSL and relevant relational specifications.

“We have implemented this technique in a relational synthesis framework called Relish which can be instantiated in different application domains by providing a suitable domain-specific language as well as the relevant relational specifications.”

Relish can successfully synthesize non-trivial string comparators that arise in real-world scenarios.

“this experiment demonstrates that Relish can successfully synthesize non-trivial string comparators that arise in real-world scenarios.”

• AssumptionRests on an assumption: The collected encoder/decoder and comparator benchmarks are representative of real-world relational synthesis tasks.

The key idea of the approach is to construct a relational version space in the form of a hierarchical finite tree automaton that encodes all tuples of programs satisfying the original specification.

“the key idea is to construct a relational version space (in the form of a hierarchical finite tree automaton) that encodes all tuples of programs that satisfy the original specification.”

Lemma A.2: Given G,M ⊢ t H, for any hierarchical tree T accepted by H, the run of Υ(v_r) on Ω(v_r) is rooted with final state q^t_s.

“(2) The run of ϒ(v r ) on Ω(v r ) is rooted with final state q t s .”

The HFTA method gives a sound and complete synthesis procedure with respect to the relaxed specification where each function symbol occurs exactly once.

“As stated by Theorems 5.2 and 5.3, the HFTA method discussed in the previous subsection gives a sound and complete synthesis procedure with respect to the relaxed specification where each function symbol occurs exactly once.”

• AssumptionThe authors state this as an assumption: Every variable x_i in function f is annotated by f to enforce its global uniqueness.

If there is a set of programs that (a) satisfy Ψ and (b) can be implemented using the DSLs given by G, then Algorithm 1 will eventually terminate with programs P satisfying Ψ.

“Theorem 5.6.(Completeness) If there is a set of programs that (a) satisfy Ψ and (b) can be implemented using the DSLs given by G, then Algorithm 1 will eventually terminate with programs P satisfying Ψ.”

The relational synthesis approach has advantages over an existing state-of-the-art solver for comparator synthesis.

“This experiment also demonstrates the advantages of our new relational synthesis approach compared to an existing state-of-the-art solver.”

• AssumptionRests on an assumption: EUSolver is a state-of-the-art enumerative solver and a fair baseline for evaluating Relish.

As the CEGIS loop progresses, the number of function occurrences in the ground relational specification increases, resulting in larger HFTAs.

“as the CEGIS loop progresses, the number of function occurrences in the ground relational specification increases, which results in larger HFTAs.”

EUSolver only supports synthesis tasks in linear integer arithmetic, bitvectors, and basic string manipulations by default.

“Since EUSolver only supports synthesis tasks in linear integer arithmetic, bitvectors, and basic string manipulations by default, we extend it to encoder/decoders and comparators by implementing the same DSLs described in Section 6.”

• cites Alur et al. 2017Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Relish outperforms EUSolver across all ten encoder/decoder benchmarks.

“Relish unequivocally outperforms EUSolver across all benchmarks.”

• AssumptionRests on an assumption: The 24-hour time limit is a fair and meaningful criterion for comparing Relish and EUSolver.
• AssumptionRests on an assumption: EUSolver is a state-of-the-art enumerative solver and a fair baseline for evaluating Relish.

The approach can synthesize a program and its inverse simultaneously rather than requiring the user to provide one of these functions.

“our approach can be used to synthesize the program and its inverse simultaneously rather than requiring the user to provide one of these functions.”

Lemma A.3: Given G,M ⊢ Φ H, if the run of Υ(v_r) on Ω(v_r) is rooted with final state q^⊤_{s0}, then Υ(v_{f1}),...,Υ(v_{fn}) |= Φ.

“(2) If the run of ϒ(v r ) on Ω(v r ) is rooted with final state q ⊤ s 0 , then ϒ(v f 1 ), . . . , ϒ(v f n ) |= Φ”

The programs currently synthesized by Relish are compositions of built-in functions provided by the DSL.

“the programs that can be currently synthesized by Relish are compositions of built-in functions provided by the DSL.”

Our HFTA construction follows the recursive decomposition of Φ' and allows us to compose the individual version spaces of each subterm in a way that the final HFTA is consistent with Φ'.

“Our HFTA construction follows the recursive decomposition of Φ ′ and allows us to compose the individual version spaces of each subterm in a way that the final HFTA is consistent with Φ ′ .”

The method does not handle relational specifications with quantifier alternation.

“our method does not handle more complex relational specifications with quantifier alternation”

For any hierarchical tree T accepted by H, the programs assigned to f_1, ..., f_n satisfy Φ.

“(2) ϒ(v f 1 ), . . . , ϒ(v f n ) satisfy Φ, i.e. ϒ(v f 1 ), . . . , ϒ(v f n ) |= Φ”

• AssumptionThe authors state this as an assumption: Every variable x_i in function f is annotated by f to enforce its global uniqueness.

The method only works with simple DSLs without recursion, loops, or let bindings.

“our method only works with simple DSLs without recursion, loops, or let bindings.”

Higher memory usage for comparators is attributed to more complex relational specifications involving multiple properties such as reflexivity, anti-symmetry, totality, and transitivity.

“Second, the relational specification for comparators is more complex and involves multiple properties such as reflexivity, anti-symmetry, totality, and transitivity.”

Lemma A.1: For any tree t accepted by FTA A built with grammar G and initial states using rules from Figure 8, t conforms to grammar G.

“Given a tree t(x 1 , . . ., x m ) that is accepted by A, we have (1) t conforms to grammar G.”

Given a relaxed relational specification Φ, the algorithm builds an HFTA H that recognizes exactly those programs that satisfy Φ.

“Given a relaxed relational specification Φ, our algorithm builds an HFTA H that recognizes exactly those programs that satisfy Φ.”

• AssumptionThe authors state this as an assumption: Every variable x_i in function f is annotated by f to enforce its global uniqueness.

For any hierarchical tree T accepted by H, the program assigned to each function symbol f_i conforms to grammar G(M^{-1}(f_i)).

“(1) ϒ(v f i ) is a program that conforms to grammar G(M -1 (f i ))”

• AssumptionThe authors state this as an assumption: Every variable x_i in function f is annotated by f to enforce its global uniqueness.

Higher memory usage for comparators is attributed to most comparator benchmarks requiring more CEGIS iterations to solve and therefore resulting in larger HFTAs.

“Finally, most benchmarks in the comparator domain require more CEGIS iterations to solve and therefore result in larger HFTAs.”