Towards eliminating expert creative help in automated reasoning

Murali, Adithya

Permalink

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

Description

Title

Towards eliminating expert creative help in automated reasoning

Author(s)

Murali, Adithya

Issue Date

2024-12-03

Director of Research (if dissertation) or Advisor (if thesis)

Parthasarathy, Madhusudan

Doctoral Committee Chair(s)

Parthasarathy, Madhusudan

Committee Member(s)

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

Department of Study

Siebel School Comp & Data Sci

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• 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

Abstract

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.

Graduation Semester

2024-12

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2024 Adithya Murali

Owning Collections