Jean-Christophe Filliâtre

Mário Pereira

In this paper we present the first formal proof of an implementation of Koda and Ruskey's algorithm, an algorithm for generating all ideals of a forest poset as a Gray code. One contribution of this work is to exhibit the invariants of this algorithm, which proved to be challenging. We implemented, specified, and proved this algorithm using the Why3 tool. This allowed us to employ a combination of several automated theorem provers to discharge most of the verification conditions, and the Coq proof assistant for the remaining two.

Introduction

Given a forest, we consider the problem of coloring its nodes in black and white, such that a white node only has white descendants. Consider for instance this forest:

It has exactly 15 colorings, which are the following: Koda and Ruskey proposed a very nice algorithm [START_REF] Koda | A Gray Code for the Ideals of a Forest Poset[END_REF] to generate all these colorings. 3 This is a Gray code algorithm, which only changes the color of one node to move from one coloring to the next one. If we read the figure above in a zig-zag way, we can notice that any coloring is indeed obtained from the previous one by changing the color of exactly one node.

There are many ways to implement Koda-Ruskey's algorithm. Koda and Ruskey themselves give two implementations in their paper. Filliâtre and Pottier propose several implementations based on higher-order functions and their defunctionalization [START_REF] Filliâtre | Producing All Ideals of a Forest, Functionally[END_REF]. Knuth has two implementations in C, including one using coroutines [START_REF] Knuth | An implementation of Koda and Ruskey's algorithm[END_REF]. In particular, Knuth makes the following comment: [...] I think it's a worthwhile challenge for people who study the science of computer programming to verify that these two implementations both define the same sequence of bitstrings.

Before trying to verify Knuth's intricate C code, a reasonable first step is to work out the invariants of Koda-Ruskey's algorithm on a simpler implementation. This is what we do in this paper, using the Why3 system. To our knowledge, this is the first formal proof of this algorithm.

This paper is organized as follows. Sec. 2 describes our implementation in Why3. Then Sec. 3 goes over the formal specification. Finally, Sec. 4 details the most interesting parts of the proof. The Why3 source code and its proof can be found at http://toccata.lri.fr/gallery/koda_ruskey.en.html.

Implementation

Our implementation of Koda-Ruskey's algorithm is given in Fig. 1. The syntax of Why3 is close to that of OCaml, and we explain it whenever necessary. The algebraic datatype of forests is declared on lines 1-3. A forest is either empty (constructor E) or composed of an integer node together with two forests, namely the forest of its children nodes and its sibling forest (constructor N). One can notice that the type forest is isomorphic to a list of pairs of nodes and forests.

The type of colors is introduced on line 4. The entry point is function main (lines 24-25). It takes an array bits as argument, to hold the coloring, and a forest f0. It then calls a recursive function enum, which implements the core of the algorithm.

Function enum operates over a stack of forests, using the predefined type list of Why3 (with constructors Nil and Cons). On entry, function enum inspects the stack. It will never be empty (line 9). If the stack is reduced to a single empty forest, we have just discovered a new coloring. We are free to do whatever we want with the contents of array bits (line 10), such as printing it, storing it, etc. If the stack starts with an empty forest, we skip it (line 11). Otherwise, the top of the stack contains a non-empty tree, with a root node i, a children forest f1, and a sibling forest f2 (line 12). If node i is white (line 13), we first enumerate the colorings of f2 together with the remaining st' of the stack (line 14), then we blacken node i (line 15), and finally we enumerate the colorings of f1, interleaving them with the colorings of f2 and st'. If node i is black (line 17), the process is reversed. First, we enumerate the colorings of f1 (line 18), so that all nodes of f1 are white again at the end. Then we whiten node i (line 19). Finally, we enumerate the colorings of f2 (line 20).

Specification

In this section we give function main a specification. The specification of function enum is considered being part of the proof and thus only described in the next section. The first requirement over function main is to have array bits large enough to hold all the nodes of the forest. So we start by defining the number of elements in a forest:

function size_forest (f: forest) : int = match f with | E → 0 | N _ f1 f2 → 1 + size_forest f1 + size_forest f2 end
In Why3, the function keyword introduces a logical function, i.e., a function with no side-effects and whose termination is checked automatically, and that one can use in a specification context. We use size_forest to introduce the first precondition of function main: let main (bits: array color) (f0: forest) requires { size_forest f0 = length bits } ...

To execute correctly, the program also requires the forest to have nodes numbered with distinct integers that are also valid indexes in array bits. These conditions are expressed, respectively, by predicates no_repeated_forest and between_range_forest, as follows:

predicate no_repeated_forest (f: forest) = match f with | E → true | N i f1 f2 → no_repeated_forest f1 && no_repeated_forest f2 && not (mem_forest i f1) && not (mem_forest i f2) && disjoint f1 f2 end predicate between_range_forest (i j: int) (f: forest) = forall n. mem_forest n f → i ≤ n < j
where mem_forest expresses that an element belongs to a forest:

predicate mem_forest (n: int) (f: forest) = match f with | E → false | N i f1 f2 → i = n || mem_forest n f1 || mem_forest n f2 end
and disjoint indicates that two trees have disjoint sets of nodes:

predicate disjoint (f1 f2: forest) = forall x. mem_forest x f1 → mem_forest x f2 → false
To write more succinct specifications in the following, we combine predicates between_range_forest and no_repeated_forest into a single predicate valid_nums_forest, which is added to the precondition of main.

predicate valid_nums_forest (f: forest) (n: int) = between_range_forest 0 n f && no_repeated_forest f let main (bits: array color) (f0: forest) requires { valid_nums_forest f0 (size_forest f0) } ...

We now turn to the part of the specification related to the enumeration of colorings. A coloring is a map from nodes, which are integers, to values of type color: type coloring = map int color At the beginning of the algorithm, all nodes of the forest must be colored white. We introduce a predicate white_forest to say so.

predicate white_forest (f: forest) (c: coloring) = match f with | E → true | N i f1 f2 → c[i] = White && white_forest f1 c && white_forest f2 c end
This predicate traverses the forest and checks that for each node i, its color c[i] is White. As for functions, termination of recursive predicates is automatically also checked. We can now use this predicate in the precondition of main: let main (bits: array color) (f0: forest) requires { white_forest f0 bits.elts } ...

Here bits.elts is the map modeling the contents of array bits, which happens to have type coloring.

Upon termination, the program must have enumerated all colorings, each coloring being visited exactly once. Since the code is not storing the colorings, we extend it with ghost code to do that. A ghost reference, visited, is declared to hold the sequence of colorings enumerated so far: To express that main enumerates all colorings exactly once, we specify that all colorings in visited are valid and pairwise distinct colorings, and that there are the expected number of colorings. The latter is easily defined recursively:

function count_forest (f: forest) : int = match f with | E → 1 | N _ f1 f2 → (1 + count_forest f1) * count_forest f2 end
Indeed, an empty forest has exactly one coloring (the empty coloring), and colorings of a non-empty forest are obtained by combining any coloring for the first tree with any coloring for the remaining forest. Last, the coloring of a tree is either all white (hence 1) or a black root with any coloring of the children forest. The postcondition of main states that we have enumerated this number of colorings: let main (bits: array color) (f0: forest) ensures { length !visited = count_forest f0 } ...

To be valid, a coloring must respect the constraint that if a node is colored white then its children forest must be all white. The predicate valid_coloring checks this constraint:

