Future Reasoning Aws Albarghouthi
March 2018
We are rushing headlong into a future where every inch of our world is swallowed by complex software.
It is thus imperative that we be able
to
reason about sophisticated program behavior and construct well-behaved programs.
E.g.:
-
How do we ensure that decision-making programs do not
discriminate against individuals or groups of people?
- How do ensure that data mining programs do not leak sensitive personal data, like medical records and web-search history?
- How do we ensure that robotic agents seamlessly integrate into our environment and follow our social and cultural norms?
My research focuses on designing
next-generation program verification and synthesis technologies to answer the above questions as well as others.
Fairness in algorithmic decision-making
More and more of our critical decisions are being delegated to software.
With the range and sensitivity of algorithmic decisions expanding by the day, the question of whether an algorithm is fair is a pressing one.
Consider, for instance, unfairness in job applications, welfare allocation, loans, etc. The possibilities for discrimination are only expanding, and, in the near future, we might even be talking about bias and discrimination in robots interacting with humans.
In the FairSquare project, we are exploring algorithmic techniques for
(a)
verifying fairness of decision-making programs,
(b)
synthesizing fair programs, and (c) automatically explaining
behavior of decision-making programs.
Privacy-preserving algorithms
Data is the new oil, and data mining is a threat to individual privacy.
To ensure that an individual's details are not leaked through data analysis, differential privacy has emerged as a popular formulation of privacy where random noise is added to analysis results.
Differentially private algorithms have been implemented
by the US Census Bureau, Apple, Google, Uber, amongst others.
In this project, we are advancing verification and synthesis technology to
(a)
verify correctness of differentially-private algorithms,
(b) verify the accuracy of these algorithms,
and, ultimately, (c) synthesize them automatically.
Program synthesis for data analysis
Over the past decade, we have witnessed a transformational rise in distributed computing platforms that allowed us to seamlessly harness the power of cloud computing infrastructure for large-scale data analysis. In the BIGλ project,
we are asking whether we can democratize cloud computing infrastructure,
such that end users with no programming skills can use it.
To do so, we are exploring how to automatically synthesize data-analysis programs from simple examples. Our work has been exploring
MapReduce programs,
Datalog programs, and recently we have started exploring synthesis in the context of differential privacy constraints—as described above.
Human–robot interactions
In the near future, it is highly likely that robotic agents will transform our world, be it in the workplace, in public spaces, or at home.
How can we program robots to seamlessly blend into our environment?
In this forward-looking project, we are developing programming technologies (languages, analyzers, and IDEs) that are aware of social norms.
Picture a designer programming a human–robot interaction;
the
IDE would interactively inform them of potential violations of social norms, e.g., the robot coming too close to a human's personal space, or the robot rudely interrupting the human, etc.
This way, designers are more aware of the impact of their designs
in the environment and can tailor them to be more socially aware.
The cross-cutting project connects verification technology with research in human–computer interaction and psychology.
Deep-learning-augmented development
The rise of deep learning has inspired the use
of machine learning in an ever-expanding range of tasks.
In this project, we are using
deep learning to rethink various programming technologies.
For example, we have been exploring the use of
deep learning
to improve the precision of static program analyses,
as well as to automatically synthesize programs from natural-language descriptions.