Withdraw
Loading…
Towards eliminating expert creative help in automated reasoning
Murali, Adithya
Loading…
Permalink
https://hdl.handle.net/2142/127256
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
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…