predicate valid_coloring (f: forest) (c: coloring) = match f with | E → true | N i f1 f2 → valid_coloring f2 c && match c[i] with | White → white_forest f1 c | Black → valid_coloring f1 c end end
Each time a white node is reached, we use predicate white_forest to ensure that its children forest is white. Comparing two colorings requires to ignore values outside of the array range. Thus we introduce predicate eq_coloring to state that two colorings coincide on a given range 0..n -1:

predicate eq_coloring (n: int) (c1 c2: coloring) = forall i. 0 ≤ i < n → c1[i] = c2[i]
We are now in position to give the full code and specification of function Note that main assigns visited to the empty sequence before calling enum. The forest f0 is also passed to enum as an extra, ghost argument.

Proof

As shown in Fig. 1, program main simply amounts to a call to enum. So, in order to prove that main respects its specification we need to specify and prove correct function enum. In this section we go over the most subtle points in the specification and proof of enum. The complete specification for this function is shown in Fig. 2.

Function enum operates on a stack of forests, and we need to relate that stack to the original forest f0 (which is passed to enum as a ghost argument). To do so, we introduce a predicate sub st f c that relates a stack st, a forest f , and a coloring c. It is defined with the following inference rules:

sub [f ] f c sub st f 2 c sub st (N i f 1 f 2 ) c sub st f 1 c c[i] = Black sub (st ++ [f 2 ]) (N i f 1 f 2 ) c
The first rule states that a stack containing a single forest f is a sub-forest of f itself. ([f ] is a notation for a one-element list.) The second rule states that we can skip the left tree (i, f 1 ) of a forest (N i f 1 f 2 ). The third rule states that we can plunge into f 1 provided c[i] is black and f 2 appears at the end of the stack. (Operator ++ is list concatenation). In Why3, such a set of inference rules is defined as an inductive predicate: We use this predicate in enum's precondition, with the current stack, the initial forest f0, and the current coloring (line 5). Together with preconditions in lines 2-4, we are already in position to prove safety of function enum. Indeed, nodes found in the stack do belong to f0, according to sub, and thus are legal array indices.

To specify what enum does, we need to characterize the final coloring in the enumeration (e.g., the bottom right coloring in the 15 colorings on page 1). Indeed, for the algorithm to work, it has to enumerate all colorings in a reverse order when called on such a final coloring, ending on a white forest. Since the algorithm is interleaving the colorings for the various trees of the forest, the final configuration depends on the parity of these numbers of colorings. So we first introduce a predicate even_forest f which means that forest f has an even number of colorings:

predicate even_forest (f: forest) = match f with | E → false | N _ f1 f2 → not (even_forest f1) || even_forest f2 end
Though we could define it instead as count_forest being even, we prefer this direct definition, which saves us some arithmetical reasoning. We can now define what is the final coloring of a forest:

predicate final_forest (f: forest) (c: coloring) = match f with | E → true | N i f1 f2 → c[i] = Black && final_forest f1 c && if not (even_forest f1
) then white_forest f2 c else final_forest f2 c end Though we can see final_forest as the dual of white_forest, from the algorithm point of view, it is clear that a final forest is not a black forest (as one can see on page 1). Function enum requires all forests in the stack to be either white or final. To say so, we introduce the following recursive predicate: From a big-step perspective, Koda-Ruskey's algorithm is switching from a white coloring to a final coloring and conversely. But enum is operating over a stack of forests and thus requires us to be more precise. For the tree on top of the stack, we are indeed switching states. However, for the next tree (its right sibling in the same forest, if any, or the next tree in the stack, otherwise), the state changes only if the first tree has an odd number of colorings. Otherwise, it is kept unchanged. To account for this inversion, we introduce the following predicate that relates a stack st and two colorings, namely the first coloring c1 and the last coloring Note that the coloring of the first forest in the stack is always inverted, while the inversion of the remaining of the stack depends on the parity of the first forest. The predicate unchanged st' c1 c2 states that c1 and c2 coincide on any node in the stack st'. The postcondition on line 9 in Fig. 2 relates the initial contents of array bits (written old bits) to its final contents using predicate inverse.

We briefly go over the remaining clauses in the specification of enum. The stack is never empty (line 2). The initial forest f0 has as many elements as the bits array (line 3) and is correctly numbered from 0 (line 4). In both preand post-state, the coloring must be valid w.r.t. f0 (lines 7 and 10). A frame postcondition ensures that any element outside of the stack is left unchanged (line 8). We characterize the sequence of enumerated colorings with a predicate stored_solutions (line 11), not shown here. It means that visited has been augmented with new, valid, and pairwise distinct colorings, which coincide with array bits outside of the stack nodes. Finally, we ensure termination with a lexicographic variant (line 12). In all cases but one, the size of the stack is decreasing, when defined as its total number of nodes, as follows:

Conclusion

In this paper we presented a formal verification of an implementation of Koda-Ruskey's algorithm using Why3. To our knowledge, this is the first formal proof of this algorithm. The main contribution of this paper is the definition of the algorithm's invariants (mostly, the definition of predicates any_stack and inverse).

We argue that such definitions could be readily reused in other proofs of this algorithm, whatever the choice of implementation and of verification tool (e.g., Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], VeriFast [START_REF] Jacobs | Veri-Fast: A powerful, sound, predictable, fast verifier for C and Java[END_REF], or Viper [START_REF] Müller | Viper: A verification infrastructure for permission-based reasoning[END_REF]). We intend to improve our verification with a proof that count_forest is indeed the right number of colorings. One way to do that would be to implement a naive enumeration of all colorings, with an obvious soundness proof. We are also interested in verifying higher-order implementations of Koda-Ruskey's algorithm, such as the ones by Filliâtre and Pottier [START_REF] Filliâtre | Producing All Ideals of a Forest, Functionally[END_REF]. This means extending Why3 with support for effectful higher-order functions.

Fig. 1 :

 1 Fig. 1: An implementation of Koda-Ruskey's algorithm.

  val ghost visited: ref (seq coloring) (Sequences are predefined in Why3 standard library.) The idea is that this reference is updated each time a new coloring is found, on line 10 of the program in Fig. 1.

Fig. 2 :

 2 Fig. 2: Specification of function enum.

  main: let main (bits: array color) (f0: forest) requires { size_forest f0 = length bits } requires { valid_nums_forest f0 (size_forest f0) } requires { white_forest f0 bits.elts } ensures { length !visited = count_forest f0 } ensures { let n = length !visited in forall j. 0 ≤ j < n → valid_coloring f0 !visited[j] && forall k. 0 ≤ k < n → j = k → not (eq_coloring (length bits) !visited[j] !visited[k]) } = visited := empty; enum bits f0 (Cons f0 Nil)

  inductive sub stack forest coloring = | Sub_reflex: forall f, c. sub (Cons f Nil) f c | Sub_brother: forall st i f1 f2 c. sub st f2 c → sub st (N i f1 f2) c | Sub_append: forall st i f1 f2 c. sub st f1 c → c[i] = Black → sub (st ++ Cons f2 Nil) (N i f1 f2) c

  predicate any_stack (st: stack) (c: coloring) = match st with | Nil → true | Cons f st → (white_forest f c || final_forest f c) && any_stack st c end It appears as a precondition on line 6.

  The last case is when the stack is of the form Cons E st', for which we perform a recursive call on st'. The number of nodes remains the same, but the stack is structurally smaller, hence the lexicographic variant.Proof Statistics. To make the proof of enum and main fully automatic, we introduce 19 proof hints in the body of enum and 37 auxiliary lemmas. Many of these lemmas require a proof by induction, which is done in Why3 by first applying a dedicated transformation (interactively, from the Why3 IDE) and then calling automated theorem provers. The table below summarizes the number of VCs and the verification time.Two VCs are proved interactively using Coq. These proofs amount to 55 lines of Coq tactics, including the why3 tactic that allows to automatically discharge some Coq sub-goals using SMT solvers. All other VCs are proved automatically, using a combination of theorem provers as follows:Our proof process consists in calling Alt-Ergo first. When it does not succeed, we switch to CVC4. And so on. So the numbers above should not be interpreted as "Alt-Ergo discharges 139 VCs and CVC4 only 57". Though we could call all provers on all VCs, we choose not to do this in practice to save time. A more detailed table is available on-line at http://toccata.lri.fr/gallery/koda_ ruskey.en.html.

	function size_stack (st: stack) : int = match st with
	| Nil → 0
	| Cons f st → size_forest f + size_stack st
	end
		number automatically verification
		of VCs	proved	time
	lemmas	102 100 (98%)	14.72 s
	enum	94	94 (100%)	47.51 s
	main	7	7 (100%)	0.07 s
	total	203	201 (99%)	62.30 s
	prover	VCs proved
	Alt-Ergo 1.01	139
	CVC4 1.4		57
	Z3 4.4.0		3
	CVC3 2.4.1		1
	Eprover 1.8-001	1

