{'fraction_non_alphanumeric': 0.032782065417126055, 'fraction_numerical': 0.010216832047041529, 'mean_word_length': 4.521577380952381, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 42, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Type-Directed Synthesis of Visualizations from Natural Language Queries

We propose a new technique based on program synthesis for automatically generating visualizations from natural language queries. Our method parses the natural language query into a refinement type specification using the intents-and-slots paradigm and leverages type-directed synthesis to generate a set of visualization programs that are most likely to meet the user's intent. Our refinement type system captures useful hints present in the natural language query and allows the synthesis algorithm to reject visualizations that violate well-established design guidelines for the input data set. We have implemented our ideas in a tool called Graphy and evaluated it on NLVCorpus, which consists of 3 popular datasets and over 700 real-world natural language queries. Our experiments show that Graphy significantly outperforms state-of-the-art natural-language-based visualization tools, including transformer and rule-based ones.


INTRODUCTION
Natural language interfaces (NLIs) [Gao et al. 2015;Sun et al. 2010;Yu and Silva 2020a] for visualization promise to democratize the visualization authoring process. Given a dataset (often a relational table) and a natural language description, an NLI can generate a set of visualizations that most likely meet the user's intent. For instance, given the dataset shown in Figure 1 and a query such as "give me a scatter plot that shows the fuel economy of all car models", an NLI can, in principle, generate the scatter plot shown on the right side of Figure 1. In this way, even a user with no programming experience can generate visualizations from large-scale data.
While existing NLIs are effective in producing relatively simple visualizations, a recent study  found that these tools are unable to generate more complex visualizations, such as those that involve subplots or that require performing non-trivial transformations on the input data. For example, for the input query "generate a graph to show the fuel efficiency for cars from   different countries segregated based on body style" and the dataset from Figure 1, state-of-the-art tools return the plot shown in Figure 2b as opposed to the ideal plot shown in Figure 2a.
In this paper, we propose a new technique for generating visualizations from natural language descriptions. Our method combines NLP techniques with program synthesis to address several challenging aspects of data visualization. In particular, our technique can handle fairly ambiguous natural language queries, including those that do not fully specify the desired plot type. In addition, our method can perform transformations and aggregations on the input data, allowing it to handle visualizations that require non-trivial data wrangling. As an example, our method can produce the correct plot, shown in Figure 2a, for the input query mentioned earlier.
At the heart of our technique lies a refinement type system that can be used to express properties of the desired visualization. At a high level, our method first uses state-of-the-art NLP techniques, namely a BERT-based [Devlin et al. 2019] intent-and-slots model [Tur et al. 2010], to parse the natural language description into a set of likely refinement type specifications for the desired visualization. Then, for each refinement type specification, our method performs type-directed program synthesis to generate a set of visualization programs of the appropriate type, using a notion of type compatability to prune large parts of the search space. Hence, the refinement type system is useful not only as a specification mechanism but also for guiding synthesis and reducing the search space.
A distinguishing feature of the synthesis problem in our setting is that a single visualization task typically results in many synthesis problems, one for each refinement type specification inferred by the parser. However, because each invocation of the synthesizer can be quite expensive, it is important to reuse information across different synthesis problems. Our approach addresses this concern by learning so-called synthesis lemmas that can be used to prove unrealizability of future synthesis tasks. In particular, our approach leverages a novel notion of refinement type interpolants to learn useful facts that can be reused across different synthesis goals involving the same data set.
We have implemented our proposed approach as a new tool called Graphy and evaluated it on NLVCorpus , which consists of 3 popular visualization datasets and over 700 real-world natural language queries. Our evaluation demonstrates that Graphy yields significantly better results compared to existing state-of-the-art baselines, including transformer and rule-based NLIs. We also perform ablation studies to evaluate the importance of our proposed techniques and show that they all contribute to making our approach practical.
To summarize, this paper makes the following key contributions: • We propose a new synthesis-based technique for generating visualizations from an input data set and natural language description. • We introduce a refinement type system that is useful both as a specification mechanism and for guiding program synthesis. • We describe a technique based on the intents-and-slots paradigm for parsing natural language descriptions into refinement type specifications. • We propose a type-directed synthesis algorithm that uses a notion of type compatibility to prune the search space and learns synthesis lemmas that are useful across different synthesis attempts. • We implement our approach in a tool called Graphy and perform a large-scale evaluation on over 700 real-world visualization tasks.

OVERVIEW
We give a high-level overview of our technique with the aid of the motivating example introduced in Section 1. In particular, consider the dataset from Figure 1 listing the fuel economy of different cars and the following natural language query: "Show the fuel efficiency of cars from different countries segregated based on body style" Given this query, our tool, Graphy, generates the visualizations shown in Figure 3. Among the plots shown here, the top one is the intended one, with corresponding visualization script shown in Figure 4. We now explain how Graphy is able to generate these visualizations, highlighting salient features of our approach.
Structure of visualization programs. Similar to prior work , the visualization programs synthesized by Graphy consist of two parts, namely a table transformation program and a plotting program (see Figure 4). Given these programs, Graphy produces a visualization by first applying to the input data set to obtain a transformed table and then applying the plotting program to . Since many real-world visualizations tasks require non-trivial data wrangling, synthesis of table transformations is a crucial aspect of the Graphy workflow. We describe the domain-specific language used for visualizations in more detail in Section 3.
Motivation for refinement types. As mentioned in Section 1, Graphy parses the natural language query into a formal specification rather than going directly from natural language to a visualization program. This design choice hinges on two key observations: First, the natural language description often does not contain sufficient information to map it directly to a program. For instance, in our running example, the NL query does not mention anything about a bar graph. Second, the data set to be visualized also contains valuable information for deciding which visualizations make more sense. As an example, looking at the data set, we see that fuel economy is continuous (as opposed to discrete), so it would not be suitable as the x-axis for a bar graph. For these reasons, Graphy parses the NL query into an intermediate specification, which is then supplied as an input to the synthesizer.
In this work, we use refinement types as our specification because both base types and logical qualifiers are useful for guiding synthesis. In particular, record types are useful for distinguishing between different types of tabular data, and logical qualifiers capture other forms of hints present in the natural language. For instance, based on the natural language query given above, it is reasonable to conjecture that the color encoding of the plot should be based on country, and our type system allows expressing such information as part of the logical qualifier. We discuss our refinement type system in more detail in Section 4.
From NL queries to refinement types. As a precursor to synthesis, Graphy first uses state-ofthe-art NLP techniques to extract refinement type specifications from the natural language query. In particular, the extracted specifications are of the form (T , T ), where T is the output type for the plotting program and T is the output type for the table transformation program. Intuitively, we parse the NL query into two different refinement types as our synthesis procedure generates the plotting and table transformation programs independently.
Our technique for parsing a natural language query to a refinement type consists of two steps. First, we use the technique of intent classification [Tur et al. 2010] to infer some of the base types (e.g. BarPlot, ScatterPlot) as well as which types of predicates should be involved in the logical qualifier. For our running example, the intent classifier is able to predict that the desired plot is a BarPlot based on the training data. In addition, note that the NL query hints at the fact that the color encoding of the plot is based on country (i.e., "Origin" column in the data set). Such information is encoded using so-called syntactic constraints in the logical qualifiers. The intent classifier can decide whether the NL query contains such syntactic constraints, but it cannot decide what the arguments of the predicate are. Hence, in a second step, we use a natural-language-processing technique known as slot filling [Jeong and Lee 2006] to decide the arguments of the inferred predicates. For our running example, the slot-filling technique can infer that the graph's color is likely to be the Origin field of the input data set and generates a logical qualifier that involves this syntactic constraint. We describe our technique for parsing the NL query into a refinement type specification in more detail in Section 5.
Synthesis workflow. Figure 5 shows the high-level workflow of our synthesis algorithm. For each specification (T , T ) generated by the parser, our synthesizer generates a set of visualization programs that satisfy it. At a high level, the synthesis algorithm first generates a plotting program such that the output type of is a subtype of T . The input type of is then used to strengthen the parsed specification T of the table transformation program to T ′ . For instance, in our running example, suppose we synthesize the following plotting program: Such a program only makes sense if there is a unique value for every ( , ) pair, so our method strengthens the output of the table transformation program with the following constraint: This constraint states that the cardinality (number of unique tuples) of the output table projected on the (Body_style) and (Origin) columns should be at least as big as the cardinality when projected onto the (Fuel_economy) column. This constraint serves as a logical qualifier for the output type of the table transformation program and is used to reduce the search space that the synthesizer needs to explore, as discussed in Section 6.1.
Type-directed synthesis. In addition to using refinement types as the specification, our technique also uses them to guide synthesis as in prior work [Polikarpova et al. 2016]. In more detail, our algorithm performs top-down enumerative search, starting with a completely unconstrained program and expanding a non-terminal (i.e., "hole") in the partial program using one of the grammar productions. Each hole is annotated with a so-called goal-type that is propagated backwards using the type system and the initial specification obtained from the NL query. As explained in more detail in Section 6.1, the goal type is used to decide (1) which grammar productions are applicable when performing top-down enumeration, and (2) whether a partial program is infeasible, meaning that its actual type is inconsistent with the annotated goal type. However, unlike prior work, our approach uses a notion of type compatibility (Section 4.3) as opposed to subtyping in order to ensure that we do not rule out correct programs.  Figure 1. Here, the goal type comes in the form of a refinement type that describes the base type Table(Model : Discrete, Fuel_economy : Qualitative) annotated with the predicate ( .Model, count). The base type describes a table with attributes Model and Fuel_economy, whose types are Discrete and Qualitative respectively. The qualifier, ( .Model, count) is a syntactic constraint that indicates that the Model attribute of the output table is obtained by applying the count operation. During synthesis, Graphy starts with a program that is a single hole and iteratively expands it using productions in the grammar. Whenever Graphy expands a hole, it propagates the above goal type to newly produced holes in the partial program. For instance, Figure 6 shows a partial program with the annotated goal type of node 2 . Using our type system, Graphy can prove that this partial program is infeasible because the actual type of the term rooted at node 2 is incompatible with its annotated goal type. This is because Fuel_economy has type Continuous in the input table, which is inconsistent with the goal type labeling node 2 , where Fuel_economy is required to be Qualitative.
Type-directed lemma learning. A unique feature of our approach is its ability to learn synthesis lemmas that can be used across different synthesis tasks involving the same data set. 1 To see why such lemmas are useful, recall that we want to generate multiple visualizations to show to the user, so we need to explore many different programs that could be consistent with the NL query. In general, there are multiple plausible specifications one can extract from the NL query, and there are multiple programs that satisfy each specification. Hence, our approach needs to explore many different programs during a single visualization session.
Our approach addresses this concern by using the type system to learn synthesis lemmas. In particular, a synthesis lemma is a pair of refinement types ( , ) such that any program with goal type also needs to be "consistent" (in a sense made precise in Section 4) with refinement type . Hence, if we encounter a synthesis goal (or sub-goal) that is a subtype of but that is inconsistent with , we immediately conclude that the synthesis task is infeasible. Our synthesis algorithm learns such lemmas by inferring so-called refinement type interpolants whenever it encounters an infeasible partial program. We discuss the algorithm for type-directed lemma learning in Section 6.2.
Going back to our running example, consider the same infeasible partial program in Figure 6. The root cause of this failure is that the program was unable to convert the Fuel_economy column from a Continuous type to Qualitative. In fact, no program in our DSL can achieve this transformation. Graphy automatically captures this fact by generating the following synthesis lemma:

DOMAIN-SPECIFIC LANGUAGE FOR VISUALIZATIONS
In this section, we introduce the domain-specific language for visualization programs. As in prior work ], a visualization program in our setting first performs the necessary table transformations to obtain an intermediate table and then generates a plot based on . Hence, as shown in Figure 7, a visualization program can be expressed as the composition of two programs  and , where , are programs expressed in the so-called table transformation and plotting DSLs, respectively. In the remainder of this section, we discuss the syntax and (informal) semantics of these two DSLs in more detail.
Plotting DSL. A program in our plotting DSL takes in an input table and outputs a plot, which can be one of four types: (1) bar graph, (2) scatter plot, (3) line plot, or (4) area plot. Figure 8 shows an example of each type of visualization supported by our plotting DSL. In more detail, a plotting program is of the form ( , x , y , color , subplot ) where specifies the plot type, is the input table, and the remaining arguments are attributes of . Specifically, the x , y columns specify the x-and y-axis of the plot and are required for every program in the plotting DSL. The remaining two arguments color and subplot are optional and only make sense for plots with multiple layers or subplots (or both). In particular, the color attribute is useful for plots that require multiple layers and specifies that each different color in the plot corresponds to a different value of the color column. Finally, the optional fourth argument specifies that each distinct entry in the subplot column should be used to generate a different subplot.  Figure 7, a table transformation program takes in an input table , and outputs a table by applying a sequence of transformations that are inspired by relational algebra and supported by many popular visualization languages, such as VegaLite and ggplot2. In particular, our table transformation DSL includes the following useful constructs: • The bin operation discretizes a numeric column in the table tgt into a set of bins. Here, the argument specifies the number of bins that the entries in tgt should be split into. For example, in the first input table shown in Figure 9, column 2 is binned.  • The filter construct corresponds to the standard selection operation in relational algebra. Given a table and predicate of the form , it produces a subset of consisting of all tuples that satisfy . The second illustration in Figure 9 offers an example of the filter operation.
• The summarize construct performs an aggregation operation specified by on a specified column tgt . In more detail, given an input table and "keys" (i.e., columns) key = [ 1 , . . . , ], it produces a new table that has columns 1 , . . . , , tgt such that for each value of the tuple ( 1 , . . . , ), the corresponding value of tgt is obtained by applying the aggregation operator to those entries that have the same value for ( 1 , . . . , ). In the third illustration in Figure 9, column 2 is summarized by the count operator.
• The mutate construct produces a table that has one more column tgt than its input table. In particular, the value stored in tgt is obtained by applying operator to the corresponding values stored in columns args . In the fourth illustration in Figure 9, the mutate operator creates column 3 by taking the max of columns 1 and 2 .
• The select construct corresponds to the standard projection operation in relational algebra. In particular, select( , args ) yields a table containing only the columns args . Observe that the first argument of each operator is a term in the table transformation DSL; thus, these transformations can be arbitrarily nested within one another. Hence, the table transformation DSL allows performing non-trivial data wrangling tasks that require applying many different operations to the input table.

