Trinity is a general-purpose framework that can be used to quickly build domain-specific program
synthesizers for automating many tedious tasks that arise in data science.
End-user
From the perspective of end-users, Trinity provides a rich PBE environment that can be used to
automate various tasks that arise in data science. In particular, current synthesizers in
Trinity can generate list and table transformations, SQL queries, and programs that consolidate
values from different sources. To perform a synthesis task, the end-user specifies her intent by
using input-output examples. Additionally, the user can (optionally) also specify so-called
preference predicates that introduce inductive bias to the synthesizer. For example,
if the user thinks that the synthesized program should contain the concat function for
concatenating two strings, she can provide this information to Trinity by adding a predicate
like occurs(concat, 80%) , where 80% indicates the user's confidence that the target
program will contain the concat function. Given such a predicate, Trinity will bias its
search towards programs that contain at least one occurrence of the concat operator.
Advanced user
From the perspective of an advanced user (or domain expert), Trinity can be used to build new
synthesizers or extend functionality of existing synthesizers. For example, to build a new
synthesizer on top of Trinity, the domain expert only needs to provide a domain-specific
language (DSL) that is suitable for the target class of tasks.
In addition to the syntax of the DSL and its interpreter, the user can also provide logical
specifications for the DSL constructs in order to speed up synthesis. However, these logical
specifications need not precisely specify the semantics of the DSL construct. For example,
consider the concat operator that concatenates two strings a and b
and returns a string c . We can encode the semantics of this operator using the logical
specification len(c)=len(a)+len(b) , where len denotes the length of the string.
Note that this specification gives a partial rather than complete description of what the
concat operator does. Internally, Trinity's synthesis algorithm uses such
specifications to dramatically prune the search space of possible programs.
Synthesis expert :
For users with some knowledge of program synthesis, Trinity's synthesis engine can be
customized to more efficiently search for programs that satisfy the user-provided examples.
At its core, Trinity's synthesis algorithm performs backtracking search over DSL programs
but leverages program semantics to significantly prune the search space. Furthermore,
the search algorithm in Trinity is conflict-driven in that it can learn
useful "lemmas" based on failed synthesis attempts (i.e., conflicts).
An advanced user with some knowledge of program synthesis can further customize the
underlying algorithm in Trinity by either changing its search strategy or by
integrating a statistical model into the enumeration engine.
Check out a tutorial written by Jia Chen.
Check out our video made by Ruben Martins.
Your browser does not support the video tag.