image part 004

Automated Reasoning

/by

Another area of interest is automated reasoning, i.e., algorithms for proving and disproving mathematical statements. In certain cases, solving reasoning tasks is an end in itself. In other cases, automated reasoning is a tool for establishing that a system is safe or inferring useful facts that can aid learning and program synthesis. In either case, the computational complexity of exploring spaces of proofs and counterexamples is a formidable barrier. As with program synthesis, we approach this challenge by complementing classical automated reasoning techniques with contemporary statistical learning methods.

image part 005

Program Synthesis

/by

Program synthesis is the problem of automatically discovering programs from specifications of their intended functionality. Such specifications can take various forms, including noisy input-output examples, desired program trajectories, behavioral constraints written in first-order or temporal logic, and visual or textual descriptions of the program’s goals. Program synthesis cuts across most of our lab’s research. In some cases, we are motivated by the potential of program synthesis to make programming more productive. In other cases, our goal is to synthesize programs that model, and help us understand better, the real world.

In either case, one faces two basic issues. First, a program synthesizer needs to search through a space of programs that is combinatorial and quickly explodes. Second, specifications are often ambiguous or incomplete, and this means that not all programs that meet the specification are interesting. Over the years, we have developed many approaches to these challenges. For example, some of our methods prune a search space of programs using automated deduction techniques. Others guide a discrete search over programs using learned statistical models. Yet others relax the space of programs into a continuous space that can be explored with scalable gradient-based optimization.

Selected Publications

Sorry, no publications matched your criteria.

image part 006

Probabilistic Programming

/by

Another running theme is probabilistic programming, in which programs are used to represent complex, structured probability distributions. We are especially interested in using such programs to unite logical and probabilistic reasoning and perform complex generative modeling, and for causal inference and discovery. Our research studies a wide variety of technical problems in probabilistic programming, including the design of probabilistic programming languages, the development of methods to infer probabilities, independence relationships, and the effects of interventions and counterfactuals in probabilistic programs, and deriving algorithms for learning the structure and parameters of probabilistic programs.

Selected Publications

Sorry, no publications matched your criteria.

image part 007

Neurosymbolic Programming

/by

A key theme in our research is the use of neurosymbolic programs, i.e., models constructed through the composition of neural networks and traditional symbolic code. The neural modules in such a program facilitate efficient learning, while the symbolic components allow the program to use human domain knowledge and also be human-comprehensible. Our research studies a wide variety of challenges in neurosymbolic programming, including the design of language abstractions that allow neural and symbolic modules to interoperate smoothly, methods for analyzing the safety and performance of neurosymbolic programs, and algorithms for learning the structure and parameters of neurosymbolic programs from data.

Selected Publications

Sorry, no publications matched your criteria.