Evanthia Dimara
email: evanthia.dimara@inria.fr

Anastasia Bezerianos
email: anastasia.bezerianos@lri.fr

Pierre Dragicevic
email: pierre.dragicevic@inria.fr

Testing the Attraction Effect on Two Information Visualization Datasets

Keywords: Negative result, information visualization, decision-making, decoy effect, attraction effect, asymmetric dominance effect, cognitive bias

The attraction effect is a well-studied cognitive bias in decision making research, where people's choice between two options is influenced by the presence of an irrelevant (dominated) third option. In another article, we report on two crowdsourced experiments showing compelling evidence that the attraction effect can generalize to visualizations. However, we also conducted another experiment between the two where we failed to observe an effect. This experiment used scatterplots generated from real datasets, and restricted participants' choice between exactly two alternatives. In accordance with the principle of full reporting, we report on this experiment and discuss the possible reasons for this negative result.

1 Introduction

The attraction effect (also called decoy effect or asymmetric dominance effect) is a well-studied cognitive bias in the psychology of decision making and in consumer behavior research, where people's choice between two options is influenced by the presence of an irrelevant (dominated) third option [START_REF] Huber | Adding asymmetrically dominated alternatives: Violations of regularity and the similarity hypothesis[END_REF][START_REF] Huber | Market boundaries and product choice: Illustrating attraction and substitution effects[END_REF][START_REF] Ariely | Seeking subjective dominance in multidimensional space: An explanation of the asymmetric dominance effect[END_REF]. Figure 1 shows an example.

The attraction effect has been so far only tested with small option sets (i.e., two alternatives plus a decoy) and simple presentation formats such numerical tables, text and pictures, but not visualizations. Since visualizations can be used to support decision-making -e.g., when choosing a house [START_REF] Williamson | The dynamic homefinder: Evaluating dynamic queries in a realestate information exploration system[END_REF], a nursing home [START_REF] Yi | Visualized decision making: development and application of information visualization techniques to improve decision quality of nursing home choice[END_REF], a financial investment [START_REF] Daradkeh | Supporting informed decision-making under uncertainty and risk through interactive visualisation[END_REF], or a software feature to support [START_REF] Aseniero | Stratos: Using visualization to support decisions in strategic software release planning[END_REF] -such an effect could have important implications.

In a separate article [START_REF] Dimara | The attraction effect in information visualization[END_REF], we report on two crowdsourced experiments showing good evidence that the attraction effect can generalize to visualizations. However, we conducted another experiment between the two experiments reported, where we failed to observe an effect despite a large sample size (n = 297). This experiment differs in two major respects from the other two: i) it uses real datasets known in the infovis domain (the "car dataset" and the "house dataset"), and ii) it uses a constrained choice task, where only two of all alternatives are available. In accordance with the principle of full reporting [START_REF] Cumming | The new statistics: why and how[END_REF] and in order to prevent publication bias [START_REF] Anderson | No result is worthless: the value of negative results in science[END_REF]The Economist, 2013), we report on this experiment here, and discuss the possible reasons for this negative result.

More extensive information on the attraction effect, the related literature, the motivations for this work, and the rationale for the methods employed can be found in the main article [START_REF] Dimara | The attraction effect in information visualization[END_REF].

Design Rationale

In the first experiment "Gyms" reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF], we found evidence for an attraction effect in scatterplots by replicating a standard experimental protocol. However, the datasets are limited to 2 or 3 alternatives, which is not realistic for a dataset people may want to visualize. The main reason for this limitation of previous work is that in numerical table representations it is hard to perform rapid attributeto-attribute comparisons, and thus recognition of dominance relationships, between many alternatives.

Scatterplots and other visualizations are designed to remove these barriers, and facilitate rapid spatial comparisons of many data points. Thus, we hypothesized that in scatterplots with many alternatives, a sufficient number of decoys will also increase the attractiveness of the target. We decided to test this in a second experiment, using sets of alternatives derived from two real datasets. In this research report we describe the motivation, design rationale and results of this experiment, referred to as experiment "Real".

A later, third experiment involving artificially generated scatterplots and referred to as experiment "Bets", is reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF], with positive results.

Additional Terminology

This section extends the terminology introduced in Dimara et al (2016)-Sections 2.2.1 and 4.2.

The Pareto front is the set of all alternatives that are not dominated in a decision task [START_REF] Ottosson | The feasibility of using pareto fronts for comparison of treatment planning systems and delivery techniques[END_REF]. In other words, it is the set of all possible choices that are not obviously "wrong". All alternatives in a Pareto front are formally uncomparable. In a classical attraction effect experiment (Figure 1), the Pareto front consists of only two alternatives: the target and the competitor.

Let T 1 be a decision task where only two choices A and B are available on the Pareto front. Let T 2 be another decision task that only differs from T 1 in that it contains additional alternatives, all dominated by A but not by B. We will refer to these additional alternatives as decoys on A, to the alternative A as the target, and to the alternative B as the competitor. These definitions are consistent with the definitions from Dimara et al (2016)-Section 4.2. Concrete examples of such cases will be provided later on.

A constrained choice task is a decision task that requires choosing an option from a subset of all the alternatives. We will refer to this subset as the choice set. A classical attraction effect experiment is not a constrained choice task, since the choice set is the same as the set of alternatives.

Stimuli and Task

As in [START_REF] Dimara | The attraction effect in information visualization[END_REF]-Experiment Gyms, we chose a 2D scatterplot to visually represent the sets of alternatives, one of the common infovis representations of large bi-dimensional datasets. This time we did not include a numerical table as a control condition, since numerical tables do not support rapid comparisons among many alternatives. Instead we looked at how the addition of decoys shifts participants' choice between target and competitor.

In numerical tables or other textual formats, people need to actively perform pairwise comparisons to see dominance relations between alternatives. According to [START_REF] Crosetto | Testing the strength and robustness of the attraction effect in consumer decision making[END_REF], the decision task in an attraction effect experiment can be broken in two stages: i) a dominance recognition stage, where participants exclude the dominated alternative; and ii) a final selection stage, where participants choose one of the two non-dominated alternatives based on their preference.

Our concern regarding the extension of attraction effect in scatterplots was that the dominance recognition task -i.e. the exclusion of multiple decoys-could be time consuming or error-prone for crowdsource participants, given the large number of alternatives. Since we were interested in the selection stage of the task, we decided to eliminate the dominance recognition part of the task by restricting participants' choice set to two non-dominated alternatives. We focused on only two alternatives instead of the full Pareto front to remain consistent with the target/competitor dichotomy used in studies on the attraction effect and to avoid interaction with other cognitive biases, as explained in [START_REF] Dimara | The attraction effect in information visualization[END_REF].

Thus, we used a constrained choice task whose the choice set consisted in two formally uncomparable alternatives picked on the Pareto front. As we can see in the stimuli shown in Figures 4,5, 6, and 7, we indicated target and competitor in red color -whereas other data points were in gray-and we labeled them as A and B. Participants indicated their choice of A and B in a radio button below the diagram.

Scenario and Attribute Values

Previous research has studied how different positions of a single decoy influence the effect, and it is believed that positions are not all of the same weight. For instance, [START_REF] Huber | Adding asymmetrically dominated alternatives: Violations of regularity and the similarity hypothesis[END_REF] found the attraction effect increasing in the dimension on which the target is the weakest (i.e., the dimension where the competitor is superior). Despite the differences in attraction intensity depending on position, the effect seems to persist regardless of where we place a single decoy [START_REF] Wedell | Distinguishing among models of contextually induced preference reversals[END_REF]. However, the decoys so far have been studied in one position at a time (single decoy), rather than having multiple decoys, at different positions at the same time, as is our case. Inria

Dataset Selection

Since we are interested in the attraction effect with many alternatives shown on scatterplots, for this second experiment we based our tasks on real datasets. We started with a corpus of five multidimensional tabular datasets containing information on houses, cars, cameras, cereals and movies 1 . These datasets are routinely used in the infovis community for the purposes of teaching, designing and demonstrating multidimensional data visualization systems (e.g., [START_REF] Elmqvist | Rolling the Dice: Multidimensional Visual Exploration using Scatterplot Matrix Navigation[END_REF]; [START_REF] Yi | Dust & magnet: multivariate information visualization using a magnet metaphor[END_REF]).

For each dataset we examined all possible 2D scatterplots and searched for distributions that were roughly linear (such as in Figure 2), indicating a trade-off between the two attributes. In addition, each attribute should be easy to understand, and as we discussed in [START_REF] Dimara | The attraction effect in information visualization[END_REF], should exhibit a clear direction of preference. For example, carbohydrate content from the cereals dataset is not a good choice of attribute, since some people might seek low carbohydrate content while others might seek the opposite, and some may not even understand what it means. Only two datasets (cars and houses) had attributes pairs that had a roughly linear relationship and where each attribute was easy to understand and had clear direction of preference. We chose a pair of attributes for each of these datasets. More specifically, the two bi-dimensional datasets we extracted from our corpus were:

• The cars dataset, a set of 407 car models from America, Japan and Europe manufactured from 1970 to 1982, described according to their horsepower and their fuel efficiency in miles per gallon. • The houses dataset, a set of 781 real estate listings in the San Luis Obispo area from 2009, described according to their size in square feet and their price in US dollars. Although the car and real estate markets have significantly evolved since the data was collected, the trade-offs involved remain the same and thus decision making tasks should not be impacted.