Acknowledgments. We thank Claude Marché for his comments on earlier versions of this paper.

This research was partly supported by the Portuguese Foundation for Sciences and Technology (grant FCT-SFRH/BD/99432/2014) and by the French National Research Organization (project VOCAL ANR-15-CE25-008). 3 Such a coloring has a mathematical interpretation as an ideal of a forest poset.


Yvonne Jansen

Kasper Hornbaek

Pierre Dragicevic
email: pierre.dragicevic@inria.fr

What Did Authors Value in the CHI'16 Reviews They Received?

Keywords: Peer review, user studies, CHI, surveys .g., HCI)]

Peer-review is key to assessing work in HCI conferences. The content and process of peer-review, and how it moves scholarship forward or impedes it, are much discussed but little data is available. We provide initial data from surveying 46 authors who submitted papers and notes to CHI 2016, and asking them what they found helpful and unhelpful in their reviews. Responses were overall positive, and showed that authors appreciated encouragement, ideas for related work, and seeing their work fairly assessed. At the same time, some authors commented that reviews may not be inclusive of new approaches, may contain insufficient details, and occasionally seem unreasonable. They also noted issues specific to the rebuttal process. We discuss how instructions for reviewers could be improved, and link our findings to ongoing debates on peer review.

Introduction

What do people who submit to CHI value to see in a peer review of their submission? What do they like and dislike? These are common topics of discussion, both in anticipation of the reviews and after receiving them. Whereas personal anecdotes and opinions are legion, little factual information is available. Opinions on what is appropriate in a review likely differ across people, particularly in a multicultural community such as CHI. Also, reviews and unfiltered opinions are rarely shared outside local peer groups, thus it is difficult to get a sense of what authors really value in the reviews they receive, and what constitutes an effective review. Overall, it is hard for authors to know what to expect from a review, difficult -in particular for junior reviewers -to know what to put into a review, and unclear for CHI as a whole how to create effective reviewing guidelines.

In this article we summarize data collected from 46 authors who shared their experiences (sometimes with quotes from reviews) through an "unofficial CHI reviewing survey". In contrast to the official CHI reviewing survey, the aim of our survey is to start an open discussion of reviews with the community, based on data and facts. We hope our survey will inspire the collection of more data to help reviewers craft better reviews and conference chairs craft more effective reviewing guidelines.

Method

We conducted an online survey on the content and perceived quality of CHI '16 reviews, including a part focusing on reporting strategies for user studies. We asked questions such as "What is your overall impression of the review quality for your submission?", "In your [study] analyses, what quantities did you report in numerical form?", or "Which aspects of your study received positive comments from reviewers?". The full survey with all questions is available at tinyurl.com/unofsurv. Three questions invited respondents to share review quotes and comment on them. A link was provided to a text where we discuss the legal, ethical and practical implications of sharing received reviews, with links to external sources (mostly discussion forums). The full text is available at tinyurl.com/sharereviews. We stated that the dataset will be shared publicly, and gave respondents the option to keep their review quotes and/or personal comments private.

We advertised the survey through snowballing (online social networks and emails) starting half an hour after CHI submitters had received their final reviews (16 Dec 2015). We tried to reach out to as many communities as possible by emailing researchers from different cities in Americas, Europe, and Asia. The survey remained open for a period of 20 days, during which all respondents (and their co-authors) could edit or retract their responses.

As survey responses were not randomly sampled from all CHI submissions (due to self-selection and possibly community bias), we do not report inferential statistics but summary statistics and a qualitative analysis of responses.

Quantitative Overview of Responses

We received 52 responses submitted by 46 respondents. Each response concerns a single CHI submission, and authors of multiple submissions could respond multiple times.

Submission Types

The responses included 36 full papers (69%), 14 notes, and 2 unspecified. The most common CHI contribution types (following the typology listed on the CHI website) were Understanding Users (44%) and Development or Refinement of Interface Artifacts or Techniques (21%). Of the 52 responses, 20 (38%) were accepted (2 with shepherding), 31 (60%) were rejected, and 1 was unspecified. Responses were thus slightly biased towards accepted submissions 1 .

Perceived Review Quality

Authors' overall perception of review quality was rather positive but very diverse, ranging from exceptionally good to exceptionally poor (see Figure 1). Reviews of rejected submissions tended to be judged more negatively than reviews of accepted submissions. Nevertheless, reviews of rejected submissions were occasionally well-received, and some authors of accepted papers felt they got poor reviews.

User Studies

Forty-four out of 52 responses (85%) reported a user study. Of these, 8 were quantitative, 9 were qualitative, 26 used mixed methods, and 1 was unspecified. Studies involved from 5 to 1618 participants in total (median 30), summed across all experiments pilots included (see Figure 2). Sample sizes were thus extremely diverse and did not predict acceptance, except perhaps in the extremes.

Among the 34 studies where at least some quantitative data were reported (this includes mixed methods), diverse statistical analysis and reporting strategies were used (Figure 4). It appears that papers were accepted and rejected across all categories. Bayesian analysis options were offered in the form but no respondent selected them. The qualitative methods used were diverse but a further analysis of these methods would go beyond the scope of this article. The degree to which reviewers approved of statistical methods varied a lot across responses, according to respondents (Figure 3, x-axis). Reviewers' approval was strongly linked to paper acceptance. Authors also varied as to how much they agreed with reviewers' methodological concerns (Figure 3, y-axis). Although agreement was frequent, strong reviewer disapproval never led to author agreement.

Textual Content

Responses included a total of 74 review quotes and 46 personal comments on these quotes. Respondents agreed to make 50 (68%) of the review quotes public, and 30 (65%) of the comments public. Some comments are quoted below, and more data is available at tinyurl.com/chi16reviewdata.

Qualitative Analysis

Textual content was classified through affinity diagramming: we printed a summary report for each response, which we cut up in pieces and sorted thematically. We used these themes to write a code book containing 37 codes grouped in 9 categories. One author coded the entire set of quotes, comments, and suggestions, while the other two authors coded one third each. We used the frequency counts of codes as a measure for including themes in this report and provide a subjective selection of salient responses here. The following sections contain paraphrased reviewer quotes2 and quotes from survey respondents which are typeset differently. Keep in mind that reviewer comments are necessarily taken out of context and may not reflect "the truth" but are only intended to give some insight into the author's perception of their reviews.

