Towards eliminating expert creative help in automated reasoning

The democratization of automated reasoning is a dream for computer scientists like few others. However, despite many years of progress there continue to exist fundamental obstacles in the way. In this thesis we identify one of the key obstacles: the inescapable need for expert help encountered when using automated reasoning tools or algorithms to prove rich sets of properties. This help takes many forms across the many reasoning frameworks that exist, but we argue that in many widely used frameworks the help is a technical intervention that experts are able to come up with by studying a problem, simply using their experience and creativity. In this work we seek to unravel the nature of this creative technical help and take steps towards eliminating it. Although at first sight the workflow we describe may appear informal or unorganized, our study reveals that it is possible to formally characterize the limits of the reasoning power of various automatic tools and heuristics. Furthermore, we show that the expert help in fact bridges (again in a formal sense) the gap between the limits of the reasoning algorithms and the power needed to prove the properties desired. We dub such gaps in automated reasoning creativity gaps and develop new theoretical tools to formally characterize them. Understanding the role of the expert help in a formal sense allows us to formulate well-defined computational problems to solve in order to bridge creativity gaps. We argue that such problems can be solved effectively using a form of learning we call logic learning in this thesis, which refers to the problem of learning logical formulas from rich example structures/ logical models. We develop new frameworks and algorithms for logic learning and use them to bridge different creativity gaps. In a third part of our work, we apply the lens of thinking about the dynamics between expert help and automation to interrogate design principles for new verification paradigms that can minimize the kind of user frustrations we focus on in this work, namely dealing with the opaqueness of creativity gaps and the inability to provide the required help to bridge the gaps without deep verification expertise. We formulate the problem of designing a predictable verification framework and develop a new framework for verifying heap manipulating programs that offers a predictable verification experience. We believe that the contributions of this work take significant steps towards eliminating creativity gaps in automated reasoning, and in doing so pave the way further for progress towards the democratization of automated reasoning.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Murali, Adithya

Contributors dc:contributor

• Parthasarathy, Madhusudan
• Viswanathan, Mahesh
• Singh, Gagandeep
• Jhala, Ranjit
• Chaudhuri, Swarat

• Automated Verification
• Automated Reasoning
• Logic
• Creativity Gaps
• Logic Learning
• Formula Synthesis
• Learning For Bridging Creativity Gaps
• Data-driven Logic Learning
• Democratizing Verification
• First-order Logic With Recursive Definitions
• First-order Logic With Least Fixpoints
• Completeness
• Functional Programs
• Refinement Types
• Inductive Lemma Synthesis
• Model-guided Synthesis
• Verification Language Design
• Predictable Verification
• Axiom Synthesis
• Axiom Discovery
• Axiom Learning
• Programming Languages
• Verification
• Smt Solvers

Statement dc:rights

• Copyright 2024 Adithya Murali

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/127256

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F127256