OVERVIEW OF REFINEMENT TYPE SYSTEM
While the visualization DSL introduced in Section 3 does not have explicit type annotations, our approach leverages a refinement type system that facilitates effective synthesis. The design of our type system is based on two pragmatic considerations: first, we want our refinement types to serve as useful specifications, meaning that they should capture the clues that are commonly found in natural language descriptions of visualization tasks. Second, we want our type system to be useful for pruning infeasible parts of the search space during synthesis. With these considerations in mind, we introduce those aspects of our refinement type system that are necessary for understanding the overall synthesis approach.

Type Syntax
As standard [Rondon et al. 2008], a refinement type is of the form { : | } where is a base type and is a logical qualifier. As shown in Figure 10, base types include strings, integers, four different types of plots, and tables. A table type Table( ) denotes a table with schema , which maps each column name (attribute) to its column type, which indicates the type of values stored under that column. The column type ⊤ indicates any type of of data, whereas Quantitative and Qualitative indicate whether the entry is associated with a quantity or quality respectively. Quantitative data Base Type Fig. 10. Type Syntax. is a column name; are values in the Table; is an integer; is a variable.
can be further divided into Continuous and Discrete, and Qualitative data can be divided into Nominal, Ordinal, and Temporal (e.g., date or year). In contrast to base types, logical qualifiers are formulas formed from atomic predicates using the standard logical connectives ¬, ∧, and ∨. We differentiate between two types of atomic predicates, namely syntactic constraints (..) and table property predicates of the form ≬ . We discuss both types of atomic predicates in more detail below.
Syntactic constraints. Given a table or plot with attribute , the predicate ( . , ) expresses that was used in the derivation of . . Here, is either a built-in function in our DSL (e.g., count, mutate) indicating that function was involved in the computation of . , or a term of the form ′ . ′ indicating data flow from ′ . ′ to . . Intuitively, the syntactic constraints in our type system allow encoding useful hints present in the natural language description about the origin of the data used in the visualization task.
Example 4.1. For the running example from Section 2, our NL parser generates the following type for the output of the plotting program: where refers to the input of the plotting program. Here, the base type indicates that we want a bar graph, and the syntactic constraint indicates that the color encoding is bound to the Origin field of the input table. In other words, it indicates that colors in the plot correspond to values of the Origin column.
Table properties. In addition to the syntactic requirements, our type system allows expressing properties of tables using predicates of the form ≬ where is a term and ≬ is a relation symbol (e.g., ≤). In more detail, terms can be formed using the following constructs: • Given a variable of type Table, | | represents the cardinality of (i.e., number of unique tuples).
• The functions Proj and Filter have the same semantics as the corresponding constructs in our table transformation DSL. • Given a column , the aggregation operators max( ) and min( ) return the maximum (resp. minimum) value in .
Intuitively, table property predicates are useful for specifying the table transformation component of the visualization task and provide significant pruning power during synthesis.
Example 4.2. Consider the following refinement type: This type describes a table that (1) has two attributes, Price and Origin, of types Discrete and Nominal respectively, (2) contains three unique tuples, and (3) has a maximum value of 8 in its Price column.