Dataset Preparation

We cleaned up the chosen datasets by i) removing all duplicate alternatives -i.e., houses or cars with identical attribute values, and ii) removing alternatives more than two standard deviations away from the mean on either of their two attributes. This prevented outliers from excessively compressing the scales of the scatterplot axes. A total of 61 duplicates and 37 outliers were removed from the car dataset, and 16 duplicates and 43 outliers were removed from the house dataset.

We then removed outliers along the Pareto front on each of the two datasets. This was done by performing a linear regression on the Pareto front and removing all alternatives whose standardized residual was greater than two. Doing so eliminated alternatives that may appear attractive only because they present an unusually good trade-off. One such outlier was removed from the car dataset, and two from the house dataset. Figure 2 shows the two datasets, their Pareto front, and the discarded outliers.

1 More information on these datasets is provided at http://www.aviz.fr/decoy We then chose two alternatives A and B on the Pareto front to act as target and competitor. The alternatives A and B were chosen so as to maximize |R A | + |R B | as defined below.

We then generated three subsets from each dataset as follows2 . Let D be the full set of alternatives (cars or houses), P its Pareto front, {A, B} the choice set, d A all alternatives dominated by A, and d B all alternatives dominated by B (see blue and red hatchings respectively in Figure 3 D ). We partitioned D in five regions:

R A = d A \ d B ; R B = d B \ d A ; R AB = d A ∩ d B ; R P = P; and R 0 = D \ (d A ∪ d B ∪ P).
We then randomly eliminated 80% of the alternatives from the sets R A , R B and R AB , and 50% of the alternatives in R 0 , yielding the subsets R - A , R - B , R - AB , and R - 0 . From this we constructed three sets of alternatives, shown in Figure 3:

D 0 = R - A ∪ R - B ∪ R - AB ∪ R - 0 ∪ R P ; D A = R A ∪ R - B ∪ R - AB ∪ R - 0 ∪ R P and D B = R - A ∪ R B ∪ R - AB ∪ R - 0 ∪ R P .
It can be seen in Figure 3 that the only difference between D 0 and D A is that D A contains more alternatives that are dominated by A but not by B. These asymmetrically dominated alternatives are analogous to decoys, while A plays the role of a target and B plays the role of a competitor. Note however that no artificial choice is added: all points belong to the original dataset, including the decoys. The roles of A and B are swapped when comparing D 0 to D B . The final stimuli can be seen in Figures 4 to 7.

Measures

As with the Bets experiment in [START_REF] Dimara | The attraction effect in information visualization[END_REF], we measure the attraction effect by the difference in the proportion of participants who chose the target in the condition with decoys vs. the condition without decoys. If p(X) S is the proportion of participants who chose X in the set of alternatives S, our data subsets allow for two possible measures of the attraction effect: E A = p(A) D Ap(A) D 0 and E B = p(B) D Bp(B) D 0 . A third aggregated measure E AB = E A + E B referred to as the combined attraction effect is possible that combines the two effects and has been used in past studies [START_REF] Wedell | Distinguishing among models of contextually induced preference reversals[END_REF]. Since E AB = p(A) D Ap(A) D B , the combined measure can be calculated without knowing the responses for D 0 . To maximize statistical power, we therefore chose to only present the decision tasks D A and D B , and use E AB as the measure of attraction effect. We report this measure for both the cars and the houses dataset.

Crowdsource Quality Control

Similar to the Gyms experiment [START_REF] Dimara | The attraction effect in information visualization[END_REF], we defined rejection criteria in advance and categorized jobs as Red (rejected) and Green (kept for analysis). There was no Orange category this time. Similar to the Gyms experiment, we made sure that participants were able to read a scatterplot. However, since our new scatterplots have many more data points, our screening test was more advanced: participants had to pick the dominant option among five options shown in red, among other unavailable options shown in gray (Figure 8). Furthermore, we measured attention with a simple catch question, by asking participants at the end of the job to recall whether the study was about houses and cars, or about other topics (e.g., cameras and cars).

A job was classified as Red if the contributor failed the scatterplot test, took an abnormal amount of time to complete the job (<1 min or >30 min), or failed the final catch question. Out of the 302 crowdsource jobs submitted with a valid completion code, 71 (24%) were categorized as Red, and 231 (76%) were classified as Green and kept for analysis.

Experiment Design

The experiment followed a mixed design. The independent between-subjects variable was the decoy position (on A or on B), while the independent within-subjects variable was the dataset (houses or cars). Each participant was presented with two decision tasks, one for each dataset. We varied the decoy position within each dataset, resulting in 2×2 = 4 different pairs of decision tasks. In addition, we counterbalanced the order of appearance of the two datasets, resulting in 8 unique sequences of tasks3 .

Figure 8: The scatterplot reading test. The answer was provided through a radio button.

As explained in subsection 2.4 our dependent variable was the combined attraction effect, i.e., the difference between the proportion of participants who chose option A when it was the target, and the proportion of participants who chose option A when the target was B. We compute and report the attraction effect for the houses dataset and for the cars dataset separately.

Participants

Our study was completed by 231 crowdflower contributors of high quality (level 3) based on their performance on the platform, and whose job was classified Green. Their demographics as reported in a post-test questionnaire is summarized in Figure 9 (middle map and stacked bar charts labeled "Real"), together with the demographics of the previous experiment "Gyms" and the next experiment "Bets" [START_REF] Dimara | The attraction effect in information visualization[END_REF]. As we can see, the demographics between the three experiments are very similar.

Bets Real Gyms

Gender Education

No schooling completed, or less than 1 year Nursery, kindergarten, and elementary (grades 1-8) Some high school, no diploma Figure 10: Proportions of participant choices in all three experiments, the experiment "Real" reported here, and "Gyms" and "Bets" reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF].

Procedure

Pre-test: As explained before and shown on Figure 8, participants were first tested on their basic ability to read a scatterplot. Participants who failed this test were removed from the analysis. Task: Participants then opened a 9-page online form which took on average 5 minutes to complete. For the house dataset, they were asked to imagine that they want to buy a house, and that all houses were similar apart from two attributes: size and price. They were then shown a scatterplot with 792 dots representing the houses in the market. Participants were told that they narrowed down their choices to two houses, shown in red. As seen before, the two red dots were labelled A and B, and all other dots where shown in gray. Participants indicated their choice using a separate radio button below the scatterplot. On the next page, they rated their confidence in their choice, justified their choice in a text area, and reported the level of their familiarity with the real estate market. After that (or before, depending on the task ordering), they had to carry out a similar task with a scatterplot displaying 356 cars according to power and efficiency. Participants could review previous pages on the form but not change their answers.

Post-task questions: Participants then had to fill a short questionnaire with their demographic information, and were given the attention test mentioned previously.

Hypothesis

Our statistical hypothesis was that the combined attraction effect will be positive for both datasets.

Results

Experimental stimuli, data and analysis scripts are available at http://www.aviz.fr/decoy.

Planned Analyses

All analyses reported here were planned before data was collected. Participant choices are shown in Figure 10, bars labeled "Real". The top two bars are the proportion of responses for the house dataset, [START_REF] Malkoc | Between a rock and a hard place: The failure of the attraction effect among unattractive alternatives[END_REF], and in all our three experiments: the experiment "Real" reported here, and "Gyms" and "Bets" reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF].

with decoys on price (A) at the top, and on size (B) at the bottom. The next two bars are the responses for the cars dataset, with decoys on efficiency (A) on the top, and power (B) on the bottom. The decoys are expected to increase the proportion of choices of the target, in the direction indicated by the arrows. As can be seen, this was not the case for either dataset, and the combined attraction effect was even negative in both cases, although small (-3% and -4%).

We now turn to inferential statistics, reported in Figure 11 for all our experiments. The two combined attraction effects mentioned previously are shown in red next to the label "Real". The two dots indicate the point estimates reported previously, and error bars are 95% confidence intervals that indicate the uncertainty around those estimates [START_REF] Cumming | Inference by eye: confidence intervals and how to read pictures of data[END_REF]. Confidence intervals were computed using score intervals for difference of proportions and independent samples. The combined attraction effect was -3%, CI [-14%, +8%] for houses, and -4% , CI [-15%, +7%] for cars.

Thus, the apparent reversal of the attraction effect observed in Figure 10 is way too unreliable for any conclusion to be drawn concerning the direction of the effect [START_REF] Cumming | Inference by eye: confidence intervals and how to read pictures of data[END_REF]. We can only be reasonably confident that the effect is no larger than 15% in either direction. If there is indeed an attraction effect, it is clearly smaller than the combined effect obtained by [START_REF] Malkoc | Between a rock and a hard place: The failure of the attraction effect among unattractive alternatives[END_REF] using the classical procedure, and likely smaller than the effect we previously obtained in our Gyms experiment. A "repulsion" effect is also possible. In summary, our results in this experiment are largely inconclusive.

Additional Analyses

As can be seen in Figure 12, participants reported similar levels of confidence in their answers across both datasets. For the houses dataset, participants reported a mean level of confidence of 6.0 on a 7-point Likert scale. For cars the mean confidence was 5.9. When it comes to familiarity, responses were diverse for both houses and cars as can be seen in Figure 12, but on average, people were similarly familiar with both datasets (both means 4.2). Figure 12: Self-reported familiarity and confidence in all three experiments: experiment "Real" reported here, and experiments "Gyms" and "Bets" reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF].