As far as possible, we tried to contrast high-quality reviewer comments with those authors considered to be of lowquality. However, review quotes which authors considered high-quality are not necessarily positive in content, but might have been selected by respondents because they were particularly helpful, informative, or constructive.

General Comments on Reviews

A number of general comments, both positive and negative, were offered concerning content, form and tone of reviews.

Encouraging Tone

In the "high-quality reviews" section of the survey, ten responses included review quotes with encouraging comments. Encouraging comments could be simple and rather unspecific such as that all reviewers recognized that the paper was doing a great job. Authors particularly appreciated when reviewers not only critiqued their submission, but also expressed which parts were good or whether the authors were on to something interesting and relevant.

Detailed versus Vague Comments

Authors appreciated detailed reviews that provided clear and actionable remarks. One response highlights an exceptionally constructive review with the following explanation:

"This reviewer presented overall review / summary followed by the list of things that needs to be addressed with SUBSTANTIVE marks when needed. I really appreciated this review because it was done by a domain expert (4 on self-rating, but I think this reviewer deserves 5) and VERY thorough. Also, with SUBSTAN-TIVE mark, I could see what are the weakest points of my paper and figure out how to make it stronger (it also helped me set my rebuttal strategy)"

Conversely, four responses included complaints about remarks being too vague, such as the necessity to do "some" extra experiments, on which the author commented: "This is vague, unhelpful, and could be applied to any paper. It is unclear what extra experiments this reviewer expects to see, and no suggestions were offered."

Similarly, one response included a quote asking for a "lightweight informal study" without any suggestions how such a study might look like. The author stated that they discussed this question in the paper and the rebuttal. Thus more concrete suggestions what the reviewer would consider sufficient would have been more constructive.

One author sent us the following comment: "... this reviewer was "sure others already did this" -but this reviewer couldn't point to a similar experiment, study or finding in literature to support his claim."

The overall sentiment can be summarized by one respondent who suggested:

"If you say the findings are not new, please give at least one example saying where it has been done."

Balance

Balanced reviews that acknowledge the positive while providing clear recommendations for improving the weak parts were particularly well received. One respondent appreciated the "detailed responses from referees [...] including what they found good, what they found lacking, and the recommendations offered", while another one found a reviewer's comment "particularly good because it made a positive comment (having made explicit ethical issues), criticized (maybe still dangerous for patients), pointed to people with whom this should be discussed (IRB), and provided literature pointers to read about this subject."

Another author commented:

"I think the previous comment was particularly useful because the reviewer was not only criticizing, but putting her or himself in my place and explicitly telling me how they would change it."

Attention Paid to the Paper

Two responses lauded reviewers for having read the paper carefully, e.g., one author appreciated that "reviewers read and understood the paper".

At the same time, eight responses included remarks about reviewers not reading the submission carefully enough. One author suggest as a guideline "that reviewers read the paper carefully, or not review it at all?" Another author offered the following comment:

"RTFM -where M stands for Manuscript! Some papers are trying to address a complex topic and it cannot be made simpler without dumbing down the quality of the submission -to provide scientific rigour and good scholarship the author needs to use complex arguments. If you do not have time to read the paper then do not accept to review the paper -it is worse to volunteer and do a bad job than to not volunteer at all!"

Level of Understanding

Related to the previous issue is the reviewer's level of understanding of the submission content. While one response expressed appreciation for a reviewer's level of understanding, seven responses complained about a lack of understanding. Here are comments from four different responses:

"Reviewer completely misunderstood the analysis. There was only one independent variable." "The questions R2 raised were already answered in the papers. It was clear that he/she did not understand parts of our design." "one reviewer saying that he can't believe the results but obviously he did not understand the methods and another reviewer clearly not understanding the value of qualitative results" "Twice (reviews + rebuttal) my AC did not clarify on a misunderstanding from one reviewer. The reviewer did totally misunderstand the concept while all others did not."

Unreasonable Requests

Seven responses referred to unreasonable requests such as effectively asking authors to write a different paper. One author felt that a reviewer's remark "would apply to the next iteration, not this one" while another author commented: "Asking to expand discussion beyond the scope of our work or what our data can cover seemed too much to ask."

Similarly, another author commented:

"This felt like a classic "the reviewer wished we wrote a different paper than we did" review. They were well-intentioned and were clearly trying to make our work stronger, but this review was not helpful in evaluating our current submission."

Structure and Length

Reviewers' styles concerning structure and length of their reviews varied considerably. We highlight here a few examples which authors deemed particularly valuable.

For a rejected submission the author indicated as high quality aspects of the received reviews "very long and detailed reviewers", and that "reviewers sorted their comments to give major and minor comments". Another one mentioned:

"Two of the externals broke down their review into paragraphs like: Significance, Originality, Validity, Method, Presentation clarity, Previous work. I like this format, since it more encourages to cover all the goods and the bads."

While authors generally praised long reviews, three commented negatively on reviews that were too short: "Writing a paragraph is not considered a review at CHI" and:

"There should be a minimum length for the reviews -it's ridiculous to see some reviews that are one paragraph vs. 3 pages long." "[...] students work very hard, and they deserve more than oneliner reviews from the most respected conference in HCI."

No author complained about a review that was too long.

Remarks Inappropriate in a Review

Four responses referred to remarks that could be deemed inappropriate in a review. For example, one reviewer said that what an author did in their submission would make the entire community look bad and should therefore not be supported. One primary AC offered a personal attack as a post-rebuttal by commenting that for a paper written by well-known authors, the number of issues was surprising.

Studies

User study methodology traditionally generates lots of disagreement between researchers, and this is why one part of our survey focused on user studies.

Study mandatory?

Only a few responses referred to the long-standing debate on whether every CHI paper needs a study (we counted one positive reference, one negative and two neutral). One author shared review excerpts where a reviewer asks for a field study to validate findings resulting from a literature review. Another reviewer wrote as a post-rebuttal comment that while Infovis published cool but unusable ideas, there should be at least for CHI some form of validation.

The same author was told from a different reviewer that the efficiency of their proposed techniques would be difficult to validate with a user study, as no status quo existed to compare against.

Reviewers occasionally asked for an extra study. One author stated that "referees wanted far more precision than was appropriate for a study informing initial design (where we were trying to scope out the design space), and then asked for yet another study of the system we developed from that study."

Sample Size

The number of study participants is another common point of contention. Indeed, authors and reviewers disagreed (often inconsistently across responses) on what is an "appropriate" sample size, particularly for qualitative studies.

An author offers as a suggestion for reviewers:

"Pay more attention to the contribution of the paper than criticizing small points that makes less difference in the final results such as number of participants in a qualitative study, the need of evaluation in every study."

Statistical Reporting Methods

Ten responses referred to the use of statistical analysis and reporting methods. We received responses from authors using different approaches, where each was sometimes positively received, and sometimes negatively received.

For example, in one response, an author pointed out that reviewers did not agree with the use of estimation, i.e., reporting interval estimates without p-values: "One of the reviewer was concerned with the methodology we used for analyzing our data. We calculated confidence intervals (bootstraping), and presented our results using graphs. [...] We were reproached of not using inferential statistics. [...] estimation methods ARE inferential statistics, so the argument per se is unfounded and fallacious."