Subtyping
Given a refinement type specification T, the goal of our approach is to synthesize a visualization program of type T ′ such that T ′ is a subtype of T. Thus, we start by formalizing the subtyping relation for our type system using judgments of the following form: where Γ is a type environment mapping variables (and built-in DSL functions) to their corresponding types. As standard, the meaning of this judgment is that T 1 is a subtype of T 2 under type environment Γ. Since deciding subtyping between base types does not require the type environment, we omit the type environment for base types. Figure 11 presents our subtyping rules. The first several rules are straightforward and show the subtyping relation between primitive types like Discrete and Quantitative. The subtyping rules for tables are essentially standard subtyping rules for records [Pierce 2002]. The last two rules for refinement types are also standard and require (1) checking the subtyping relation between base types and (2) checking the validity of a logical formula for the logical qualifiers. In particular, these rules make use of a function called Encode that converts the logical qualifier of a refinement type into an SMT formula. The interested reader can find details of the SMT encoding in the appendix.

Type compatibility
While our synthesis algorithm ensures that the type of the synthesized program is a subtype of the specification, we utilize a weaker notion of type compatibility for pruning during synthesis. In particular, because our synthesis algorithm needs to reason about the feasibility of incomplete programs (where some parts are yet to be determined), we introduce a notion of type compatibility that is much weaker than subtyping. Intuitively, two types T 1 and T 2 are compatible with each other if there exists a subtype T of T 1 that is also a subtype of T 2 . Conversely, if two types T 1 and T 2 are incompatible, there is no refinement of T 1 that will make it a subtype of T 2 . As we will see in Section 6, the notion of type (in)compatibility is very useful for pruning during synthesis. In this section, we formalize this notion and present rules for checking type compatibility. We define the compatibility relation for our type system using judgments of the form: 12. Base and refinement type compatibility relation stating that T 1 is compatible with T 2 under environment Γ, as shown in Figure 12. Unlike the subtyping relation, the compatibility relation is symmetric (first rule in Figure 12); however it is not transitive. The second rule in Figure 12 defines the type compatibility relation for primitive types and states that they are compatible if one is a subtype of the other or vice versa. The third rule ( Table) asserts that two table types are compatible when all their shared columns are compatible. The intuition is that if all shared columns are type compatible, then we can construct a new table type that is a refinement of both by taking the union of their schemas. Finally, Refinement-Comp and Func are similar to their subtyping counterparts in that they reduce the compatibility check to an SMT query. However, there are two key differences. First, the encoded formula is a conjunction of the qualifiers as opposed to an implication. Second, we check that the encoding is satisfiable as opposed to valid. The intuition behind this rule is that, if the resulting formula is satisfiable, then { : T | 1 ∧ 2 } is a well defined type in our type system that has at least one inhabitant, and it refines both { : T | 1 } and { : T | 2 }.

Typing Rules
In this section, we give an overview of our typing rules for assigning types to DSL terms. In particular, our typing rules derive judgments of the form Γ ⊢ : T to indicate that term has type T under environment Γ. Since the typing rules are not the primary focus of this paper, we only discuss two representative rules and leave the rest to the appendix.
Typing rules for the plotting sub-DSL. To illustrate the typing rules for the plotting sub-DSL, Figure 13 shows the rule for the Bar construct, which generates a bar graph given table . At a high level, this rule states that if 's type satisfies two constraints, then the output type will be a refinement of BarPlot. The first constraint is that 's schema must be suitable for generating bar graphs, meaning that x is Discrete and y is Quantitative. This requirement is captured by the second premise. In addition to having a suitable schema, another important requirement for a bar graph is that it should not have overlapping bars, meaning that the x-label in each subplot must correspond to a unique y-value. This requirement is captured through the cardinality constraint in the third premise, which checks that the logical qualifier for implies that there is unique 14. Typing rule for Summarize instantiated with a Mean operation. We use notation ( , { 1 , . . . , }) as a shorthand for Proj( , { 1 , . . . , }), and the operator is defined in the text.
for each . If these premises hold, then the entire term is well-typed with base type BarPlot and a logical qualifier stating the syntactic constraint for the return value of Bar. In particular, the logical qualifier in the conclusion states, for example, that the x attribute of the plot is derived from the x attribute of the input table .
Typing rules for table transformation sub-DSL. Figure 14 shows the typing rule for the summarize construct in our table transformation DSL. Recall that summarize takes as input an aggregation operator, and the type depends on which aggregation operator summarize is invoked with. In Figure 14, we consider instantiating summarize with mean as a representative example. To understand this typing rule, let us first recall the semantics of summarize, which associates each unique value of the specified key columns with the mean of the values in the specified target column (see Figure 9). The first two premises in the typing rule Summ-Mean impose some requirements on the input table. In particular, because it only makes sense to take the mean of quantitative values, the second premise ensures that the target column has a suitable type. Furthermore, since the mean operation produces a value of type Continuous, the column has type Continuous in the output table with base type ′ . The fourth and fifth lines in Figure 14 state the relationship between the logical qualifiers of the input and output tables. To that end, given a logical qualifier and a set of terms , we use the notation to denote the strongest logical qualifier ′ that is implied by and that does not imply anything about any term ∈ . 2 Thus, according to our typing rule, the new logical qualifier ′ for the output table differs from the qualifier for the input table in the following ways: First, it "removes" from any knowledge about the terms that involve tgt which are affected by the summarize operation. Second, it asserts that the number of unique tuples over is greater than or equal to the number of unique values in tgt . This is because the cardinality of the output table is equal to the number of unique ( 1 , . . . , ) values where each ∈ . However, as two distinct ( 1 , . . . , ) values could have the same value for tgt , we cannot infer a stronger constraint. Finally, since the values of tgt were produced by the mean operation, ′ includes the syntactic constraint ( . tgt , mean).

FROM NATURAL LANGUAGE TO REFINEMENT TYPES
In this section, we describe a technique for generating refinement type specifications from natural language queries. At a high level, we frame this problem as an instance of the intents-and-slots problem [Jeong and Lee 2006;Tur et al. 2010] and build a parser that combines intent detection and slot filling on top of the BERT language model [Devlin et al. 2019].

