Teaching Research Writing to Chinese Graduate Students: A Guided Discovery Genre Approach

One of the biggest challenges graduate-level research writing instructors face is how to motivate students in large and multidisciplinary classes effectively. This article explores the influence of a guided inductive and discovery-based genre approach on improving students’ knowledge of research writing. A questionnaire survey was conducted, and some of the students’ written assignments were analyzed. The survey results show that the students were generally satisfied with this approach and affirmed its effectiveness in increasing their knowledge of the textual organization, format and documentation, and language style in research writing. Examining the students’ written analysis of the move structure of abstracts indicates that this approach has enhanced the students’ ability to identify moves and facilitated their acquisition of more appropriate genre knowledge. Further examination of the students’ written reflections reveals a more in-depth understanding of their learning experience. Implications and directions for future research are discussed.

UDF to SQL translation through compositional lazy inductive synthesis

Many data processing systems allow SQL queries that call user-defined functions (UDFs) written in conventional programming languages. While such SQL extensions provide convenience and flexibility to users, queries involving UDFs are not as efficient as their pure SQL counterparts that invoke SQL’s highly-optimized built-in functions. Motivated by this problem, we propose a new technique for translating SQL queries with UDFs to pure SQL expressions. Unlike prior work in this space, our method is not based on syntactic rewrite rules and can handle a much more general class of UDFs. At a high-level, our method is based on counterexample-guided inductive synthesis (CEGIS) but employs a novel compositional strategy that decomposes the synthesis task into simpler sub-problems. However, because there is no universal decomposition strategy that works for all UDFs, we propose a novel lazy inductive synthesis approach that generates a sequence of decompositions that correspond to increasingly harder inductive synthesis problems. Because most realistic UDF-to-SQL translation tasks are amenable to a fine-grained decomposition strategy, our lazy inductive synthesis method scales significantly better than traditional CEGIS. We have implemented our proposed technique in a tool called CLIS for optimizing Spark SQL programs containing Scala UDFs. To evaluate CLIS, we manually study 100 randomly selected UDFs and find that 63 of them can be expressed in pure SQL. Our evaluation on these 63 UDFs shows that CLIS can automatically synthesize equivalent SQL expressions in 92% of the cases and that it can solve 2.4× more benchmarks compared to a baseline that does not use our compositional approach. We also show that CLIS yields an average speed-up of 3.5× for individual UDFs and 1.3× to 3.1× in terms of end-to-end application performance.

Learning Probabilistic Termination Proofs

We present the first machine learning approach to the termination analysis of probabilistic programs. Ranking supermartingales (RSMs) prove that probabilistic programs halt, in expectation, within a finite number of steps. While previously RSMs were directly synthesised from source code, our method learns them from sampled execution traces. We introduce the neural ranking supermartingale: we let a neural network fit an RSM over execution traces and then we verify it over the source code using satisfiability modulo theories (SMT); if the latter step produces a counterexample, we generate from it new sample traces and repeat learning in a counterexample-guided inductive synthesis loop, until the SMT solver confirms the validity of the RSM. The result is thus a sound witness of probabilistic termination. Our learning strategy is agnostic to the source code and its verification counterpart supports the widest range of probabilistic single-loop programs that any existing tool can handle to date. We demonstrate the efficacy of our method over a range of benchmarks that include linear and polynomial programs with discrete, continuous, state-dependent, multi-variate, hierarchical distributions, and distributions with undefined moments.

Decision Tree Learning in CEGIS-Based Termination Analysis

We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.

Constraint-Based Relational Verification

In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses ($$\mathrm {CHCs}$$ CHCs ) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-safety such as generalized non-interference and co-termination.This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called $$\mathrm {pfwCSP}$$ pfwCSP where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over $$\mathrm {CHCs}$$ CHCs permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for $$\mathrm {pfwCSP}$$ pfwCSP based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.

self-paced reading study of language processing and retention comparing guided induction and deductive instruction

The present study measured the effects of guided-inductive (GI) versus deductive computer-delivered instruction on the processing and retention of the Spanish true passive using a self-paced reading design. Fifty-four foreign language learners of Spanish participated in the study, which operationalised guided-inductive and deductive approaches using an adaptation of the PACE model and processing instruction (PI), respectively. Results revealed that each experimental group significantly improved after the pedagogical intervention, and that the GI group outperformed the PI group in terms of accuracy on an immediate post-test. Differences between the groups, however, were not durative; at the delayed post-test, each group performed the same. Additional analyses revealed that the GI group spent over twice as much time on task during instruction than the PI group, with no long-term advantages on processing, calling into question the pedagogical justification for implementing GI at a curricular level.