General Discussion and Conclusion

One major reason for these inconclusive results is a lack of statistical power: since the effect seems small, we would need a remarkably large sample size (i.e., much larger than N=231) or a modified design to be able to reliably assess both the direction and the magnitude of the effect.

Our inability to detect an effect at least indicates that in this experiment, the manipulation we used was not sufficient to trigger the same attraction effect as the effects typically observed in more typical experiments. Attempting to interpret this finding a-posteriori, it may be due to the choice of a constrained decision task. As explained in the background section in [START_REF] Dimara | The attraction effect in information visualization[END_REF], the attraction effect requires that participants recognize the dominance relationship between the target and the decoy. Although our participants could read scatterplots (we used a screening test) and the scatterplots we used gave them the opportunity to perceive and to recognize these dominance relationships, it is possible that the dominated alternatives (and thus the decoys) were ignored. Since these alternatives were not part of the choice set, it may have been more clear to participants that they were not needed to carry out the task. In classical attraction effect experiments it is also the case that the decoy is irrelevant to the decision task, but participants have to determine its irrelevance (i.e., perform dominance recognition) themselves. The visual design of the scatterplot (i.e., the two available options shown in red, all other options in gray) may have reinforced the impression that non-available alternatives could be entirely ignored. The disregard of decoys could have also been reinforced by the way participants gave their answers (radio buttons, one for each of the two red choices).

Given this possible interpretation as well as the low statistical power of the experiment considering the effect size investigated, it is premature to conclude that the attraction effect does not exist in scatterplots. This is particularly the case as we were able to replicate a classical attraction effect (one target, one competitor, one decoy) using scatterplots in our experiment "Gyms" [START_REF] Dimara | The attraction effect in information visualization[END_REF]. We thus decided to conduct a third experiment, reported in [START_REF] Dimara | The attraction effect in information visualization[END_REF] as experiment "Bets", where we modified the choice procedure (any alternative can be selected), the datasets (synthetically generated to maximize the effect), and the experiment design (within-subjects to maximize statistical power). We were able to find compelling evidence for an attraction effect, but more realistic datasets like the ones described here remain to be tested.

Figure 1 :

 1 Figure 1: Example of an attraction effect in elections: Bob has an excellent education plan, while Alice is very strong in crime control. The addition of Eve, a candidate similar but slightly inferior to Alice, raises Alice's attractiveness as a candidate. This irrelevant option is called a decoy. (Photos Benjamin Miller, FSP Standard License, icons by Ivan Boyco, CC-BY license)

Figure 2 :Figure 3 :

 23 Figure 2: The cars and houses datasets with their Pareto front, in blue. Crosses are discarded outliers.

Figure 4 :Figure 6 :

 46 Figure 4: Cars dataset, decoys on A Figure 5: Cars dataset, decoys on B

  High school (grades 9-12, no degree) High school graduate (or equivalent) Some college (1-4 years, no degree) Associate's degree (occupational & academic) Bachelor's degree (BA, BS, AB, etc) Master's degree (MA, MS, MENG, MSW, etc) Professional school degree (MD, DDC, JD, etc) Doctorate degree(PhD, EdD, etc)

Figure 9 :

 9 Figure9: Self-reported location, gender, age and education of the participants for all three experiments: the experiment "Real" reported here, and the experiments "Gyms" and "Bets" in[START_REF] Dimara | The attraction effect in information visualization[END_REF].

Figure 11 :

 11 Figure11: Point estimates and 95% confidence intervals for the attraction effects in Malkoc et al.[START_REF] Malkoc | Between a rock and a hard place: The failure of the attraction effect among unattractive alternatives[END_REF], and in all our three experiments: the experiment "Real" reported here, and "Gyms" and "Bets" reported in[START_REF] Dimara | The attraction effect in information visualization[END_REF].

  Terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Stimuli and Task . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Scenario and Attribute Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3.1 Dataset Selection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3.2 Dataset Preparation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.5 Crowdsource Quality Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Experiment Design 7 3.1 Participants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.3 Hypothesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4 Results 9 4.1 Planned Analyses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 Additional Analyses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

  Test de l'effet d'attraction sur deux jeux de données de visualisation d'information Résumé : L'effet d'attraction est un biais cognitif souvent étudié dans la recherche en prise de décision, et selon lequel un choix entre deux options est influencé par la présence d'une troisième option non pertinente (dominée). Dans un autre article, nous décrivons deux expériences qui montrent que l'effet d'attraction se généralise aux visualisations. Cependant, nous avons aussi conduit une autre expérience où nous n'avons pas pu observer d'effet. Cette expérience a employé des nuages de points générés à partir de jeux de données réelles, et a restreint les choix à exactement deux options. Nous décrivons ici cette expérience et discutons les raisons possibles de ce résultat négatif. Mots-clés : Résultat négatif, visualisation d'information, prise de décision, effet d'attraction, effet de leurre, effet de domination asymétrique, biais cognitif

	Bob	Alice	Eve
	Education
	Crime control

Table Table TableTable Table Table

 TableTable

						Simple attraction effect
		Format	Scenario	Decoy position		Combined effect
	Malkoc 2013		Gyms Gyms Gyms	Cleanliness Variety Combined	No effect
			Gyms	Cleanliness
			Gyms	Variety
	Gyms	Plot	Gyms Gyms	Combined Cleanliness
		Plot	Gyms	Variety
		Plot	Gyms	Combined
	Real	Plot Plot	Houses Cars	Combined Combined
	Bets	Plot	Bets	Combined
				-20%	0%	20%	40%	60%

RR n°8895

The construction described here is slightly different than that of[START_REF] Dimara | The attraction effect in information visualization[END_REF], but the resulting regions are equivalent.Inria

houses A -cars A , houses A -cars B , houses B -cars A , houses B -cars B , cars A -houses A , cars A -houses B , cars B -houses A , cars B -houses B . RR n°8895


Pierre Dragicevic

My Technique is 20% Faster: Problems with Reports of Speed Improvements in HCI

In human-computer interaction (HCI), speed improvements are often used as an informal measure of effect size, with statements such as "technique A was about 20% faster than technique B". Such statements are however surrounded by confusion. A quick analysis of the literature reveals that half of the time, the term "% faster" actually refers to a percent change in task completion time, while one third of the time it correctly refers to a percent change in speed. The rest of the time, the meaning is unknown or the calculation is wrong. We explain why percent changes are inherently confusing, and propose to focus effect size discussions on ratios, or on measures of percent difference where the normalizer is the mean of the compared values. When percent changes need to be reported, it is suggested to focus the discussion on improvements in task completion times rather than speed.

I. INTRODUCTION

. What is ultimately of interest to HCI researchers is often how interaction techniques differ in their performance, e.g., their differences in average error rates or task completion times.

Many authors use percent changes in speed as an informal measure of effect size, using statements such as "our results show that technique A was 20% faster than technique B". However, such statements are confusing and should preferably be avoided for two reasons: first, percent changes are counter-intuitive. Second, percent changes in speed are often conflated with percent changes in time, leading to inconsistent and ambiguous reports.

II.

A percent change (or percentage change) is the ratio between a change in a quantity and the quantity's initial value, expressed as a percentage. That is, if the value of a quantity (e.g., the price of an item) changes from v 1 to v 2 , then its percent change is:

p = 100 × v 2 -v 1 v 1 (1)
v 2 and v 1 do not necessarily have to reflect actual changes over time and can be, e.g., the prices of an item in two different stores. Either way, one computes p and if p is found to be positive, then one can say that "v has increased by p%" or that "v 2 is p% more than v 1 ". If p turns out negative, then one would say that "v has decreased by (-p)%" or that "v 2 is (-p)% less than v 1 ".

Compared to an absolute change v 2 -v 1 , a percent change has the advantage of being unitless. Percent changes are widely used in disciplines such as medicine [START_REF] Zhang | How to Analyze Change from Baseline: Absolute or Percentage Change? D-level Essay in Statistics[END_REF] and economics [START_REF] Tornqvist | How Should Relative Changes Be Measured[END_REF]. But one difficulty with percent changes lies in their asymmetry, leading to oddities. For example, saying that A is 25% more expensive than B is equivalent to saying that B costs 20% less than A.

The term v 1 in Equation 1 is called the baseline [START_REF] Zhang | How to Analyze Change from Baseline: Absolute or Percentage Change? D-level Essay in Statistics[END_REF], or alternatively, the base [START_REF] Huff | How to lie with statistics[END_REF] or the reference value [START_REF] Gluck | Uses and Abuses of Percentages[END_REF]. Choosing the other value as the baseline, i.e, swapping v 1 and v 2 , can dramatically change the value of p. Although the choice of a baseline is obvious when measurements have been taken at different points in time -as it is typically the case in medicine or economics -it is less so when measurements have been taken in no particular order -as it is typically the case in HCI.

Baselines are so confusing that they have been often used as a means of abusing and misleading people [5, pp. 109-112]. Although HCI articles always use phrasings that clearly specify which is the baseline, the legitimacy of chosen baselines remains dubious. The convention in HCI is to report improvements of "newer" over "older" techniques. But the limits of this convention become apparent when two novel designs or two old designs need to be compared. In medicine, we want to know if a patient got better after a treatment, and reporting percent changes is sensible. But in HCI, we simply want to compare techniques with each other, and the notion of baseline is most often artificial and unnecessary.