Background on Intents-and-Slots-Paradigm
The intents-and-slots paradigm is a classical paradigm in the NLP literature on task-oriented dialog systems [Dahl et al. 1994;Hemphill et al. 1990;Tur et al. 2010] and flexibly supports many types of 2 One way to obtain is to replace all occurrences of with a fresh existentially quantified variable and then eliminate the quantifier. We formalize the operator in the appendix.
s 2 U 4 K 5 + e Z 1 0 m w 3 3 q t F 8 v K 6 3 7 s o 6 q n A G 5 3 A J L t x A C x 6 g D R 0 g M I N n e I U 3 K 7 N e r H f r Y z l a s c q d U / g D 6 / M H K H q T / w = = < / l a t e x i t > h CLS < l a t e x i t s h a 1 _ b a s e 6 4 = " 6 1 p / u 9 1 P l u z X P j w R L S j o E P s 9 a S V c z s g z + y P n 8 A L d + X 7 Q = = < / l a t e x i t > Fig. 15. Model architecture for the color encoding property in the running example. The yellow box represents the contextualized embedding of the query. Blue boxes represent the BERT embedding for each of the columns names in the table. After applying a linear layer to the BERT encoding in each task, we obtain a probability distribution across all possibles classes. The one with the highest probability is highlighted with pink.
user interactions, as evidenced by its adoption on Amazon Alexa and other dialog platforms. At a high level, intent classification is the problem of determining the topic of a query from a natural language utterance. For instance, given a set of topics such as "flights", "movies", "restaurants", intent classification can be used to determine which of these topics a sentence is about. Once the intent of the utterance is identified, slot filling determines pre-defined properties of that topic. For example, if the topic of a query is "flights", relevant parameters include airline, destination city, flight number, etc., and slot-filling techniques aim to identify these parameters.
As a concrete example, consider the query "What flights are available from San Francisco to New York?" Here, an intent classifier aims to determine that the topic of the query belongs to the flight category as opposed to movies or restaurants. Then, assuming that the flight category has attributes such as departure and destination city, a slot-filling technique can be used to determine that the departure city of the query is San Francisco and that the destination is New York.
The intents-and-slots paradigm is a good fit for our setting for two main reasons. First, compared to conventional semantic parsing [Zelle and Mooney 1996;Zettlemoyer and Collins 2005], the intents-and-slots framework does not make strict assumptions about the grammatical structure of inputs. As a result, it can more flexibly handle user inputs that do not conform to a pre-defined syntax. Second, user queries in our setting can be naturally classified into different intents based on (1) the type of the plot (e.g., bar graph, scatter plot, etc.) they refer to and (2) which predicates in our refinement type system they involve. Furthermore, the arguments of these predicates can be determined using the slot-filling paradigm.

Parsing Technique
In this section, we explain our instantiation of the intents-and-slots paradigm for our setting.
Overview. We have identified six types of properties that are typically mentioned in natural language queries and that are useful to the synthesizer. These include the following: Our parser uses six different intent classifiers, one for each category listed above. With the exception of plot type, all intent classifiers are binary and yield a yes/no prediction. In the case of a "yes" prediction, our parser uses slot filling to predict which attribute in the source data set this operation is associated with. For plot types, the intent classifier predicts whether the query refers to a bar chart, scatter plot, line graph, or area plot.
Input to BERT. Our method performs the predictions outlined above using a fine-tuned BERT model, with a shared encoder for both intent classification and slot filling as illustrated in Figure 15. The input to BERT is of the following form: where is the natural language query, 1 , . . . , denote column names from the input table , and [CLS] and [SEP] are standard placeholder tokens. We include the column names as part of the input for two reasons. First, when performing slot filling, the model needs to predict attributes of the source table, so we will need access to embedded representations of the column names. Second, even for intent classification, information about the input table provides useful context that the BERT model can condition on. Given this input, BERT generates a contextualized encoding of each of its input tokens, where each token in the input is mapped to a dense vector representation informed by all the other tokens through BERT's attention mechanism [Vaswani et al. 2017].
Intent Classification. Our intent classifier is a model of the form ( | , ; w ), where is the set of column names for input table , and ∈ {0, 1} is a binary label for classifiers other than plot type, and ∈ {Bar, Scatter, Line, Area} for the plot type classifier. Additionally, denotes the NL input, is an index denoting the property type, and are the model weights.
As standard practice, we take the vector h CLS as the representation of the sentence, and we use ( | , , ; ) = (w ⊤ h CLS ( , )), where denotes the logistic function, making this a standard logistic regression layer with the CLS token's contextualized embedding as input. Slot-filling model. As shown in Figure 15, a property like color requires a parameter in the form of one of the column names. Crucially, such arguments cannot be predicted with a standard classification model since the column names change with each table being plotted. As such, the model must be able to place a distribution over an arbitrary set of column tokens. To address this issue, we use a pointer mechanism similar to implementations of the attention mechanism in settings like machine translation [Bahdanau et al. 2014] and document summarization [See et al. 2017]. Specifically, our slot-filling model places a distribution ( | , , ; ) over column names. We use the same BERT encodings as the intent classifiers and let where W is a square weight matrix and softmax denotes the standard softmax operation, which exponentiates and normalizes the arguments to form a probability distribution.
From BERT predictions to specifications. Recall that the input to our synthesizer is a pair of refinement types of the form (T , T ) where T is the output type of the plotting program and T is the output type of the table transformation program. We now explain how to map the predictions made by the BERT model to specifications of this form.
To generate T for the plotting program, we assign the prediction of the plot type classifier to be the base type of T . The qualifier of T consists of a conjunction of syntactic constraints output by the color and subplot models. In particular, the logical qualifier of T includes a syntactic constraint ( .color, . ) if the intent classifier for the color property predicts "yes" and the slot-filling model outputs column name .
In particular, for each model, we generate the syntactic constraint for this specific property if the intent classifier returns "yes" and populate the arguments of the predicate with the output of the slot-filling model. For instance, in Figure 15 where we focus on the color property, we first generate the predicate template ( .color, .?) where ? is to be determined by the argument classifier. Then, ? is filled by the output of the argument classifier, which in this case is Origin and the model returns the predicate ( .color, .Origin) as its final output.
The base type of T is obtained using a pre-trained model [Lin et al. 2020] that outputs the set of likely columns in the table mentioned in the query. For the logical qualifier of T , we use the predictions made by the mean, sum and count intent classifiers and their corresponding slot-filling models. For example, the logical qualifier includes a predicate ( . , sum) if the sum model predicts "yes" and the slot-filling mechanism predicts column name for the first argument.
Distribution over specifications. Our parser assigns a probability to each specification by using the probabilities output by each model. In particular, let us view a refinement type T as a set of tuples { , } where is a intent and is an attribute predicted by the slot-filling model. Then, our method assigns a probability to these sets of tuples as ({ , } ) = ( | , , ; w ) ( | , , ; W). Hence, we can rank all possible specifications from highest to lowest probability.

SYNTHESIS FROM REFINEMENT TYPE SPECIFICATIONS
In this section, we describe our synthesis algorithm which takes as input a visualization specification (T , T ) and an input table and generates all visualization programs = • such that (1) ( ) is an inhabitant of T (written ( ) ⊨ T ) and (2) ( ) is an inhabitant of T . At a high level, the synthesis algorithm is based on type-directed top-down enumerative search and uses the refinement type system from Section 4 to significantly reduce the search space. We first start by explaining the basic synthesis algorithm (Section 6.1) and then introduce the concept of type-directed lemma learning to improve the scalability of our approach (Section 6.2). Our algorithms frequently use the typing judgements from Section 4. While these typing judgments make use of a type environment, we treat the type environment as implicit and drop it to simplify presentation.