Another submission, also using estimation, was criticized for log-transforming their data, even though the authors provided a CHI reference to explain and justify their choice.

In a different submission, reviewers reacted positively to the use of estimation:

"ALL reviewers were positive about the evaluation, and one of them even commented on the statistical method used, which they qualified to be "easier to interpret" than pValues (estimation methods are not common at CHI)."

Conversely, study reports relying on more traditional methods (i.e., null hypothesis significance testing / NHST) were occasionally criticized for being hard to understand. In one of the responses, the authors report a series of regression tables and shared a reviewer's comment stressing that the high number of p-values in the paper was difficult to comprehend.

One author submitted a review quote where the reviewer stated that the statistics were standing too much in the foreground and a discussion of what this work meant was lack-ing. The author commented: "We were very thorough and one of the reviewers commented that we were rigorous but that he/she got TIRED of reading so much statistics!"

In two cases, the authors seemed to have entirely abstained from using any inferential statistics. In response to one of these cases, a reviewer pedagogically explains that inferential statistics were needed to support the conclusion that there was no effect, especially with the presence of large statistical noise. In another case, the authors seemed to have explicitly stated known problems with NHST to justify their decision to refrain from using statistical inference and to only report summary statistics, which reviewers found unacceptable.

The review process

A number of comments had to do with the review process in general, including the role of ACs and of the rebuttal.

The Role of Associate Chairs

Twelve responses commented on AC reviews or on the role of ACs, but were overall balanced: four positive, four negative and four neutral.

Several AC reviews were praised and found extremely helpful. One respondent wrote "1AC's comment on what needs to be addressed on rebuttal was very helpful", while another wrote:

"The meta-review acknowledged concerns shared across reviewers in this work, and simultaneously made a suggestion for how to find space to fix it in a dense note."

Other examples of clearly positive feedback can be found in the subsections "Encouraging Tone" and "Detailed and Vague Comments".

Other respondents however found that their AC did not fulfill their role of overseer and moderator. One author who sub-mitted private comments wishes their AC had weighed in more in their meta-review, instead of simply summarizing reviewers' comments without considering whether these were justified. Similarly, an author commented:

"The AC should comment on all reviewers. Twice (reviews + rebuttal) my AC did not clarify on a misunderstanding from one reviewer. The reviewer did totally misunderstand the concept while all others did not. The AC did never picked this up. That's just unprofessional."

While a different respondent wrote:

"ACs should be instructed to ask the externals to revise their review when they are offending or when they write mistakes, and if the external does not respond, the AC(s) could always add a comment in the meta-review to make it explicit that that or that comment is not appropriate."

One author received no meta-review but was instead invited by the AC to do it themselves. That AC stated that reviewers raised valid points and asked the authors to read the reviews and summarize the questions. The author requested:

"More guidelines for ACs how to write a good meta review to give authors a chance in the rebuttal [...] How can we ever answer to all [questions] in a 1 1/2 page rebuttal? Without a meta review, you just pick the major ones, but that doesn't help to clear all questions of the reviewers ..."

Post-Rebuttal Comments

A relatively large number of survey responses (5 positive, 8 negative, 9 neutral) referred to post-rebuttal comments, although our survey had no specific question on this.

One author shared a long excerpt from a post-rebuttal reviewer comment as a high-quality review example. This excerpt clearly shows that the reviewer considered the rebuttal and argues why the changes described in the rebuttal would still require an additional review cycle, hence the decision remained to reject the paper. Another author writes that "all reviewers wrote a fair answer to the rebuttal".

Several authors however complained that their rebuttal was mostly ignored by reviewers or that they received no postrebuttal comments. One author suggests: "Clearly state if there is a chance that the rebuttal could reverse the decision. If there is no way it can, then it's best to save author's time. Some reviewers do not even read the rebuttal."

On the issue of post-rebuttal comments, one author (whose paper was accepted with high scores) writes:

"We received the post-rebuttal reviews. How many of the 5 reviewers replied? TWO. How many total number of lines used per review? ONE. Did 1AC (who raised 3 issues) reply? NO. This is very disrespectful."

Even when rebuttals are considered, authors are often disappointed by how hard it is to change reviewers' mind:

"We spent a lot of time in rebuttal defending our decisions, and still only sort-of convinced the reviewer."

Another author shared a post-rebuttal comment tersely stating that the reviewer read the rebuttal, that all questions were addressed, but it did not change their mind.

Insights into the Review Process

In five survey responses, authors spontaneously mentioned that they appreciated when ACs shared information about the review process. In a meta-review comment highly appraised by the author, the AC disclosed having played a role in reviewing the submission the year before and summarized the outcomes from last year's submission.

Another author shared a review quote pointing out that the paper was discussed at the PC meeting and the rebuttal was considered. Even though the submission was in the end rejected, the author commented:

"It was nice to know that our paper had been discussed at the PC meeting, and we know that, given our scores, this may very well have not happened. We appreciate that our work had been carefully considered by the committee."

Another author made similar comments: "...I very much appreciate that both 1AC and 2AC made a thorough report about what happened during the PC (discussion before and during the meeting, additional AC assigned), and very well summarized what was the major point that played against acceptance. The concerns are fair, and the recommendations are helpful and encouraging."

Suggestions by Authors

One part of the survey asked respondents if they had any suggestions to improve the existing reviewing guidelines: • Eight respondents asked for more guidance on what is expected in a rebuttal and its possible impact, • Six respondents asked for more guidance on how to write reviews. One specifically suggests to "maybe diversify the reviewing guidelines a bit according to the subcommittee",

• Five respondents asked for more open-minded reviews:

"...be more open to new ideas and new ways of doing research than asking for a boring structure that has been followed for 20 years."

• Three respondents asked for a better way of controlling reviewer expertise, e.g.:

"Reviewers should report their expertise in individual areas (study design, statistics, engineering, ...). ACs should then assign different tasks to one or more suitable reviewers (check spelling, check for novelty, check equations, etc.) in order to make reviews more thorough."

• Two respondents asked for more accountability, i.e., "more Incentives for the Reviewers to actually produce high quality reviews", and "means of punishing sloppy readers :)" • Two respondents advocated a revise-and-resubmit cycle similar to CSCW 2012 [START_REF] Grudin | Varieties of conference experience[END_REF]:

"ACM CSCW seems to do a better job of it now, as they have a full two-pass process. I suspect this gives referees and ACs more latitude in suggesting improvements, then waiting to see how the authors handle that. Because authors respond with a paper (vs just a rebuttal), I think referees and ACs take that attempt more seriously. [I should note that I was initially skeptical about the ACM CSCW process]."

Feedback on our Survey

Most respondents were very positive and were looking forward to the outcomes of this survey. Two respondents shared reservations about sharing review quotes:

"I hesitated a lot before submitting something. I suspect many people fear the "unofficial" aspect of this survey. I am myself only half comfortable reporting this, because I believe that reviewers could manage to trace back our identity. But good initiative, to try to improve the reviewing process."

"I did not feel comfortable in sharing our reviews -even as a reviewer and a metareviewer, I wouldn't want my reviews to be quoted out of context. I think we should have a better way of collecting this kind of feedback."