Aside from baseline issues, a drawback of percent changes is that they are not the most intuitive measure of difference one can think of. Suppose you are proposed a special fare for a hotel room and can pay $100 instead of $300. Will you think of it as a 67% discount? More likely, you will consider that you will pay only 1/3 of the price (a ratio), or possibly that you will save $200 (an absolute difference). Or take any bar chart and try to estimate percent changes. This is hard because percent changes do not directly map to the way we naturally think of differences and proportions. Knowing this, it is hard to understand why they are so popular.

But why not take percent differences in speed for what they are, i.e, rough estimates of how impressive new techniques are? Cannot we adopt them as a convenient HCI standard and agree on the meaning of percentages, e.g., "50% faster" than the best technique would be revolutionary whereas "5% faster" would too incremental for publication? Unfortunately not, as we will now see.

III. CHANGES IN SPEED VS. TIME

The most serious issue with percent changes in speed is the easy confusion between speed and time. If technique A takes on average 20% less time than technique B, it does not follow that technique A is 20% faster than technique B. Speed is a different measure from time. Suppose we are not comparing techniques but cars. We have different pilots drive car A and car B on a 10-km circuit (the task ), and we measure how long they take to cover this distance (task completion time). We find that on average, it takes them 125 seconds with car A, but 200 seconds with car B. If we take B as the baseline, the percent change is p = 100 × (125 -200)/200 = -37.5%, meaning A takes on average 37.5% less time than B to cover this distance (to complete this task).

But how do the cars differ in speed? The average speed of car A is the distance it covered divided by the time it took on average, or 10/125 = 0.08 km/s (or 288 km/h), whereas the average speed of car B is 10/200 = 0.05 km/s (or 180 km/h). The speed improvement of A over B is therefore p = 100 × (0.08 -0.05)/0.05 = 60%. So car A takes 37.5% less time than car B to cover the same distance, but it is 60% faster than car B.

There is no reason why techniques in user studies should be treated differently: speed always refers to a quantity of something per unit of time. The purpose of a car is to cover distances, the purpose of a technique is to carry out tasks. Therefore, the speed of a technique should refer to a number of tasks (or pieces of task) carried out per unit of time. Actually, it can be verified that the choice of units does not affect p. For cars it could be kilometers per hour, meters per minutes, mph, etc. In particular, one can take the inverse of travel times and ignore distances: p = 100 × (1/125 -1/200)/(1/200) = 60%. The general formula is:

p speed = 100 × 1/t 2 -1/t 1 1/t 1 (2)
Or after simplification:

p speed = 100 × t 1 -t 2 t 2 (3)
Equation 3 can also be used to compute the percent change in speed of interaction techniques, t 1 being the average task completion time for the baseline technique, and t 2 the average task completion time for the new technique. One could think of it as applying Equation 1 to the average number of tasks carried out per unit of time, but the actual units do not matter for computing p. Now compare this with the original formula for computing the percent change in task completion time:

p time = 100 × t 2 -t 1 t 1 (4)
We can see that Equation 3is the same as what we would have obtained by swapping t 1 and t 2 in Equation 4, i.e., by switching the baseline. To summarize:

• Saying that A takes x% less time than B is not the same as saying that A is x% faster than B.

• Saying that B takes x% more time than A is the same as saying that A is x% faster than B.

• Saying that A takes y% less time than B is the same as saying that B is y% slower than A.

The following article excerpt shows how the equivalence between "% more time" and "% faster" can be exploited in a discussion:

"Results show that the selected visual augmentation caused users to believe it had a duration equal to that of a progress bar 11% longer in actual time. In other words, visually augmented progress bars could be used to make processes appear 11% faster, when in reality, their duration remains unchanged." [4, p. 4] So where is the problem with percent changes in speed? Can't we all simply follow those mathematical definitions? Again, the real problem is that these measures are counter-intuitive. The math may be correct, it remains difficult for readers to quickly grasp the meaning of statements like "A takes 10% less time than B" or "B is 10% slower than A", and figure out whether there is a difference between them. Not only readers are confused but also a number of authors, as we will now see.

IV. LITERATURE ANALYSIS

We searched the term "% faster" in 10 conference proceedings: the last three proceedings of the SIGCHI conference on Human Factors in Computing Systems (CHI' 09-11), the last five proceedings of the IEEE Symposium on Information Visualization (InfoVis' 07-11), and the last two proceedings of the ACM Symposium on User Interface Software and Technology (UIST' 10-11).

The term appeared 89 times in 43 different papers. We used the reported descriptive statistics to determine what the term was referring to. Among all 89 occurrences:

• ≈50% of the time (n=43), the term "% faster" referred to a percent change in task completion time, i.e., Equation 4 was used instead of Equation 3.

• ≈30% of the time (n=28), the term correctly referred to a percent change in speed:

-≈20% of the time (n=19), the measures of interest were task completion times, and Equation 3 was used to obtain the corresponding percent change in speed. -≈10% of the time (n=9), the measures of interest were speeds (e.g., words per minute), and the percent change was directly obtained from Equation 1.

• ≈20% of the time (n=18), the meaning was undetermined:

-≈15% of the time (n=15), the values from which the percent change was computed were not reported, in either numerical or graphical form. -≈5% of the time (n=3), the percent changes were wrong, i.e., their numerical value did not match the result of any formula.

This quick analysis reveals the confusion that surrounds the term "% faster" in HCI, except in rare cases where the dependent variable is already a speed (e.g., words per minute). A reader can easily resolve ambiguities when the values t 1 and t 2 are provided in the same sentence or in a table nearby. However, percent changes in speed are often used to feed discussions that are remote from the descriptive statistics, including in introductions, conclusions and abstracts.

The values t 1 and t 2 are sometimes provided in graphical form only, e.g., bar charts. Although it was tedious to extract numerical values from these charts in the context of this survey, in practice charts are enough for the reader to get a clear idea of effect sizes and whenever they are provided, percent changes can be safely ignored.

Ambiguities surrounding percent changes are especially problematic when the values from which they are computed are not provided in any form (15% of the time). This includes expeditious statistics reports (especially in short papers), citations of results from previous work, and percent changes reflecting comparisons with previous work. This suggests that percent changes in speed are believed to be adequate for quickly summarizing results, but our analysis provides clear evidence to the contrary.

We know turn to two alternatives: ratios and symmetric measures of percent differences.

V. RATIOS

Physical measurements with a true zero point such as distances and times are sometimes called ratio scales. A natural way of comparing several such measurements is by thinking in terms of ratios. In the previous example, the time it took for car A to cover the circuit length was 125/200 = 0.625 times the time it took for car B. So one could say that on average, it took for car A less than 2/3 of the time it took for car B. It is easy to build a mental picture of the corresponding bar chart.

Ratios are asymmetric but switching baselines only requires taking the inverse of the ratio. For example, saying that "it took car A less than 2/3 of the time it took car B" is the same as saying that "it took car B more than 3/2 of the time it took car A". Time ratios and speed ratios are also related by an inverse relationship. For example the two previous statements are equivalent to "the speed of car A was more than 3/2 the speed of car B".

One may want to multiply these ratios by 100 to turn them into percentages and say, e.g., "the speed of car A was 160% the speed of car B", or "the speed of car B was 62.5% the speed of car A". But these percentages run the risk of being confused with percent changes. Percent changes are easy to spot because they are followed by comparatives (e.g., "% faster") or trend nouns (e.g., "% increase"). To minimize the risk of confusion, these should be avoided when reporting percent ratios.

Equations 1-4 can be rewritten so that only ratios appear, so it is possible to convert between ratios and percent changes without knowing v 1 and v 2 (below, replace a and b with "the time for A/B" or "the speed of A/B"):

• Saying that a is x% higher than b is the same as saying that a is (x + 100)% of b.

• Saying that a is x% lower than b is the same as saying that a is (100 -x)% of b.

• Saying that a is x% of b if x ≥ 100 is the same as saying that a is (x -100)% higher than b.

• Saying that a is x% of b if x ≤ 100 is the same as saying that a is (100 -x)% lower than b.

Note that these conversions are simple mathematically but not necessarily cognitively, so focusing a discussion on ratios will be easier for readers than if all percent changes need to be mentally converted to ratios. Unfortunately, apart from special cases (e.g., when a technique can be said to be "twice as fast"), reporting ratios requires phrasings that are generally longer and maybe more awkward than reporting percent changes. It seems that simple concepts do not always map to simple language, while confusing concepts sometimes do.

VI. PERCENT DIFFERENCES

When discussing differences, one may prefer a measure of effect size that really captures a difference, i.e, that is equal to zero when the two values are equal. This can be achieved using percent differences. Several formulas exist for computing percent differences [START_REF] Tornqvist | How Should Relative Changes Be Measured[END_REF]. One of them -and perhaps the worst -is Equation 1. In fact, when v 1 and v 2 have no clear chronological order, "percent difference" is a more appropriate term for p than "percent change", but we chose to stick to the latter to avoid ambiguities, since there are many ways of computing percent differences.

In physics measurements [START_REF] Wenning | Percent Difference -Percent Error[END_REF], a percent difference generally refers to the following measure, which uses the mean value as the normalizer instead of the initial value:

p = 100 × v 2 -v 1 1 2 (v 1 + v 2 ) (5)
This measure has the advantage of being symmetric. If we take car B as the baseline, then p = 100 × (125 -200)/ 1 2 (125 + 200) = -46.2%. If we take car A as the baseline instead, then p = 46.2%. Switching baselines only changes the sign of p, so it is sufficient to report the direction of the effect and its size |p|, without having to specify a baseline. For example, one could say that "car A was faster than car B, with a difference of 46.2%". Now if we consider car speeds instead of travel times and keep car B as the baseline, we get a percent difference of p = 100 × (10/125 -10/200)/ 1 2 (10/125 + 10/200) = 46.2%. It can be verified that replacing times with speeds has the same effect as switching baselines: it only changes the sign of p. Therefore, when we reported a 46.2% difference between the cars, we did not need to specify whether we were talking about travel times or speeds.

Here are two imaginary examples of use in HCI: Example 1. "Technique A was found to be faster than technique B overall, but there was a clear interaction with target size. For large targets (W = 40 mm), the percent difference was only 2.5%, while it was as much as 50% for small targets (W = 1 mm)."

Example 2. "The superiority of technique A over technique B was consistent with previous studies but we found a larger difference. Table 1 summarizes results from previous studies. The largest previously reported difference was 11% (Smith et al.), while ours was as much as 33%."

Since several formulas are possible for computing percent differences (including using the max of v 1 and v 2 as the normalizer, the min, the geometric means, etc. [START_REF] Tornqvist | How Should Relative Changes Be Measured[END_REF]), it is necessary to specify the formula used, for example in a footnote: "all percent differences were computed using p = 100(v 2 -v 1 )/ 1 2 (v 1 + v 2 ) in order to get symmetric measures of relative differences".

Arguably, the ambiguity surrounding the term percent difference is a drawback of this approach. Also, as with percent changes, it is difficult to mentally switch between percent differences and simple graphical representations such as bar charts. However, the symmetric nature of Equation 5 makes it a more elegant, more convenient and less confusing measure than percent change.

VII. CONCLUSION

Although speed improvements are a common measure of effect size in HCI, they confuse readers and authors alike. The term "% faster" most often refers to a percent change in task completion time, and sometimes it correctly refers to a percent change in speed. Related terms such as "% slower" likely suffer from the same problems.

Confusions stem from the counter-intuitive nature of percent changes, with odd behaviors when switching baselines and switching between times and speeds. This suggests that percent changes should be best avoided. They may be useful in economics or medicine where measurements are ordered, but most user studies in HCI involve comparing techniques independently from any notion of chronology, so percent changes are not needed.

There is still a need for reporting effect sizes in a compact numerical format, in order to assess how "impressive" new results are or for discussing previous work. We suggest to use ratios as an alternative. The concept of ratio is easy to grasp, directly maps to graphical representations, and one only needs to take the inverse of a ratio for switching baselines or for switching between times and speeds. We also propose to adopt the measure of percent difference used in physics, where the normalizer is the mean between the two compared values. This measure only requires changing sign for switching baselines or for switching between times and speeds.

Other measures of effect size exist, among which are standardized effect sizes such as Cohen's d that normalize absolute differences based on data distributions [START_REF] Fritz | Effect size estimates: Current use, calculations, and interpretation[END_REF]. These are useful for capturing the variability across subjects or when the units of measurement are not meaningful to readers [START_REF] Wilkinson | Statistical methods in psychology journals: Guidelines and explanations[END_REF]. But for discussing familiar units, non-standardized measures (such as time or speed ratios and percent differences) are easier to understand [START_REF] Wilkinson | Statistical methods in psychology journals: Guidelines and explanations[END_REF].

When percent changes need to be reported and the dependent variables are task completion times, it is advised to either i) focus on improvements in task completion times and avoid terms such as "% faster" or "% slower", or ii) clearly specify what is meant by these terms.