Overview of Synthesis Algorithm
Our top-level synthesis algorithm is presented in Figure 16a and works as follows: Given a table of type T and specification (T , T ), it first synthesizes a set of plotting programs P whose output type is a subtype of the goal type (line 3). In more detail, each plotting program ∈ P of type T → T satisfies the following two properties: (1) T <: T and (2) T ∽ T . The first constraint ensures that the generated visualization satisfies the user's specification, and the second constraint ensures that there is at least one input table to the plotting program that is consistent with T . Then, for each synthesized plotting program of type T → T , the algorithm synthesizes (at line 6) a set of corresponding table transformation programs P of type T → T such that (1) T ∽ T ∧ T and (2) T <: T . Note that the first condition strengthens the original specification using T (via intersection types) and ensures that there is at least one output of the table transformation program that is a valid input to the plotting program.
The key part of the algorithm is the SynthesizeGoal procedure, presented in Figure 16c, that is used to synthesize both table transformation and plotting programs. To unify presentation, SynthesizeGoal takes a few additional arguments: • G, the grammar for the DSL in which we synthesize programs • The correctness checking condition ▷ for the input type (either <: or ∽) • The correctness checking condition ◁ for the output type (either <: or ∽) At a high level, SynthesizeGoal is a top-down enumeration procedure which starts from the root symbol of the grammar and keeps expanding non-terminals until it generates a complete program. We represent the syntax of the underlying DSL as a context-free grammar G = ( , Σ, , ), where , Σ denote non-terminals and terminals respectively, is a set of productions, and is the start symbol. As standard [Feng et al. 2018], we formalize our top-down enumeration procedure using the notion of partial programs: Definition 6.1 (Partial program). A partial program is a sequence ∈ (Σ ∪ ) * such that * = ⇒ (i.e. can be derived from via a sequence of productions). We refer to any non-terminal in as a hole, and we say that is complete if it does not contain any holes.
In the remainder of this section, we represent each partial program as an abstract syntax tree (AST) ( , ) with nodes and edges . Each node ∈ is represented as a pair ( , T ) where is a node label (either a terminal or non-terminal symbol in G) and T is the goal type of the subprogram rooted at . The goal type T of a node serves as a necessary correctness condition such that if the sub-program rooted at does not satisfy T , then the whole program cannot satisfy its specification. For a node , we use the notation ( ) to denote the subtree of rooted at , and use Label( ) and GoalType( ) to refer to the label and goal type of , respectively. Finally, we refer to a node as complete if the subtree rooted at is a complete program.
With this notation in place, we now describe the basic version (everything not underlined) of SynthesizeGoal in more detail. Our algorithm maintains a worklist W of partial programs and iteratively grows it. At the beginning, W is initialized to be the empty program 0 with a single node 0 annotated with the grammar start symbol G and top-level goal T . The loop in lines 4-18 dequeues a program from the worklist with type T T and checks if it is complete and whether it satisfies the correctness conditions. If so, this program is added to the set S containing all synthesis results. Otherwise, SynthesizeGoal calls Expand at line 12 to generate a new set of partial programs by expanding a hole ℎ in . Similar to prior work [Feser et al. 2015;Polikarpova et al. 2016], when Expand generates a new partial program ′ , it propagates the goal type at ℎ to its children. However, the goal types we infer are necessary conditions for correctness with respect to type compatibility (as opposed to subtyping) and are derived based on the premises of the typing rules from Section 4.4. In other words, the types of all subprograms must be compatible with their propagated goal type in order for the overall program to be compatible with its goal type.
Next, for each expansion ′ of , the TypeIncompatible procedure (presented in Figure 16b) uses our refinement type system to check whether ′ is infeasible. To do so, it iterates over all nodes and checks whether the subtree rooted at that node is a complete program (line 3). If so, it infers the type T of this sub-program using our type system (line 4) and queries whether T is type-compatible with the goal type of . Theorem 1. Let be a partial program with input type T and top level goal type T . If TypeIncompatible( ) returns true, then for any completion ′ of , ′ ̸ ∽ ( : T T ).

Type-Directed Learning
We now describe our type-directed learning technique that refines the basic synthesis algorithm from the previous subsection. The motivation for this technique is that we need to synthesize many programs during each visualization session. To leverage the similarities across all these synthesis tasks, our algorithm learns so-called synthesis lemmas that capture inferred constraints for the input data set. While this idea is somewhat similar to the notion of conflict-driven learning in prior synthesis work [Feng et al. 2018], there are two key differences. First, our learned lemmas can be reused across different specifications as long as the input data set is the same. Second, the learning of the synthesis lemmas is type-directed and leverages our refinement type system. for all ∈ Nodes( ) do 3: if IsComplete( ( )) then 4: T ← TypeOf( ( ));

5:
if ⊢ T ≁ GoalType( ) then  (c) Goal type synthesis algorithm. Fig. 16. Procedures for program synthesis. In SynthesizeVis, G is the grammar for the plotting sub-DSL and G is the grammar for the table transformation sub-DSL. T ∧ T stands for the intersection type of T and T . We provide the procedure for computing type intersection in the appendix.
Definition 6.2 (Synthesis lemma). A synthesis lemma for an input table is a pair of refinement types ( , ) such that, for any program and type T satisfying T <: , if ( ) is an inhabitant of T, then we have T ∽ .
In other words, a synthesis lemma captures additional (learned) constraints that the synthesized program must satisfy if its output type is to be a subtype of . Given a lemma ( , ) and partial program , the basic idea is to use for pruning as follows: If the desired goal type T of is a subtype of but T is not type-compatible with , then we can prune without even attempting synthesis. Hence, such lemmas can be useful both for proving the unrealizability of a top-level synthesis goal as well as pruning the search space during synthesis.
Given a lemma ( , ), we refer to as the guard of the lemma and as the requirement. We also say that a lemma is activated if the goal type of the synthesis task is a subtype of . Clearly, the more general the guard of the lemma, the more pruning opportunities that lemma provides.
Pruning with lemmas. To understand how our synthesis procedure utilizes such lemmas, observe that the SynthesizeGoal algorithm from Figure 16c invokes the ViolatesLemma procedure shown in Figure 17a. Given a partial program and a lemma ( , ) ∈ Φ, this procedure checks if there exists some hole in that violates that lemma. In particular, a hole ℎ with annotated goal for all ∈ CompleteNodes( ) do 4: T ← TypeOf( ( ));

