We present a new approach, called meta-meta classification, to learning in small-data settings. In this approach, one uses a large set of learning problems to design an ensemble of learners, where each learner has high bias and low variance and is skilled at solving a specific type of learning problem. The meta-meta classifier learns how to examine a given learning problem and combine the various learners to solve the problem. The meta-meta learning approach is especially suited to solving few-shot learning tasks, as it is easier to learn to classify a new learning problem with little data than it is to apply a learning algorithm to a small data set. We evaluate the approach on a one-shot, one-class-versus-all classification task and show that it is able to outperform traditional meta-learning as well as ensembling approaches.

State-of-the-art neural models of source code tend to be evaluated on the generation of individual expressions and lines of code, and commonly fail on long-horizon tasks such as the generation of entire method bodies. We propose to address this deficiency using weak supervision from a static program analyzer. Our neurosymbolic method allows a deep generative model to symbolically compute, using calls to a static analysis tool, long-distance semantic relationships in the code that it has already generated. During training, the model observes these relationships and learns to generate programs conditioned on them. We apply our approach to the problem of generating entire Java methods given the remainder of the class that contains the method. Our experiments show that the approach substantially outperforms a state-of-the-art transformer and a model that explicitly tries to learn program semantics on this task, both in terms of producing programs free of basic semantic errors and in terms of syntactically matching the ground truth.

We present a neurosymbolic framework for the lifelong learning of algorithmic tasks that mix perception and procedural reasoning. Reusing high-level concepts across domains and learning complex procedures are key challenges in lifelong learning. We show that a program synthesis approach that combines gradient descent with combinatorial search over programs can be a more effective response to these challenges than purely neural methods. Our framework, called HOUDINI, represents neural networks as strongly typed, differentiable functional programs that use symbolic higher-order combinators to compose a library of neural functions. Our learning algorithm consists of: (1) a symbolic program synthesizer that performs a type-directed search over parameterized programs, and decides on the library functions to reuse, and the architectures to combine them, while learning a sequence of tasks; and (2) a neural module that trains these programs using stochastic gradient descent. We evaluate HOUDINI on three benchmarks that combine perception with the algorithmic tasks of counting, summing, and shortest-path computation. Our experiments show that HOUDINI transfers high-level concepts more effectively than traditional transfer learning and progressive neural networks, and that the typed representation of networks significantly accelerates the search.

Abstract In the correct-by-construction programming methodology, programs are incrementally derived from their formal specifications, by repeatedly applying transformations to partially derived programs. At an intermediate stage in a derivation, users may have to make certain assumptions to proceed further. To ensure that the assumptions hold true at that point in the program, certain other assumptions may need to be introduced upstream as loop invariants or preconditions. Typically these other assumptions are made in an ad hoc fashion and may result in unnecessary rework, or worse, complete exclusion of some of the alternative solutions. In this work, we present rules for propagating assumptions through annotated programs. We show how these rules can be integrated in a top-down derivation methodology to provide a systematic approach for propagating the assumptions, materializing them with executable statements at a place different from the place of introduction, and strengthening of loop invariants with minimal additional proof efforts.

Existing attempts towards including formal methods in introductory programming courses focus on introducing program verification tools. When using the verification tools, there is no structured help available to the students in the actual task of implementing the program, except for the hints provided by the failed proof obligations. In contrast, in the correct-by-construction programming methodology, programs are incrementally derived from their specifications. By restricting our attention to program derivation, we have identifed a small core of the formal method concepts that can easily be taught in the first two years of a computing curricula. Based on our learning from multiple years of paper and pencil based teaching, we have developed a programming assistant tool that addresses several of the issues faced by the students in the manual program derivation. The tool ensures that the most common students' error of performing incorrect proofs does not happen.