Martin Clochard

Léon Gondelman

Mário Pereira

The Matrix Reproved ‹ (Verification Pearl)

In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and the Strassen's algorithm. The proofs are conducted using the Why3 platform for deductive program verification, and automated theorem provers to discharge proof obligations. In order to specify and prove the two multiplication algorithms, we develop a new Why3 theory of matrices and apply the proof by reflection methodology.

Introduction

In this paper we describe a complete solution for the first challenge of the Veri-fyThis 2016 competition using the Why3 platform for deductive verification.

As it was asked in the original challenge, we prove the correctness of two different implementations of matrix multiplication. First, we specify and prove a naive algorithm which runs in cubic time; then the more efficient Strassen's algorithm. To our knowledge, this is the first proof of Strassen's algorithm for square matrices of arbitrary size in a program verification environment based on automated theorem provers.

Wishing to make our solutions both concise and generic, we devised in Why3 an axiomatic theory for matrices and showed various algebraic properties for their arithmetic operations, in particular multiplication distributivity over addition and associativity (which was asked in the challenge second task). Our full development is available online 3 .

It turns out that proving Strassen's algorithm was virtually impossible for automated theorem provers due to their incapacity to perform reasoning on algebraic matrix equations. To overcome this obstacle, we devise an algebraic expression simplifier in order to conduct proof by reflection. This paper is organized as follows. The Section 2 presents briefly Why3. The Section 3 describes our solution for naive matrix multiplication. Then, the Section 4 presents our solution for the second task and for that purpose introduces our axiomatic matrix theory. We specify and prove Strassen's algorithm in Sections 5 and 6. We discuss related work in Section 7.

Why3 in a Nutshell

The Why3 platform proposes a set of tools allowing the user to implement, formally specify, and prove programs. It comes with a programming language, WhyML [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF], an ML dialect with some restrictions in order to get simpler proof obligations. This language offers some features commonly found in functional languages, like pattern-matching, algebraic types and polymorphism, but also imperative constructions, like records with mutable fields and exceptions. Programs written in WhyML can be annotated with contracts, that is, pre-and postconditions. The code itself can be annotated, for instance, to express loop invariants or to justify termination of loops and recursive functions. It is also possible to add intermediate assertions in the code to ease automatic proofs. The WhyML language features ghost code [START_REF] Filliâtre | The spirit of ghost code[END_REF], which is used only for specification and proof purposes and can be removed with no observable modification in the program's execution. The system uses the annotations to generate proof obligations thanks to a weakest precondition calculus.

Why3 uses external provers to discharge proof obligations, either automatic theorem provers (ATP) or interactive proof assistants such as Coq, Isabelle, and PVS. The system also allows the user to manually apply transformations to proof obligations before they are sent to provers, in order to make proofs easier.

The logic used to write formal specifications is an extension of first-order logic with rank-1 polymorphic types, algebraic types, (co-)inductive predicates and recursive definitions [START_REF] Filliâtre | One logic to use them all[END_REF], as well as a limited form of higher-order logic [START_REF] Clochard | Formalizing semantics with an automatic program verifier[END_REF]. This logic is used to write theories for the purpose of modeling the behavior of programs. The Why3 standard library is formed of many such logic theories, in particular for integer and floating point arithmetic, sets, and sequences.

The entire standard library, numerous verified examples, as well as a more detailed presentation of Why3 and WhyML are available on the project web site, http://why3.lri.fr.

Naive Matrix Multiplication

The VerifyThis 2016 first challenge starts with a proposal to verify a naive implementation of the multiplication of two matrices using three nested loops, though in non-standard order. In this section we present our solution to this part of the challenge.

We first write the WhyML equivalent of the challenge code for multiplication of two matrices a and b: let mult_naive (a b: matrix int) : matrix int = let rs = make (rows a) (columns b) 0 in for i = 0 to rows a -1 do for k = 0 to rows b -1 do for j = 0 to columns b -1 do set rs i j (get rs i j + get a i k * get b k j) done; done; done; rs To encode matrices, we use two-dimensional arrays as provided in the Why3 standard library. Operations get and set have the usual semantics, and make carries out creation and initialization. Such arrays are represented by the following abstract type, whose fields can only be accessed in specifications. In order to define this predicate concisely we use higher-order features and the sum function from Why3 standard library. This function returns the sum of f n for n ranging between a and b, as defined by the following axioms: The last argument we give to sum is a first-class function λk.M . Why3 supports such definitions by translating them to first-order values [START_REF] Clochard | Formalizing semantics with an automatic program verifier[END_REF].

To prove that mult_naive meets its specification, we give suitable loop invariants. There are two kinds of invariant per loop. The first one is the frame invariant, which describes the part of the matrix that is left unchanged. The second one describes the contents of cells affected by the loop. Let us illustrate this with the inner loop. In that case, the loop has the effect of writing a partial sum into cells 0 to j-1 of the i-th row, leaving other cells unchanged.

'I: for j = 0 to columns b -1 do invariant { forall i0 j0. 0 ď i0 ă rows a ^0 ď j0 ă columns b Ñ (i0 ‰ i _ j0 ě j) Ñ rs.elts[i0][j0] = (at rs 'I).elts[i0][j0] } invariant { forall j0. 0 ď j0 ă j Ñ rs.elts[i][j0] = sum 0 (k+1) (mul_atom a b i j0) }
With the given specification all the generated verification conditions are discharged in a fraction of second using the Alt-Ergo SMT solver.