5:
if ⊢ GoalType( ) ≁ T then  type T violates the lemma if is activated (i.e., T <: ) and T is incompatible with requirement . If this type compatibility check fails for any of the holes, then guaranteed to be infeasible.
Theorem 2. Let be a partial program with input type T for table and whose top level goal type is T . If ViolatesLemma( , Φ) returns true, then ( ) is not an inhabitant of T .
Learning lemmas. Next, we discuss how to use our refinement type system to infer these synthesis lemmas. As shown in line 16 of Figure 16c, our synthesis technique invokes a procedure called InferLemmas (presented in Figure 17b) every time it encounters an infeasible partial program. In order to generate useful lemmas, we introduce the notion of type interpolants that are inspired by Craig interpolation [Craig 1957] in logic. Intuitively, type interpolants allow our algorithm to learn lemmas with generalizable guards that can be activated in many contexts. Definition 6.3 (Base type interpolant). Given two incompatible base types 1 and 2 , we say that is a base type interpolant for 1 and 2 if (1) 1 <: , (2) ≁ 2 , and (3) for any ′ such that <: ′ , we have ′ ∼ 2 .
Next, we generalize this notion from base types to refinement types: Definition 6.4 (Refinement type interpolant). Given two refinement types T 1 = { : 1 | 1 } and T 2 = { : 2 | 2 }, we say that T is a type interpolant for T 1 and T 2 if: • 1 ≁ 2 , then T is the base type interpolant for 1 and 2 • 1 ∼ 2 , then T = { : 1 | } and is a Craig interpolant for 1 and 2 Example 6.2. Let T 1 = { : With these definitions in place, we now describe InferLemma in more detail. Given an infeasible partial program , InferLemma first iterates over every complete node in and checks whether 's goal type and actual type are incompatible (lines 4-5). If they are, it proceeds to generate a Fig. 18. GenReq procedure where describes an upper bound on the maximum AST depth of the function to be synthesized. is the desired input type and is a base type that the output must be compatible with.
lemma ( , ) where is a type interpolant between 's goal and actual types (lines 6) and the requirement is generated using the call GenReq (line 8). Intuitively, the use of type interpolants allows learning lemmas whose guards are as general possible so that they are frequently activated.
The GenReq procedure for generating a requirement is presented as inference rules in Figure 18. At a high level, GenReq infers DSL constructs that must be used in order to satisfy the goal type and expresses these as syntactic constraints. In more detail, this procedure takes three inputs: (1) the base type for input table , (2) the base type of the lemma guard, and (3) a synthesis depth which serves as an upper-bound on the AST depth of the program to be synthesized. The output of GenReq is a refinement type such that all programs of maximum AST depth and with base type → where ∽ must have an output type that is compatible with . We now explain the two inference rules from Figure 18 in more detail. The first rule, labeled Base, is the base case for the recursive GenReq procedure. In the case where = 1, GenReq finds the set of of all DSL operators such that takes as input a value of base type and produces an output whose base type is compatible with . Then, the generated requirement is that the synthesized function must contain one of the operators in : this is expressed as a disjunction of syntactic constraints, where each formula is of the form ( . , ) and is an index over the attributes of . Intuitively, this formula says that could be used to derive any of the columns in the target table's schema.
The second rule from Figure 18 handles the case for > 1. To compute a suitable requirement, it first utilizes the base case to get an encoding 1 of all programs of depth 1 whose input type is to whose output is compatible with . Next, it computes an encoding 2 of all programs of depth ≥ 2 of the form −1 • 1 where 1 is a function from to an intermediate type , and −1 is a program of depth at most − 1 whose input type is and output type is compatible with . Thus, the constraint 1 ∨ 2 encodes the requirement for all programs up to depth .
Example 6.4. Suppose = Table({colA : Qualitative}) and = Table({colA : Continuous}). Then 1 is ⊥ (false) because there is no operation that can directly transform a Qualitative column to a Continuous one. However, a Qualitative column can only be converted to a Continuous one via the count operation followed by a mean or sum. As such, 2 = ( .colA, count) ∧ ( ( .colA, mean) ∨ ( .colA, sum)). Thus, GenReq returns { : Table(

IMPLEMENTATION
We have implemented the proposed algorithm as a new tool called Graphy written in Python. In what follows, we describe key implementation details that are not covered in the technical sections.
Parser implementation and training. Our NL parser is based on the BERT implementation and pre-trained weights provided by HuggingFace [Wolf et al. 2020]. For training, our model is jointly trained on a collection of examples ( , { * , * } ) where we observe the goal properties and values for each natural language utterance. Our training loss for an example is: which is the standard negative log likelihood objective. We can optimize this objective with standard stochastic gradient descent, simultaneously training the shared BERT encoder parameters as well as the weight vectors and matrices comprising the classification layers. To implement the training procedure, we use the AdamW optimizer [Loshchilov and Hutter 2019], and train the models for 20 epochs with a batch size of 16. We provide the detailed hyperparameters including the learning rates in the appendix.
Type interpolants. Recall that our lemma generation technique from Section 6.2 utilizes the notion of type interpolants to generate guards. While computing interpolants for base types is quite straightforward, we sometimes also need to compute Craig interpolants for the logical qualifiers. In order to ensure that the overhead of this procedure does not outweigh its benefits, we use a simple template-based approach to generate interpolants. In particular, we only generate interpolants that are conjunctions of predicates and enumerate them in increasing number of atomic predicates up to a small bound. The atomic predicates are generated from a pre-defined family of predicates and instantiated with terms and constants that appear in the input formulas.
Ranking visualizations. As described in Section 5, Graphy ranks specifications based on the probabilities produced by the intent classifier and slot filling model. To break ties between programs associated with the same specification, we use the order in which they were explored during the synthesis process, which has the effect of ranking simpler programs above more complicated ones.

EVALUATION
We now describe a series of experiments designed to answer the following research questions: • RQ1. How do the results produced by Graphy compare against those of existing tools? • RQ2. How long does Graphy take to synthesize visualizations? • RQ3. How important are the refinement type system and lemma learning for performance? • RQ4. How effective do users find Graphy in generating visualizations?
Benchmarks. To answer these questions, we perform an evaluation on the NLVCorpus benchmark suite ]. NLVCorpus contains a large collection of real-world natural language queries and their corresponding ground truth visualizations for three domains, namely  Table 3. Comparison between Graphy and other tools in terms of accuracy on the NLVCorpus.
Cars, Movies, and Superstore. In total, the corpus contains over 700 queries, gathered from around 200 users and specifying a variety of visualizations. We also note that the queries in this benchmark set are quite diverse as they are syntactically unrestricted, and each user was only allowed to specify the visualizations from one of the domains. Table 1 gives a high level summary of the NLVCorpus benchmarks.
Training set for the parser. In order to use our parser, recall that we first need to train it. Hence, to evaluate Graphy on one of the domains (e.g., Cars) of NLVCorpus, we train it on the other two domains (e.g., Movies and Superstore). The training data for each of the domain is automatically generated from the corresponding ground truth visualization programs provided by NLVCorpus with no manual effort required.
Experimental Setup. All of our experiments are conducted on a machine with Intel Xeon(R) W-3275 2.50 GHz CPU and 32 GB of physical memory, running the Ubuntu 18.04 operating system with a NVIDIA Quadro RTX8000 GPU.
Graphy Configuration. In all of our experiments, we configure Graphy to terminate after it finds ten visualization programs. We sort these programs by the score obtained from the parser and break ties by prioritizing programs with smaller AST sizes.

Comparison with Other Tools
To answer our first research question, we compare Graphy against the following existing tools: • NL4DV [Narechania et al. 2021]: A state-of-the-art rule-based technique for generating visualizations from natural language. • Draco-NL [Moritz et al. 2019]: A variant of Draco, which is a visualization recommendation system that generates visualizations from a partial specification. Even though Draco does not support natural language queries by default, we implemented a custom translator that converts the output of our NL parser to partial specifications in Draco's query language. • NcNet-Original [Luo et al. 2022]: A transformer based encoder-decoder model which translates natural language queries to visualizations. This variant of NcNet was trained only on the NL2VIS dataset [Luo et al. 2021]. • NcNet-Augmented: A variant of NcNet that was trained on an augmented dataset that combines both NL2VIS and NLVCorpus. To ensure there is no overlap between the training and test data, we test on one of the domains (e.g., Cars) from NLVCorpus and train on the other two (e.g., Movies and Superstore) when performing our evaluation. • Bart-Vis [Lewis et al. 2020]: A translation-based approach that uses a fine-tuned BART language model to directly generate visualizations. We adopt a similar training and testing set-up as NcNet-Augmented. Main results. We evaluate the performance of all tools in terms of their average top-1, top-5 and top-10 accuracy with respect to the ground truth label. As summarized in Table 3, Graphy outperforms all other tools in terms of accuracy. Among these tools, NL4DV and Draco-NL are the closest competitors to Graphy; however, they both have significantly lower top-10 results compared to Graphy, and their performance fluctuates across different domains.
Running time. As demonstrated in Table 3, Graphy has better overall accuracy across the board; however, the reader may wonder if this accuracy comes at the cost of significantly longer running times. The last column in Table 2 shows the average end-to-end running time of Graphy across the three different domains. As we can see from this table, Graphy is quite fast despite performing enumerative synthesis, taking an average 5.89 seconds to complete each benchmark.
Failure analysis for the baselines. As we can see from Table 3, some of the baseline tools perform quite poorly on the NLVCorpus data set, so we try to provide some intuition about why this is the case. At a high level, machine translation-style approaches do not do well for two main reasons. First, they require the natural language query to have a complete specification of the intended plot; however, many of the queries in NLVCorpus only have partial specifications, similar to the working example from Section 2. Second, machine translation approaches do not take any logical constraints into account and may therefore end up generating non-sensical visualizations, such as a bar chart where the x-axis is associated with a continuous variable. Among the rule-based techniques, NL4DV heavily relies on the both the parsing and visualization recommendation rules encoded in the tool and therefore fails to achieve good results when the dataset becomes more complicated and rules cannot generalize. Finally, while Draco-NL utilizes the output of our parser, we observed that it produces low-quality results when the ground truth visualization requires performing non-trivial aggregation operations over the input data set.
Failure analysis for Graphy. We also analyzed the cases where Graphy does not produce the intended visualization among its top-results. In some cases, the ground truth visualization was not ranked sufficiently high, but Graphy can generate the intended visualization as we increase the value of . In most cases, however, Graphy fails to generate the correct visualization because the natural language query does not contain enough hints about the attributes that should be used to generate the visualization. In such cases, the parser is not able to infer even the base type for the output of the table transformation program, resulting in a very imprecise specification.

Ablation Study
In this section, we present the results of an ablation study to justify some of the design choices underlying Graphy.
8.2.1 Importance of refinement types. First, we quantify the impact that each component of our refinement type system has on Graphy's ability to prune infeasible programs. We do so by comparing the following three variants of Graphy: • Graphy-BaseOnly: This is a variant of Graphy that only uses base types, but no logical qualifiers.
• Graphy-SynOnly: This is a variant of Graphy that uses the base types and the syntactic constraints in the type system, but no table property constraints. • Graphy-TableOnly: This is a variant of Graphy that uses the base types and the table property predicates in the type system, but no syntactic constraints.
Given unbounded time, all of these variants will have the same accuracy as Graphy because they all check that a candidate program satisfies the specification by running it on the input table. As such, we compare the time they take to complete each benchmark (i.e., return ten visualization programs). In particular, we run each variant over all the benchmarks (with a 60 second timeout), and record the number of benchmarks each one completes along with the average time taken.
The results of this ablation study are shown in Table 4, where we report both the average synthesis time in seconds (excluding the time to parse the natural language description into a refinement type) as well as the percentage of benchmarks solved within the 60 second time limit. Compared to BaseOnly, SynOnly is almost 10× faster and TableOnly completes nearly 50 more benchmarks within the time limit. Finally, having both syntactic and table property constraints allows Graphy to complete all the benchmarks (66 more benchmarks than SynOnly) and provides an overall speedup of 28× compared to base types alone.
8.2.2 Importance of lemma learning. We also perform a second ablation study to evaluate the importance of the type-directed lemma learning technique presented in Section 6.2. To perform this study, we consider a variant of Graphy called Graphy-NoLemma that is the same as Graphy except that it does not perform type-directed lemma learning.
The results of this ablation study are presented in Figure 19, which shows the number of benchmarks completed (x-axis) within a given time limit (y-axis) when generating top-10 visualizations. As we can see from the gap between the two lines, Graphy is significantly faster than Graphy-NoLemma and achieves an overall speed of 2.1× across all benchmarks. For example, Graphy can complete 97% of the benchmarks within 2 seconds, whereas Graphy-NoLemma completes 77%.

User Study
We conducted a small user study to evaluate whether Graphy is helpful to end users. We recruited 12 participants, consisting of a mix of undergraduate and graduate students in computer science, math, and business. We asked each participant to reproduce 2 plots 4 from the Cars domain using both Graphy and Excel. For each plot and tool, we gave the participants 15 minutes to reproduce the plot using the tool.
Graphy Setup. To facilitate this user study, we developed a UI on top of Graphy. The UI allows users to enter a natural language query and presents the top 10 visualizations generated by Graphy. To avoid biasing the type of natural language query, no examples were given; participants were only told to keep the query high-level and under twenty words.
Excel Setup. We gave each participant a 10 minute tutorial demonstrating how to generate a scatter plot and perform table transformations using PivotTable. Participants were also allowed to use any online resource of their choice.
Results. When using Excel, participants could only finish 92% of the tasks within the time limit, and took 443 seconds on average to solve a task. On the other hand, when using Graphy, the participants could solve all the tasks and were, on average, nearly 12.7× faster. We give a more thorough presentation of our user study in the appendix.

RELATED WORK
NLIs for data visualization. Many visualization NLIs are powered by (1) ruled-based translation engines [Gao et al. 2015;Sun et al. 2010;Yu and Silva 2020b] that pattern-match keywords in the user input and translate them into visualization constructs, or (2) neural translation engines that leverage encoder-decoder models [Luo et al. 2021[Luo et al. , 2022 or pre-trained language models [Poesia et al. 2022] to directly generate a visualization program. Because existing systems expect the input NL to be complete specifications of the visualization task, they do not perform well in complex tasks where the query is incomplete or the task requires data transformation [Narechania et al. 2021]. Graphy addresses this issue by formulating the visualization task as a recommendation task: it first extracts an incomplete user specification from the NL query and then generates diverse recommendations from it. As shown in our evaluation, Graphy generalizes better to complex tasks and improves user experience.
Visualization recommendation systems. Visualization recommendation systems are built to help the user explore the visualization design space from incomplete specifications. For example, Draco [Moritz et al. 2019] leverages a constraint solver to recommend visualizations based on the user's design and data constraints written in answer set programs; Voyager [Wongsuphasawat et al. 2015] and ShowMe [Mackinlay et al. 2007] use heuristics to recommend visualization chart type and axes based on the user's fields of interests and the data statistics; DeepEye [Qin et al. 2018] is similar to Voyager but with a statistical learning-to-rank model to the rank visualizations. Unlike existing systems that require formal specifications (e.g., constraints, concrete fields) as input, Graphy supports visualization recommendation from natural language.
Type-directed program synthesis. Since refinement types [Martin-Lof et al. 1984;Rondon et al. 2008] were introduced, there have been a number of proposed techniques for synthesizing programs from refinement type specifications [Frankle et al. 2016;Knoth et al. 2019;Knowles and Flanagan 2009;Osera 2019;Osera and Zdancewic 2015;Polikarpova et al. 2016]. In particular, Myth2 takes a function type, along with input-output examples and generates a refinement type specification by combining the type signature and examples. Synqid [Polikarpova et al. 2016] synthesizes programs using polymorphic refinement types. At the heart of their procedures is a round-trip type checking mechanism that interleaves top-down and bottom-up propagation of type information. Graphy employs a similar approach but with two key differences: First our approach propagates necessary conditions to ensure type-compatibility as opposed to subtyping, and second, we apply type-directed lemma learning to further speedup synthesis over multiple specifications.
Program synthesis from NL. Beyond data visualization, there have also been proposals for performing program synthesis directly from natural language [Brown et al. 2020;Lin et al. 2020;Yaghmazadeh et al. 2017;Ye et al. 2021]. These techniques can mainly divided into two categories: end-to-end parsing vs parse-then-synthesize techniques. Most of the recent work from the NLP community focuses on end-to-end parsing, using either powerful generic language models [Brown et al. 2020;Lewis et al. 2020] or domain-specific techniques targeting SQL [Lin et al. 2020;, spreadsheet formulas [Gulwani and Marron 2014], and bash commands [Lin et al. 2018]. Parse-then-synthesize approaches, of which Graphy is an instance, first parse the natural language into an intermediate specification such as a sketch [Yaghmazadeh et al. 2017] or a function declaration [Gvero and Kuncak 2015] and then synthesize programs from these intermediate specifications.
Lemma learning. Graphy's type directed lemma learning strategy is most similar to the conflict analysis procedures in CDCL-based synthesizers such as Neo and Concord [Chen et al. 2020;Feng et al. 2018]. In particular, these conflict analysis procedures generate a conflict clause whenever the synthesizer determines a partial program is infeasible, and this clause is used prune many other infeasible partial programs. However, unlike Graphy's lemmas, these conflict clauses are only useful for a single synthesis task whereas Graphy's lemmas can be reused across multiple synthesis tasks so long as they use the same input dataset.

CONCLUSION
We have presented Graphy, a new synthesis-based NLI for visualizations. We evaluated Graphy on 3 datasets with over 700 natural language queries and found it significantly outperforms prior state-of-the-art approaches in top-1, top-5, and top-10 accuracy.

ACKNOWLEDGMENTS
We would like to thank Anders Miltner, Ben Mariano, Xi Ye, fellow graduate students on GDC 5S, and the anonymous reviewers for their help and feedback for this paper. This material is based upon work supported by the National Science Foundation under grant number CCF-1811865, CCF-1712067, CCF-1762299, CCF-1918889, Google under the Google Faculty Research Grant, as well as Facebook, Amazon and RelationalAI.
Similarly, since there exists a completion of +1 that inhabits its goal type, by contrapositive of Theorem 2, ViolatesLemma( +1 , Φ) will return false. +1 will thus be added to W on line 16. □ Lemma 5. (Completeness of SynthesizeGoal) Let G, T , T , ▷, ◁ be inputs to SynthesizeGoal, let be an input table with type ⊨ T , and let S be the set of programs with respect to the typing environment Γ returned by SynthesizeGoal. Then for any complete program with the most precise type T ′ T ′ in the grammar G such that ( ) ⊨ T , ∈ S.
Proof. By Lemma 4, is added to W. Note that the only termination condition for the while loop on line 4 of Figure 16c is that we exhaust W. Thus, will be dequeued on line 5 of Figure 16c at some point. Since is complete, we check if Γ ⊢ T ▷ T ′ ∧ Γ ⊢ T ′ ◁ T (line 7). Since ( ) ⊨ T , we have Γ ⊢ T ′ <: T and Γ ⊢ T <: T ′ . It then follows that Γ ⊢ T ′ ◁ T and Γ ⊢ T ◁ T ′ , so will be added to S on line 8 of Figure 16c.

C FORMULA ENCODING
In this section, we describe our Encode procedure which encodes qualifiers in our refinement type system as formulas in the combined theory of equality, uninterpreted functions, and integers.
Formula Language. Figure 23 presents the syntax of our encoded formulas as a context free grammar. Note that many of the terminals in our refinement type system also appear in this grammar but now have different semantics. The symbols | · |, Filter and Proj refer to relational operators in our refinement type system, but correspond to uninterpreted functions in the formula language. We also import column names into our formula language, but they refer to object constants. Finally, in our refinement type system, Proj takes a list of column names as its second input, whereas in this formula language, Proj takes two inputs where the second argument is an object constant.
We formalize our encoding procedure as inference rules incorporating judgments of the form.
where Σ is an environment that maps terms in our refinement type language to terms in the formula language. This judgment means: given an environment Σ and a term in the refinement type language, Encode returns the corresponding term in our formula language along with an updated environment Σ ′ . This formalization is presented in Figure 24. Most of the rules are straightforward, so we highlight the most interesting.
• Syntactic. Our encoding scheme associates each syntactic constraint ( . , ) with a unique propositional variable (Syn-1, Syn-2) • Projection. For each set of columns , we associate a fresh object constant . In particular, { 1 , 2 } and { 2 , 1 } are associated with the same fresh constant as they represent the same sets (Proj-1, Proj-2). • Filter. Every filter operator is assigned a fresh function constant , and each value is assigned a fresh object constant . Thus, the filter operation is treated as the function application ( , ).
Correctness of SynthesizeVis. Since the combined theory of integers and equality with uninterpreted functions over-approximates the semantics of our qualifiers, one may wonder whether SynthesizeVis is still complete i.e., doesn't prune correct programs. We now argue that the procedure is still complete. First, we note that our compatibility check will not prune feasible programs since (1) our encoding is the conjunction of formulas that over-approximate their corresponding qualifiers, and (2) our compatibility rule checks that the formula is satisfiable. Second, our subtyping checks are used to prune prune plotting programs whose output type is not a subtype of the goal type specification produced by the parser (line 3 SynthesizeVis). In that case, the logical qualifiers in the goal type specification are only syntactic constraints, which are precisely encoded as boolean constraints. As such, our subtyping check will not prune correct programs there.

D SEMANTICS OF OPERATOR
In this section, we describe the operator introduced in Section 4.4 in more detail. Here we assume the operator takes qualifiers of the form ∧ , where (resp ) is a boolean combination of semantic (resp. syntactic) constraints. We give the semantics of as a procedure shown in Figure 25. Given a qualifier ∧ along with a set of terms to remove, we have ∧ ≡ Remove( ∧ , ).
We now describe this procedure in more detail. In line 2 we call Encode (described in Section C) to encode our qualifiers as logical formulas. Then in lines 4-10, we iterate over all the terms in . If is a semantic term (line 5), we generate a fresh variable and replace all occurrences of in Φ with . We then update Φ to be its existential generalization (line 7). On the other hand, if is a syntactic term we perform a similar procedure, except Φ becomes a QBF formula. Finally, since the fresh variables we introduced represent the terms we want to forget, we compute the strongest formulas entailed by (resp. ) that don't contain the fresh variables. Since, QBF admits quantifier elimination [Pan and Vardi 2004], we can derive the strongest QFF formula entailed by by applying quantifier elimination (line 11). However, since our semantic constraints are expressed in the combined theory of equality, uninterpreted functions, and integers, which does not admit quantifier elimination, we instead the Cover algorithm [Gulwani and Musuvathi 2008] to compute the strongest formula (line 12). Finally, we convert Φ and Φ back into qualifiers and return their conjunction (line 13).
Optimization. In our implementation of Remove, we apply two optimizations based on the following observations. First, we observe that nearly all our logical qualifiers are conjunctions of literals, and so we represent our qualifiers as sets of literals. As such, when removing a syntactic constraint, we simply remove all corresponding literals from the set. Second, as all our semantic constraints are linear inequalities, we encode our semantic constraints as formulas in Presburger Arithemtic. We then apply Fourier-Motzkin variable elimination when removing semantic terms. We illustrate these optimizations in the examples below.
input: Logical qualifier of the form ∧ where is a boolean combination of semantic constraints, and is a boolean combination of syntactic constraints. input: A set of terms to forget output: A qualifier that does not contain any terms in and whose encoding is the strongest QFF formula that is entailed by the encoding of ∧ .

E TRAINING PARAMETERS FOR THE PARSER
Each intent-and-slot-filling model in the parser is trained for 20 epochs using the AdamW optimizer [Loshchilov and Hutter 2019] with a batch size of 16. We use a learning rate of 2 − 05 for BERT, which is one of the standard suggested learning rates [Devlin et al. 2019], a warm-up ratio of 0.05, and an input dropout rate of 0.2 to reduce overfitting [Srivastava et al. 2014]. We trained the models on one NVIDIA Quadro RTX 8000 with 48GB of memory. Each training run of the model took around 10 minutes.

F USER STUDY PROCEDURE
In this section, we describe our user-study protocol in more detail.
User study sessions. Our user study was completed in 12 sessions, one for each participant. The participants used the same laptop, which had Excel and Graphy installed, across all sessions.
Participant Introduction. We started each user study session by first describing the task that the participant needed to accomplish. In particular, we asked them to reproduce two plots shown in Figure 26 using both Excel and Graphy. We chose Excel as the baseline because it is a common data visualization tool that is designed to be accessible to non-expert users. In order to minimize the effect of knowledge transfer, we randomly determined whether a participant was first given access to Graphy or to Excel.
Plot Selection. To avoid biasing the study in Graphy's favor, we randomly selected two plots of different types from the Cars domain in NLVCorpus for the participants to reproduce. To ensure that the plots were reasonably challenging we only selected among plots that required data aggregation operations in the table transformation.
Dataset Introduction. After instructing the participants on what they needed to do, we showed them the relational table Cars that the plots are based on. We gave them 2 minutes to get familiar 1970 1972 1974 1976 1978 1980 Year 0k 0.5k with the data set and ask any questions related about it. After they were familiarized, we gave each user a training session for each tool.
Excel Training. We first introduced the Excel spreadsheet interface and showed the participants (1) how to make a scatter plot, and (2) how to do data aggregation using PivotTable, a feature in Excel that enables users to do data aggregation without any coding knowledge. Afterwards, we gave the users 10 minutes to play around with the tool. We encouraged them to try and produce a line chart and a bar chart. In addition to the training session, we also provided a "cheat-sheet" that included Excel documentation that we thought would be helpful to the user when performing the task. Finally, we allowed them to search online for help during the study.
Graphy Training. Like with Excel, we started the training by introducing the participant to Graphy's UI, shown in Figure 27. To avoid biasing the user in any way, we did not present any examples about how to use Graphy but simply asked the user to try it themselves for 5 minutes.
User Study Workflow. Once the participant was familiar with the data set and the tools, we gave them 2 minutes to familiarize themselves with the plots they needed to reproduce. We told the user to let us know when we could start timing and when they thought they had finished the task. In total, each participant had an hour to complete all the tasks using all the tools (15 minutes per task per tool). We made it clear to the participants that they were not required to reproduce exactly the same plot as shown in the ground truth, and they could consider themselves to be finished as long as they thought they had produced a plot that conveys the same meaning.
When using Graphy, users would enter a natural language query, and Graphy would return the top-10 results as visualizations back to the user. The user would then skim through the graphs and choose a visualization if they thought was equivalent to the ground truth. If the participant decided none of the visualizations shown was the one they wanted, they could try again by entering a different query. For Excel, we provided the user a spreadsheet that contained the table to be visualized so they did not need to import the data to Excel. During their time working on the plot, the user was allowed to use any resources such as searching the Internet or using the "cheat-sheet" we provide. At the end of the session, we went over the participants' solutions and collected data on how many of the tasks they successfully solved, as well as the time it took to solve them with Excel and Graphy.