Our survey sparked discussions in private, in social networks and in the alt.chi review and discussion forum, revealing polarized opinions on whether it is ethically appropriate to share review quotes without explicit reviewer permission (also see discussions at [START_REF]Ethics of publishing received peer reviews[END_REF][START_REF] Venkatasubramanian | Who owns a review, and who's having the conversation? Online[END_REF]). In our opinion, the merits of releasing such a valuable source of information likely outweigh the occasional and minor harm that may result from commenting on anonymous review quotes unfairly.

Discussion

Overall, many reviews are found to be helpful and of excellent quality. But how can we improve the others?

1. Can guidelines be improved? Many of the the authors' concerns and proposals as captured in our survey highlight dos and don'ts that are already covered in both official and unofficial reviewing guidelines (e.g.: seek out the positive, be specific, be courteous, and avoid very short reviews [START_REF]Guide to Reviewing Papers and Notes[END_REF][START_REF]CHI Reviewing: A Guide and Examples[END_REF][START_REF] Vgtc | Ethics Guidelines for Reviewers[END_REF][START_REF] Hinckley | So You're a Program Committee Member Now: On Excellence in Reviews and Meta-Reviews and Championing Submitted Work That Has Merit[END_REF]). It appears that these guidelines go often ignored. How can we have reviewers read them and follow them? One possibility could be, in addition to improving guidelines, other strategies to ensure that the guidelines play some role in how reviewers assess a paper. These include structuring review forms, injecting questions into such forms, giving more examples of using guidelines, and structuring courses/learning activities around applying them.

Other findings from our survey are less discussed and not well addressed in the official CHI reviewing guidelines. These include a desire for more transparency and honesty about the process, as well as more openness towards different methods. For instance, there are many debates about statistical practice (e.g., [START_REF] Dragicevic | Fair Statistical Communication in HCI[END_REF]), but multiple valid approaches exist and the choice of methods and reporting style is the author's decision. The same way authors are required to justify their use of non-standard methods, reviewers should be required to provide references when they deem these methods insufficient. However, CHI peer reviewing is not the best place to advocate one's preferred methods.

Apart from alt.chi, the review system at CHI is closed. Information flows poorly. The only way for authors to react to their reviews is through the rebuttal which usually is only read by a handful of reviewers assigned to one paper. Instead, continuous feedback should be provided to reviewers, meta reviewers, and conference chairs about authors' expectations and their experience with the process. This should be no surprise to HCI researchers. CHI does conduct surveys, it also has hard-working and dedicated volunteers, and the process is improving constantly. However, these surveys are analyzed behind closed doors and can at best influence top-down changes. While unofficial surveys such as ours cannot paint a complete picture, data can nonetheless contribute to building a richer picture and driving public discussions.

Guidelines for all

Reviewing guidelines are almost exclusively for external reviewers. Instructions specifically for meta reviewers at CHI are rather limited (e.g., less than 300 words in the 1AC instructions for CHI 2016), despite the enormous difficulty and responsibility implied [START_REF] Bardzell | A Position on Peer Reviewing in HCI[END_REF][START_REF] Hinckley | So You're a Program Committee Member Now: On Excellence in Reviews and Meta-Reviews and Championing Submitted Work That Has Merit[END_REF]. Our survey respondents suggest that (at least some) ACs need more specific guidance about their roles. An excellent unofficial guide for meta reviewers has been recently written [START_REF] Hinckley | So You're a Program Committee Member Now: On Excellence in Reviews and Meta-Reviews and Championing Submitted Work That Has Merit[END_REF] and is advocated in this year's CHI reviewing guidelines. This is an excellent step forward, but will reviewers read it if its recommendations are not integrated to official guidelines?

Better match expectations

It seems that much of the distress and disappointment felt by some authors has to do with various unmet expectations about the role of meta reviewers, of rebuttals, and the amount of details in reviews. Not all expectations may be realistic. The previously quoted examples for authors appreciating more insight into the hidden parts of the review process suggest that more transparency and better communication about what can and what cannot be expected might help to match expectations from both sides. Peer review is an inherently noisy process, especially in large conferences [START_REF] Grudin | Varieties of conference experience[END_REF]. The workload on both external reviewers and meta reviewers is extremely high, with tight deadlines. Even scientists suffer from cognitive biases, they do not easily change their mind in the face of evidence, and the relative ineffectiveness of rebuttals should not be a surprise. Why not provide a honest picture of all of this to authors?

4. Allow reviews to circulate more freely Whereas guidelines are legion, actual examples of reviews and meta reviews are not. Yet a set of exemplary reviews would provide invaluable training material for reviewers and be a useful exemplification of good review practice. There are many ways a review can be poor, so we need many examples of these too. User feedback in the form of author comments on reviews are crucial too, in order to guide the evolution of review guidelines and processes, and to facilitate open discussions on best research practices [START_REF] Lindley | Peer review and design fiction: "Honestly, they're not just made up[END_REF].

This study offers a first exploration in collecting and analyzing such user feedback. We would like to see it continued alongside the official survey for reviewers. By allowing authors to share their comments publicly and anonymously, we aim to give a voice to authors who would like to explain what they personally value in reviews, and to authors who feel their hard work has been unfairly treated and were not given the chance to express their "user feedback" in other ways. Negative emotions will necessarily surface, but feedback collected in such a way will likely be more content-rich and ultimately more productive than isolated rants from disgruntled authors near their local water cooler.

Figure 1 :

 1 Figure 1: Perceived review quality for each response (n = 52),from exceptionally poor (1) to exceptionally good[START_REF]CHI Reviewing: A Guide and Examples[END_REF].

Figure 2 :

 2 Figure 2: Total number of participants per study (n = 44).

Figure 3 :

 3 Figure 3: Scatterplot showing to what extent reviewers approve of the author's choice of data analysis and reporting strategy, and to what extent the author agrees with their criticisms (n = 34).

The acceptance rate for papers at CHI'16 was

23.4%.

Due to a controversy during the alt.chi review process over whether or not publishing review quotes without reviewer permission is acceptable, we were asked by the alt.chi chairs to redact direct reviewer quotes.

Acknowledgements

Thanks to all who took the time to participate in this survey, and to M. Kay, E. Mekler, M. R. Jakobsen, S. Reeves, and A. Tuch for providing early feedback on the survey.


Arthur Mensch

Julien Mairal

Gaël Varoquaux

Bertrand Thirion

Subsampled online matrix factorization with convergence guarantees

We present a matrix factorization algorithm that scales to input matrices that are large in both dimensions (i.e., that contains more than 1TB of data). The algorithm streams the matrix columns while subsampling them, resulting in low complexity per iteration and reasonable memory footprint. In contrast to previous online matrix factorization methods, our approach relies on low-dimensional statistics from past iterates to control the extra variance introduced by subsampling. We present a convergence analysis that guarantees us to reach a stationary point of the problem. Large speed-ups can be obtained compared to previous online algorithms that do not perform subsampling, thanks to the feature redundancy that often exists in high-dimensional settings.

Setup. The goal of matrix factorization is to decompose a matrix X ∈ R p×n -typically n signals of dimension p -as a product of two smaller matrices:

X ≈ DA with D ∈ R p×k , A ∈ R k×n , (1)
with potential sparsity or structure requirements on D and A. We consider a sample stream (x t ) t≥0 that cycles into the columns {x (i) } i of X. Matrix factorization can be formulated as a non-convex optimization problem, where the factor D (the dictionary) minimizes the following empirical risk:

D = argmin D∈C f def = 1 n n i=1 f (i) (D), where f (i) (D) = min α∈R k 1 2 x (i) -Dα 2 2 + λ Ω(α). (2)
C is a column-wise separable convex set of R p×k , and Ω : R p → R is a penalty over the code. The problem of dictionary learning [START_REF] Olshausen | Sparse coding with an overcomplete basis set: A strategy employed by V1?[END_REF][START_REF] Agarwal | Learning sparsely used overcomplete dictionaries[END_REF] sets C = B k 2 and Ω = • 1 . Due to the sparsifying effect of 1 penalty [START_REF] Tibshirani | Regression shrinkage and selection via the lasso[END_REF], the dictionary forms a basis in which the data admit a sparse representation. Setting C = B k 1 and Ω = • 2 2 yields a data-adapted sparse basis, akin to sparse PCA [START_REF] Zou | Sparse principal component analysis[END_REF]. The algorithm presented here accommodates elastic-net penalties Ω(α) (1 -ν) α 2 2 + ν α 1 , and elastic-net ball-constraints C {D ∈ R p×k / d (j) µ d

(j) 1 + (1 -µ) d (j) 2 2 ≤ 1}.
Problem. For many applications of matrix factorization, datasets are growing in both sample number and sample dimension. The online matrix factorization algorithm [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF] can handle large numbers of samples but was designed to work in relatively small dimension. Recent work [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF] has adapted this algorithm to handle very high dimensional dataset. Though it demonstrates good empirical performance, the proposed algorithm yields sequences of iterates with non vanishing variance and is not asymptotically convergent.

Contribution. We address this issue and correct some aspects of the algorithm in [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF] to establish convergence and correctness. We thus introduce a new method to efficient solve (2) for numerous high-dimensional data -large p, large n -with theoretical guarantees.

As in [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF], we perform subsampling at each iteration of the online matrix factorization algorithm. The sample stream is downsampled in a stochastic manner -we observe different subsets of successive colunms. We thus each step of the online algorithm in a space of reduced dimension q < p. Unlike [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF], we control the variance introduced by the subsampling to obtain convergence. For this, we rely on low-dimensional statistics kept from the past, as many recent stochastic algorithms [START_REF] Schmidt | Minimizing finite sums with the stochastic average gradient[END_REF][START_REF] Johnson | Accelerating stochastic gradient descent using predictive variance reduction[END_REF][START_REF] Defazio | Saga: A fast incremental gradient method with support for non-strongly convex composite objectives[END_REF].

Algorithm

Original online algorithm. The problem (2) can be solved online, following [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF]. At each iteration t, a sample x t is drawn from one of the columns {x (i) } 1≤i≤n of X. Its code α t is computed from the previous dictionary D t-1 : α t argmin α∈R p 1 2 x t -D t-1 α 2 2 + λ Ω(α). Then, D t is updated as

D t ∈ argmin D∈C ḡt (D) 1 t t s=1 1 2 x s -Dα s 2 2 + λΩ(α s ) , (3)
In other words, D t is chosen to be the best dictionary that relates past codes (α s ) s≤t to past samples (x t ) s≤t . Codes are not recomputed from the current iterate D, which would be necessary to compute the true past loss fonction ft (D), of which ḡt is a strongly-convex upper-bound:

ft (D) 1 t t s=1 min α∈R p 1 2 x s -Dα 2 2 + λΩ(α) ≤ ḡt (D) (4)
It can be shown [see 5, for theoretical grounding] that minimizing (ḡ t ) t yields a sequence of iterates that is asymptotically a critical point of f defined in [START_REF] Defazio | Saga: A fast incremental gradient method with support for non-strongly convex composite objectives[END_REF]. ḡt can be minimized efficiently by projected block coordinate descent, which makes it useful in practice. Indeed, minimizing ḡt is equivalent to minimizing the quadratic function

D → 1 2 Tr (D D Ct ) -Tr (D B t ), where Bt = 1 t t s=1 x s α s , Ct = 1 t t s=1 α s α s . (5)
Its gradient ∇ḡ t : D → D Ct -Bt can be tracked online by updating Ct and Bt at each iteration:

Ct = (1 - 1 t ) Ct-1 + 1 t α t α t Bt = (1 - 1 t ) Bt-1 + 1 t x t α t . (6)
Those two statistics are thus sufficient to yield the sequence (D t ) t . The weight 1 t used above can be replaced by a more general w t . In addition, the online algorithm has a minibatch extension.

Subsampled algorithm. We adapt the algorithm from [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF] to handle large sample dimension p. The complexity of this algorithm linearly depends on the dimension p in three aspects:

• x t ∈ R p is used to compute the code α t ,
• it is used to update the surrogate parameters Ct ∈ R p×k , • D t ∈ R p×k is fully updated at each iteration. Our new subsampling online matrix factorization algorithm (SOMF) reduces the dimensionality of each of these steps, so that the single-iteration complexity in p depends on q = p r rather than p. r > 1 is a reduction factor that is close to the computational speed-up per iteration in the large dimensional regime p k. Formally, we randomly draw, at iteration t, a mask M t that "selects" a random subset of x t . M t is a R p×p random diagonal matrix, such that each coefficient is a Bernouilli variable with parameter 1 r , normalized to be 1 in expectation. With this definition at hand, M t x t constitutes a non-biased, low-dimensional estimator of x t : E[ M t x t 0 ] = p r = q, and E[M t x t ] = x t , with • 0 counting the number of non-zero coefficients. Thus, r is the average proportion of observed features at each iteration. We further define the pair of orthogonal projectors P t ∈ R q×p and P ⊥ t ∈ R (p-q)×p that projects R p onto Im(M t ) and Ker(M t ), which we will use for the dictionary update step. In brief, SOMF, defined in Alg. 1, follows the outer loop of online matrix factorization, with the following major modifications at iteration t:

• it uses M t x t and low-size statistics instead of x t to estimate the code α t and the surrogate g t ,

• it updates a subset of the dictionary P t D t-1 to reduce the surrogate value ḡt (D). Relevant parameters of ḡt are computed using P t x t and α t only. We describe in detail the new code computation and dictionary update steps. We then state convergence guarantees for SOMF. Those are non trivial to obtain as SOMF is not an exact (stochastic) majorization-minimization algorithm.

Algorithm 1 Subsampled online matrix factorization (SOMF)

Input: Initial iterate D 0 , weight sequences (w t ) t>0 , (γ c ) c>0 , sample set {x (i) } i>0 , # iterations T . for t from 1 to T do Draw x t = x (i) at random and M t (see text) Update the regression parameters for sample i:

c (i) ← c (i) + 1, γ ← γ c (i) (β (i) t , G (i) t ) ← (1-γ)(β (i) t-1 , G (i) t-1 )+γ(D t-1 M t x (i) , D t-1 M t D t-1 ), (β t , G t ) ← ( β(i) t , Ḡ(i) t )
Compute the approximate code for x t : α t ← argmin α∈R k 1 2 α G t αα β t + λ Ω(α). Update the parameters of the aggregated surrogate ḡt :

Ct ← (1 -w t ) Ct + w t α t α t . P t Bt ← (1 -w t )P t Bt + w t P t x t α t . (7)
Compute simultaneously (using (using [7, Alg 2]) for 1st expression):

P t D t ← argmin D r ∈C r 1 2 Tr (D r (D r Ct -Bt )), P ⊥ t Bt ← (1 -w t )P ⊥ t Bt-1 + w t P ⊥ t x t α t . (8)
Output: Final iterate D T .

Code computation. In the online algorithm, α t is obtained solving the linear regression problem

α t = argmin α∈R k 1 2 α G t α -α β t + λΩ(α), where G t = D t-1 D t-1 and β t = D t-1 x t (9)
For large p, computing G t and β t dominates the complexity of the code computation step. To reduce this complexity, we introduce estimators for G t and β t , computable at a cost proportional to q, whose use does not break convergence. Recall that the sample x t is drawn from a finite set of samples {x (i) } i . We estimate G t and β t from M t x t and data from previous iterations s < t for which x (i) was drawn. Namely, we keep in memory 2n estimators, written (G

(i) t , β (i)
t ) 1≤i≤n , observe the sample i = i t at iteration t and use it to update the i-th estimators

Ḡ(i) t , β(i) t following β (i) t = (1 -γ)G (i) t-1 + γD t-1 M t x (i) , G (i) t = (1 -γ)G (i) t-1 + γD t-1 M t D (i) t , (10)
where γ is a weight factor determined by the number of time sample i has been previously observed at time t. Precisely, given (γ c ) c a decreasing sequence of weights, γ γ c (i)

t

, where c

(i) t = |{s ≤ t, x s = x (i) }| All others estimators {G (j) t , β (j) t } j =i are left unchanged from iteration t -1. The set {G (i) t , β (i)
t } 1≤i≤n is used to define the averaged estimators at iteration t, related to sample i: [START_REF] Tibshirani | Regression shrinkage and selection via the lasso[END_REF] where γ 9), α t minimizes the masked loss averaged over the previous iterations where sample i appeared:

G t G (i) t = s≤t,xs=x (i) γ (i) s,t D s-1 M s D s-1 , β t β (i) t = s≤t,xs=x (i) γ (i) s,t D s-1 M s x (i) ,
(i) s,t = γ c (i) t s<t,xs=x (i) (1 -γ c (i) s ). Replacing (G t , β t ) by (G t , β t ) in (
min α∈R k s≤txs=x (i) γ (i) s,t 2 M s (x (i) -D s-1 α) 2 2 + λΩ(α). ( 12
)
The sequences (G t ) t and (β t ) t are consistent estimations of (G t ) t and (β t ) t -consistency arises from the fact that a single sample x (i) is observed with different masks along iterations. This was not the case in the algorithm proposed in [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF], which use estimators that does involve averaging from past data. Solving ( 12) is made closer and closer to solving [START_REF] Richtárik | Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function[END_REF], in a manner that ensures the correctness of the algorithm. Yet, computing the estimators ( 11) is r times as costly as computing G t and β t from ( 9) and permits to speed up the code computation steop close to r times. The weight sequences (w t ) t and (γ c ) c are selected appropriately to ensure convergence. For instance, we can set

w t = 1 t v , γ c = 1 c 2.5-2v , with v ∈ ( 3 4 , 1).
Dictionary update. In the original online algorithm, the whole dictionnary D t-1 is updated at iteration t. To reduce the time complexity of this step, we add a "freezing" constraint to the minimization of the quadratic function [START_REF]Stochastic majorization-minimization algorithms for large-scale optimization[END_REF]. Every row r of D that corresponds to an unseen row r at iteration r (such that M t [r, r] = 0) remains unchanged. D t is thus obtained solving

D t ∈ argmin D∈C P ⊥ t D=P ⊥ t Dt-1 1 2
Tr (D D Ct ) -Tr (D Bt ), with P t orth. projector on Im(M t ) (

With elastic-net ball constraints, solving (13) reduces to performing the partial dictionary update (8) (Alg. 1), with

C r = {D r ∈ R k×q , (d r ) (j) ≤ 1 -d (j) t-1 + P t d (j)
t-1 }. We perform this update using a single pass of projected block coordinate descent with blocks in the reduced space R q . The dictionary update step is thus performed r times faster than the original algorithm.

Surrogate computation

The gradient we use to solve [START_REF] Olshausen | Sparse coding with an overcomplete basis set: A strategy employed by V1?[END_REF] requires to know only Ct and P t Bt . We thus parallelize the partial update of the dictionary and the update of P ⊥ t Bt , using a second thread. The update of P t Bt is performed in the main thread at a cost proportional to q. As the parallel computation is dominated by dictionary update, this is enough to effectively reduce the computation time of Bt computation.

Convergence guarantees All in all, the three steps whose complexity depends on p in the original algorithm now depends on q, which speeds-up a single iteration by a factor close to r. Yet SOMF retain convergence guarantees. We assume that there exists ν such that for all t > 0, D t D t νI (met in practice or by adding a small ridge regularization to (2)), and make a technical data-independent hypothesis on (w t ) t and (γ c ) c decay. Then SOMF iterates converge in the same sense as in the original algorithm [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF]:

D t → D ∞ ∈ R p×k and ∇ f (D ∞ , D -D ∞ ) ≥ 0 for any D ∈ C
, where f is the empirical risk defined in [START_REF] Defazio | Saga: A fast incremental gradient method with support for non-strongly convex composite objectives[END_REF].

Proof sketch. We use the aggregated nature of ḡt and the fact that we can obtain a geometric rate of convergence for a single pass of projected block coordinate descent [e.g see 9] to control the terms D t -D t-1 and ḡt (D t ) -ḡt (D * t ), where D * t = argmin D∈C ḡt . We obtain ḡt (D t ) -ḡt (D t-1 ) = O(w t ), a crucial result on estimate stability. Simultaneously, we show that the partial minimization yields the same result as the full minimization for t → ∞, as θ t -θ t → 0. Using this result, with appropriate selection of (w t ) t and (γ t ) t , the noise induced by the use of estimators in (9) can be bounded in the derivations of [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF]. We then write the difference ( 12) -( 9) as the sum of a lag term and an empirical mean over {M s } xs=xt . Both can be bounded with appropriate selection of weights. Formally, (ḡ t ) t are no longer upper-bounds of ( ft ) t , but become so for t → ∞, at a sufficient rate to guarantee convergence.

Experiments

Hyperspectral images. We benchmark our algorithm by performing dictionary learning on a large hyperspectral image. Dictionary learning is indeed used on patches of hyperspectral images, as in [START_REF] Maggioni | Nonlocal transform-domain filter for volumetric data denoising and reconstruction[END_REF]. Extracting 16×16 patches from an 1GB hyperspectral image from the AVIRIS project with 224 channels yields samples of dimension p = 57, 000. Figure 1 demonstrates that the newly proposed algorithm is faster than the original, non-subsampled algorithm from [START_REF] Mairal | Online learning for matrix factorization and sparse coding[END_REF] by a factor close to r = 4. This speed-up is helped by the redundancy in the different channels of the hyperspectral patches. In the first epochs, the proposed method also outperforms the recent subsampled algorithm from [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF], thanks to the introduction of consistent estimators in the code computation step. All algorithms are implemented in Cython and benched on two cores. They cycle over 100,000 normalized samples with minibatches of size 50. The code for reproduction is available at github.com/arthurmensch/modl..

Conclusion

The new SOMF algorithm can efficiently factorize large and tall matrices. It preserves the speed gains of [START_REF] Mensch | Dictionary learning for massive matrix factorization[END_REF] but has convergence guarantees that are beneficial in practice.

Figure 1

 1 Figure 1 Performing dictionary learning on hyperspectral data (224 channels, 16 × 16 patches) is faster with stochastic subsampling, and even faster with the newly proposed variance control.

30th Conference on Neural Information Processing Systems (NIPS 2016), Barcelona, Spain.

Acknowledgments

The research leading to these results was supported by the ANR (MACARON project, ANR-14-CE23-0003-01 -NiConnect project, ANR-11-BINF-0004NiConnect) and has received funding from the MetaMRI Inria Associate Team.