From Multiplication Associativity to a Matrix Theory

The next task was to show that matrix multiplication is associative. More precisely, participants were asked to write a program that performs the two different computations pABqC and ApBCq, and then prove the corresponding results are always the same. In our case, this corresponds to prove the following:

forall i j. 0 ď i ă ab_c.rows ^0 ď j ă ab_c.columns Ñ ab_c.elts[i][j] = a_bc.elts[i][j] }
As one can guess, the proof of associativity relies essentially on the linearity properties of the sum operator and Fubini's principle. Let us illustrate how we establish the additivity of the sum (the homogeneity of the sum and Fubini's principle are done in a similar way). First we define a higher-order function addf which, given two integer functions f and g, returns a function \x. f x + g x. Then, we state the additivity as a lemma function: The fact that we write the lemma not as a logical statement but as a recursive function allows us to do two important things. First, we simulate the induction hypothesis via a recursive call, which is useful since the ATPs usually do not support reasoning by induction. Second, writing a lemma as a program function allows us to call it with convenient arguments later, which amounts to giving instances. Notice that the lemma is given an explicit variant clause. Indeed, when one writes a lemma function, Why3 verifies that it is effect-free and terminating. Now, a possible way to complete the second task would be to show the associativity directly for the multiplication implemented by the naive algorithm from task one. However, such a solution would be ad hoc: each time we implement the matrix multiplication differently, the associativity must be reproved.

To make our solution more general, we opt for a different solution which consists roughly of two steps. First, we provide an axiomatized theory of matrices where we prove that matrix product, as a mathematical operation, is associative. Second, we create a model function from program matrices to their logical representation in our theory. Finally, we show that from the model perspective naive multiplication implements the mathematical product. When all this is done, we have the associativity of naive multiplication for free.

We split our matrix axiomatization in two modules. The first module introduces a new abstract type and declares the following functions and adds a set of axioms that describes their behavior. We add the create function to build new matrices by comprehension. Additionally, we have an extensionality axiom, i.e. that for any pair of matrices m1, m2, we have m1 == m2 Ñ m1 = m2 where m1 == m2 means that both matrices have the same dimensions and the content of their cells are the same.

The second module defines arithmetic operations over integer matrices as straightforward instances of create, and exports various proved lemmas about their algebraic properties, including associativity and distributivity. Although we are looking for associativity, the other properties are expected in such a theory, and we will use some of them in later sections. A typical proof amounts to writing the following: The by connective in the last line instruments the lemma with a logical cut for its proof, to show the desired instance of extensionality. It follows by the auxiliary lemma function mul_assoc_get, whose proof is omitted here.

Once we formalized the matrix theory and proved associativity, it remains to connect it to the implementation by a model function:

Strassen's Algorithm in Why3

The last (and optional) part in the VerifyThis challenge was to verify Strassen's algorithm for power-of-two square matrices. We prove a more general implementation that uses a padding scheme to handle square matrices of any size.

Implementation

The principle behind Strassen's Algorithm is to use 2ˆ2 block multiplication recursively, using a scheme that uses 7 sub-multiplications instead of 8. More precisely, it works in 3 phases. It first partitions both input matrices in 4 equalsized square matrices. Then, it computes 7 products of matrices obtained by additions and subtractions. Finally, it obtains a similar partition of the result using addition and subtractions from those products. The details can be found in appendix B.

For even sizes, our implementation closely follows Strassen's recursive scheme. To this end, we first implement and prove a few simple matrix routines:

-Matrix addition (add) and subtraction (sub); -Matrix block-to-block copy (blit); -Sub-matrix extraction (block).

For odd sizes, the recursive scheme cannot be applied. This is typically solved by peeling or zero-padding, either statically or dynamically to recover an even size. We use a dynamic padding solution. In case the matrices have odd size, we add a zero row and column to recover an even size, make a recursive call and extract the relevant sub-matrices.

When the size gets below an arbitrary cutoff we use naive matrix multiplication. Although we used a concrete value, the code is correct for any positive cutoff. We ensure this by wrapping the cutoff value under an abstract block, which hides its precise value in verification conditions.

Specification and Proof

Except for the additional requirements that the matrices are square, we give the same specification for Strassen's algorithm as for naive multiplication.

As for the proof, let us first focus on the correctness of Strassen's recursive scheme. We break down that proof in two parts. First, we prove that the usual 2ˆ2 block decomposition of matrix product is correct. Then, we prove that the efficient computation scheme that uses seven multiplication indeed computes that block decomposition. That second part boils down to checking four ring equations, which we will cover in details in Section 6.

In order to prove block decomposition, we introduce a dedicated module where sub-matrix extraction is defined by comprehension. It extracts a rectangle from a matrix, given the low corner at coordinates r, c and with dimensions dr, dc: The module essentially proves two lemmas about relations between submatrix extraction and product, which are best seen graphically as in Figure 1. One expresses sub-matrices of the product as products of sub-matrices, while the other decomposes products into sums of sub-matrices products. We then expect to obtain the desired block decomposition by two successive partitioning steps, but there is a catch. Our implementation extracts directly the 4 input sub-matrices, while using those lemmas implies extracting from intermediate sub-matrices. We bridge the gap by reducing successive sub-matrix extraction to single ones. In practice, we do this by proving and then calling a lemma function with the following postcondition:

ensures { block (block a.mdl r1 dr1 c1 dc1) r2 dr2 c2 dc2 = block a.mdl (r1+r2) dr2 (c1+c2) dc2 }
This is sufficient to prove the algebraic relations between the partition of the product and the partitions of the input matrices. Also, note that we can readily reuse the same proof scheme for padding correctness. Indeed, it amounts to checking that the block we extract from the product of padded matrices is the right one. This follows immediately from the relevant block decomposition of the matrix product. Finally, there is only one non-trivial remaining part: termination. It is nontrivial because our padding scheme increases the matrix size. This does not cause any problem, because the next step will halve it. We prove termination by introducing an extra ghost argument identifying matrices that will not require padding: All generated VCs for the described specification are automatically discharged using a combination of Alt-Ergo, CVC4, and Z3 SMT solvers.

Proving Validity of Ring Equations by Reflection

Once we got rid of block matrix multiplication, proving validity of algebraic equations was the major difficulty. Indeed, Strassen's algorithm relies on equations like

A 1,1 B 1,2 `A1,2 B 2,2 " A 1,1 pB 1,2 ´B2,2 q `pA 1,1 `A1,2 qB 2,2
which is obvious for humans, but turns out to be quite a trouble for ATPs.

A possible explanation is that ATPs are not directly aware that fixed-size square matrices form a ring, struggling to instantiate relevant lemmas correctly. Moreover, the dimension constraints from those lemmas must be proved at each application, which makes the situation even worse.

One possible solution would be to add assertions about intermediate equations inside the code until they are easy enough to be exploitable by ATPs to bridge the gap. However, after trying to go this way, we found that even for the equality above (the easiest one), the gap was too large for ATPs which were still spending too much time to discharge the proof obligations.

Without support of automated provers, making use of an interactive one (typically Coq) would be a standard choice. If the interactive prover has support for proving ring equations, then it would suffice to embed our matrix theory inside the prover's ring structure. However, we were curious to see if we could embed some kind of similar ring support inside Why3 itself. That leads us to the technique known as proof by reflection. The methodology we follow is actually very similar to the one presented in [1, chapter 16].

To carry out proof by reflection of algebraic equations, we have to do two things. First, we have to reflect (translate) the original expressions on each side by equivalent syntactical forms. Second, we need a procedure that normalizes a syntactical form so that the comparison of algebraic expressions becomes trivial. This can be implemented in Why3 logic, and run using the compute specified transformation. This transformation normalizes a given goal, making boolean and integer arithmetic simplifications, and applying user-defined rewrite rules (in the source code one can add declarations to configure the transformation). To complete the proof, we need a lemma saying that the normalization procedure preserves the interpretation of the syntactic form. Let us now describe how we carry out these two phases in more detail.

Reflecting Algebraic Expressions by Ghost Tagging

Essentially, the reflection phase amounts to building an equivalent syntactic form for each algebraic expression. In our case, we achieve that by tagging each matrix with a ghost symbolic expression: Notice that the representation predicate above is parametrized by an environment, which binds expression variables to matrices. Also, as field sym is ghost, it will not incur any extra runtime cost. It remains then to provide, for each arithmetic operation, a tagging combinator that wraps in parallel the corresponding matrix computations and symbolic executions on their reflection. For instance, the combinator for addition is defined by:

Normalizing Algebraic Expressions

In practice, we choose not to reflect completely algebraic expressions as syntactic objects. Instead, we implement in Why3 logic smart constructors that maintain normal forms, and reflect algebraic expressions as a computation tree made of those constructors. This has the advantage that we can use the ghost tagging mechanism to instantiate correctness lemmas as well. Also, this reduces the proof work to first write an assertion like assert { e_mdl e m11.sym = e_mdl e egm11 } then to apply the transformation on the associated goal. This completely reduces both computation trees and interprets back the results as standard expressions. Since they are in normal form, the equation becomes trivial and is reduced to true by the transformation directly.

The normal form we choose for algebraic expressions is a sorted sequence of signed variable products (monomials), interpreted as the sum of those monomials. We represent them using Why3 algebraic datatype of lists, and integers for variables. To correlate variables with effective matrices, we use a simple environment composed of a mapping and a symbol generator.

type mono = { m_prod : list int; m_pos : bool } type expr = { e_body : list mono; e_rows : int; e_cols : int } type env = { mutable ev_f : int Ñ mat int; mutable ev_c : int }

The smart constructor implementations are fairly straightforward. For instance, addition is done by merging sorted lists followed by collapsing opposite terms. Multiplication is reduced to addition by distributing. We carried out smart constructors correctness proof by writing ghost procedures that mimic the control structure of the logical functions. Those procedures are then called in the ghost tagging combinators.

Note that we only prove that the simplifications are correct, not that we indeed compute normal forms. Although it may be desirable, it is not necessary if our goal is to prove algebraic equations. We only need both sides to be reduced to the same term. This also makes the aforementioned correctness proofs very easy, as the simplifications we carry out mirror the lemmas of our matrix theory.

All generated proof obligations for the correctness of smart constructors are automatically discharged using a combination of Alt-Ergo and CVC4 SMT solvers. The algebraic equations involved in Strassen's algorithm are directly eliminated by compute specified.

Related Work

There are other works in the literature that tackle the proof of matrix multiplication algorithm similar to Strassen's. The closest to our work is that of Dénès et al. [START_REF] Dénès | A refinement-based approach to computational algebra in Coq[END_REF]. They propose a refinement-based mechanism to specify and prove efficient algebraic algorithms in the Coq proof assistant. The authors report on the use of Coq's ring tactic to ease the proof of Winograd's algorithm (a variant of Strassen's with fewer additions and subtractions), a similar approach to our proof by reflection. To cope with the case of odd-sized matrices they implemented dynamic peeling to remove extra rows or columns.

Another work is the proof of Strassen's algorithm in the ACL2 system [START_REF] Palomo-Lozano | Certification of matrix multiplication algorithms. Strassen's algorithm in ACL2[END_REF]. The use of ACL2 with suitable rewriting rules and proper ring structure allows a high degree of automation in the proof process. However, they use an ad hoc definition of matrices whose sizes can only be powers of 2.

Srivastava et al. propose a technique for the synthesis of imperative programs [START_REF] Srivastava | From program verification to program synthesis[END_REF] where synthesis is regarded as a verification problem. Verification tools are then used with a two-folded purpose: to synthesize programs and their correctness proof. One case-study presented for this technique is Strassen's algorithm for 2ˆ2 integer matrices, for which the authors have been able to synthesize the additions and subtractions operations over block matrices.

Conclusion

We presented our solution for the first challenge of the VerifyThis 2016 competition. While presenting our solutions in detail, we took the opportunity to illustrate some interesting features of Why3, among which are higher-order functions in logic, lemma functions, ghost code, and proof obligation transformations. It would be interesting to see whether the proof by reflection methodology we use in this work can be helpful for verification of some other case studies, especially in a context which favours ATPs.

  type matrix 'a model { rows: int; columns: int; mutable elts: map int (map int 'a) } Let us now specify the multiplication procedure let mult_naive (a b: matrix int) : matrix int requires { a.columns = b.rows } ensures { result.rows = a.rows ^result.columns = b.columns } ensures { matrix_product result a b } The matrix_product predicate mimicks the mathematical definition of matrix product pABq ij " ř m´1 k"0 A ik B kj : function mul_atom (a b: matrix int) (i j: int) : int Ñ int = \k. a.elts[i][k] * b.elts[k][j] predicate matrix_product (m a b: matrix int) = forall i j. 0 ď i ă m.rows Ñ 0 ď j ă m.columns Ñ m.elts[i][j] = sum 0 a.columns (mul_atom a b i j)

  function sum (a b: int) (f: int Ñ int) : int axiom sum_def1: forall f a b. b ď a Ñ sum a b f = 0 axiom sum_def2: forall f a b. a ă b Ñ sum a b f = sum a (b -1) f + f (b -1)

  let assoc_proof (a b c: matrix int) : unit requires { a.columns = b.rows ^b.columns = c.rows } = let ab_c = mult_naive (mult_naive a b) c in let a_bc = mult_naive a (mult_naive b c) in assert { ab_c.rows = a_bc.rows ^ab_c.columns = a_bc.columns

  let rec lemma additivity (a b: int) (f g: int Ñ int) : unit ensures { sum a b (addf f g) = sum a b f + sum a b g } variant { b -a } = if b ą a then additivity a (b-1) f g

  type mat 'a function rows (mat 'a) : int function cols (mat 'a) : int function get (mat 'a) int int : 'a function set (mat 'a) int int 'a : mat 'a function create (r c: int) (f: int Ñ int Ñ 'a) : mat 'a

  function mul_atom (a b: mat int) (i j:int) : int Ñ int = \k. get a i k * get b k j function mul (a b: mat int) : mat int = create (rows a) (cols b) (\i j. sum 0 (cols a) (mul_atom a b i j)) let lemma mul_assoc_get (a b c: mat int) (i j: int) requires { cols a = rows b ^cols b = rows c } requires { 0 ď i ă rows a ^0 ď j ă cols c } ensures { get (mul (mul a b) c) i j = get (mul a (mul b c)) i j } = ... lemma mul_assoc: forall a b c. cols a = rows b Ñ cols b = rows c Ñ mul a (mul b c) = mul (mul a b) c by mul a (mul b c) == mul (mul a b) c

  function mdl (m: matrix 'a) : mat 'a = create m.rows m.columns (get m) Then, we change the specification of mult_naive to use the model. This turns the postcondition to mdl result = mul (mdl a) (mdl b). The proof of this new specification is immediate and makes the second task trivial.

Fig. 1 .

 1 Fig. 1. Relations between sub-matrices and product function block (a: mat int) (r dr c dc: int) : mat int = create dr dc (\i j. get a (r+i) (c+j))

requires { 0

 0 ď flag } requires { flag = 0 Ñ a.mdl.cols = 1 _ exists k. a.mdl.cols = 2 * k } variant { a.mdl.cols + flag, flag } (* lexicographic order *)

  type with_symb = { phy : matrix int; ghost sym : expr; (* reflection *) } predicate with_symb_vld (env:env) (ws:with_symb) = e_vld env ws.sym ^(* internal dimension conditions *) e_mdl env ws.sym = ws.phy.mdl ^(* Model correlation *) ws.sym.e_rows = ws.phy.mdl.rows ^(* Dimensions correlation *) ws.sym.e_cols = ws.phy.mdl.cols

  let add_ws (ghost env:env) (a b:with_symb) : with_symb requires { a.phy.mdl.rows = b.phy.mdl.rows } requires { a.phy.mdl.cols = b.phy.mdl.cols } requires { with_symb_vld env a ^with_symb_vld env b } ensures { result.phy.mdl = add a.phy.mdl b.phy.mdl } ensures { result.sym = symb_add a.sym b.sym } ensures { with_symb_vld env result } = { phy = add a.phy b.phy; sym = ghost symb_add env a.sym b.sym } Introduction of variables is carried out by a similar combinator on top of submatrix extraction.

Acknowledgements We thank Arthur Charguéraud, Jean-Christophe Filliâtre, and Claude Marché for their comments and remarks.

‹ This work is partly supported by the Bware (ANR-12-INSE-0010, http://bware. lri.fr/) and VOCAL (ANR-15-CE25-008, https://vocal.lri.fr/) projects of the French national research organization (ANR) and by the Portuguese Foundation for the Sciences and Technology (grant FCT-SFRH/BD/99432/2014). 3 http://toccata.lri.fr/gallery/verifythis_2016_matrix_multiplication.en. html

A Challenge 1 original text

Consider the following pseudocode algorithm, which is naive implementation of matrix multiplication. For simplicity we assume that the matrices are square.

1. Provide a specification to describe the behaviour of this algorithm, and prove that it correctly implements its specification.

2. Show that matrix multiplication is associative, i.e., the order in which matrices are multiplied can be disregarded: ApBCq " pABqC. To show this, you should write a program that performs the two different computations, and then prove that the result of the two computations is always the same.

rOptional, if time permitss

In the literature, there exist many proposals for more efficient matrix multiplication algorithms. Strassen's algorithm was one of the first. The key idea of the algorithm is to use a recursive algorithm that reduces the number of multiplications on submatrices (from 8 to 7), see Strassen algorithm on wikipedia for an explanation. A relatively clean Java implementation (and Python and C++) can be found here. Prove that the naive algorithm above has the same behaviour as Strassen's algorithm.

Proving it for a restricted case, like a 2 ˆ2 matrix should be straightforward, the challenge is to prove it for arbitrary matrices with size 2 n .

B Strassen recursion scheme

Given three matrices A,B and M " AB partitionned as:



Then we can compute the partition of M from the two others as follow:

A 1,1 pB 1,2 ´B2,2 q X 4 " A 2,2 pB 2,1 ´B1,1 q X 5 " pA 1,1 `A1,2 q B 2,2 X 6 " pA 2,1 ´A1,1 q pB 1,1 `B1,2 q X 7 " pA 1,2 ´A2,2 q pB 2,1 `B2,2 q


Matthew Kay
email: mjskay@uw.edu

Steve Haroz

Shion Guha
email: sguha@cs.cornell.edu

Pierre Dragicevic
email: pierre.dragicevic@inria.fr

Special Interest Group on Transparent Statistics in HCI

Keywords: Statistics, methodology, user studies. ACM Classification H.5.m [Information interfaces and presentation (e.g., HCI)]

Transparent statistics is a philosophy of statistical reporting whose purpose is scientific advancement rather than persuasion. We propose a SIG to discuss problems and limitations in statistical practices in HCI and options for moving the field towards clearer and more reliable ways of writing about experiments.

Motivation

Empirical studies in HCI typically consist of solitary experiments analyzed through null hypothesis significance testing (NHST). However, this traditional approach is under growing criticism at CHI [START_REF] Kaptein | Rethinking statistical analysis methods for CHI[END_REF][START_REF] Cairns | HCI... not as it should be: inferential statistics in HCI research[END_REF][START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF][START_REF] Kay | Researcher-centered design of statistics: Why Bayesian statistics better fit the culture and incentives of HCI[END_REF] and has been strongly criticized for more than 50 years in other fields [START_REF] Kline | Beyond significance testing: Reforming data analysis methods in behavioral research[END_REF][START_REF] Cumming | The new statistics why and how[END_REF][START_REF]Estimating the reproducibility of psychological science[END_REF].

Problems with current practices include [START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF][START_REF] Wilson | RepliCHI SIG: From a panel to a new submission venue for replication[END_REF][START_REF] Kaptein | Rethinking statistical analysis methods for CHI[END_REF][START_REF] Kay | Researcher-centered design of statistics: Why Bayesian statistics better fit the culture and incentives of HCI[END_REF]:

• The use of statistical constructs (e.g, p-values) that most researchers have trouble grasping intuitively • Overemphasis on conveying evidence and numbers rather than useful information and generalizable conclusions, leading to tedious p-cluttered reports • Dichotomous thinking, i.e., thinking of hypotheses as either true or false, and of effects and evidence as either existing or not existing • Undisclosed flexibility in data analyses, yielding cherrypicked results or p-hacking (even if unintentional) • Simplistic criteria for paper acceptance (e.g., looking at whether results are "significant") leading to positive results bias, and thus an incomplete and distorted literature

What is Transparent Statistics?

Our use of the term transparent statistics is not meant to imply that statistical reports at CHI are necessarily opaque. Instead, it aims to emphasize transparency in reporting.

More specifically, we propose to refer to transparent statistics as a philosophy of statistical reporting whose purpose is to advance scientific knowledge rather than to persuade.

Although transparent statistics recognizes that rhetoric plays a major role in scientific writing [START_REF] Robert P Abelson | Statistics as principled argument[END_REF], it dictates that when persuasion is at odds with the dissemination of clear and complete knowledge, the latter should prevail. For example, when empirical data provides incomplete or mixed evidence, a transparent investigator should refrain from drawing definitive conclusions and instead communicate all relevant information "in intelligible form, in recognition of the right of other free minds to utilize them in making their own decisions" [START_REF] Fisher | Statistical methods and scientific induction[END_REF]. Transparent statistics puts clarity before messiness, and messiness before false clarity-study results are often disappointingly complex, but in transparent statistics the quest for scientific truth prevails over "aesthetic criteria of novelty, narrative facility, and perfection" [START_REF] Giner-Sorolla | Science or art? How aesthetic standards grease the way through the publication bottleneck but undermine science[END_REF].

Acknowledging the messiness of results is often at odds with our desire to make strong, definitive statements ("technique A outperforms technique B" ). But conveying uncertainty more faithfully represents our results and even makes them more useful: practitioners do not want to know if p is less than .05; they want to know by how much does technique A improve over technique B (plus-or-minus some error) so that they can perform a cost-benefit analysis and decide whether to adopt it. Besides advancing clarity within our field, transparent statistics can help address another existential crisis for HCI-impact on real-world systemsby expressing our results in statistical language that is amenable to assessing practical significance.

How to Move Towards Transparent Statistics?

The purpose of this SIG meeting is to discuss how we can move toward more transparent statistical practice in HCI and also what HCI can contribute to broader statistical reform. We offer several discussion points, ideas, and opinions to start that conversation.

Reporting Transparent Statistics

Transparent statistics are about both what we report and how we report it. While methodologists have been discussing what to report to maximize transparency (e.g, communicating simple/standardized effect sizes with frequentist/Bayesian interval estimates, clearly distinguishing between planned and unplanned analyses), HCI can advance guidelines for how to report transparent statistics in a userfriendly manner. For instance, clear, straightforward graphical communication of effects can be written into modern reporting guidelines [START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF]. These approaches could become both the standard within HCI and the standard we aspire to create through new statistical tools-what if the output of any procedure in a statistical package was an annotated, self-explanatory visualization, rather than a cryptic table? This approach may make some uncomfortable, as guidelines already exist that insist upon many orthodox practices that can be harmful to transparent statistical communication. These older standards lead to ubiquitous impenetrable results sections that are peppered with numerical statistical results. We plan to discuss how authors can educate reviewers when writing results that do not follow old norms. This includes amassing a set of citations that lend credence SIG Meeting #chi4good, CHI 2016, San Jose, CA, USA to (currently) unorthodox approaches; e.g., essays by advocates of estimation [START_REF] Cumming | The new statistics why and how[END_REF][START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF] and of Bayesian methods [START_REF] Kay | Researcher-centered design of statistics: Why Bayesian statistics better fit the culture and incentives of HCI[END_REF].

Having more papers in the field using these methods can also help. Done well, these methods could speak for themselves. Clearer communication (with relevant citations) can be enough to convince reviewers simply through the deeper understanding they gain from the work. However, some rethinking is still necessary: a wide confidence interval that just overlaps 0 in a small-n study is more honest than a p value just above .05 (and better informs future meta-or Bayesian analysis), but might feel like a lackluster result to a reviewer used to thinking in binary rejection criteria.

Emphasizing Practical Significance over Testing

In contrast to a focus on binary testing (is A better than B?), transparent statistics emphasize effect size (how much better?) and uncertainty (what are the upper and lower bounds on the difference?). These inform us on practical significance: is the difference large enough, and are we certain enough to act on it? Given an estimated difference between two conditions, a practitioner could apply a cost function to decide whether the increase in performance is worth the cost of switching to a new interface or technique.

Cost/benefit analysis, not statistical significance, is the language of industry, and therefore one way for results from HCI to make it out of the lab and into real-world systems.

Training and Education

Training and education is an important part of this debate. Many HCI researchers learn statistics in one of two ways: through an applied statistics course (for non-statisticians) taught by statisticians, or through a course (or part of a course) taught by an HCI or computer science professor in their home departments. The latter approach can perpetuate old norms in the field which, as we have argued, need to be reexamined and reformed. How can we better integrate transparent statistics education into HCI curricula (as is becoming more common in other fields)?

Open Data and Replications

While clear communication of statistical analyses is critical, publishing the underlying data allows those analyses to be verified. Open data allows readers to answer questions about aspects of analysis that may be missing from the text. It also allows subsequent researchers to analyze facets of the data that the original researchers did not examine, perform meta analyses on multiple publications, and more easily use existing data to form priors for future Bayesian analyses. Science is a cumulative and collective enterprise.

Nevertheless, questions have arisen regarding the costs and merits of open data. Documenting and anonymizing data takes time. There are also limits to its error-correcting ability. While reexamination of an experiment's data can help detect mistakes, problems can occur in any stage of an experiment, including incorrect stimulus presentation, incorrect response recording, and the possibility of a statistical fluke. Furthermore, reusing materials can propagate these mistakes across multiple publications. Overcoming these problems requires complete experiment replication [START_REF] Wilson | RepliCHI SIG: From a panel to a new submission venue for replication[END_REF], not just reproduction of the analysis.

Transparent Conclusions

While our focus is on reporting and analysis, transparent statistics necessarily go hand-in-hand with well-designed and implemented experiments with reasonable conclusions. The conclusions should be nuanced and not convey more certainty than the results [START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF]. Overgeneralizing results should also be avoided. If a technique is beneficial in one implementation or task [START_REF] Haroz | How capacity limits of attention influence information visualization effectiveness[END_REF], how can theory be used to make conclusions that extend beyond the narrow SIG Meeting #chi4good, CHI 2016, San Jose, CA, USA scope of the experiment? How we write about generalizability typically follows uncodified conventions that depend on whether the research took a hypothesis-driven or datadriven approach-themselves direct successors of deductive and inductive reasoning [START_REF] Dillon | User analysis in HCI-the historical lessons from individual differences research[END_REF]. Failure to differentiate the two often results in overclaiming about the external validity or generalizability of human-centered research [START_REF] Michael S Bernstein | The trouble with social computing systems research[END_REF]. Transparency is increased if research projects describe (1) how they connect to and build off of existing theories and (2) why or if the conclusions are externally valid.

HCI Can Help Statistics!

Beyond advancing transparent statistics within our own field, HCI can provide a unique voice in the ongoing conversation around improving the usability of analysis tools and improving the clarity of statistical communication. We can help improve cryptic statistical systems that are hard to learn, require substantial background to use, and even fail silently (returning incorrect results to unwitting users).

Conclusion

We propose a meeting at CHI to discuss the present and future of transparent statistical communication in HCI, a conversation we hope will improve the clarity, reliability, and impact of quantitative results in the field.