Learning symbolic concepts and domain-specific languages

Krogmeier, Paul M

Permalink

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

Description

Title

Learning symbolic concepts and domain-specific languages

Author(s)

Krogmeier, Paul M

Issue Date

2025-04-21

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

Parthasarathy, Madhusudan

Doctoral Committee Chair(s)

Parthasarathy, Madhusudan

Committee Member(s)

• Viswanathan, Mahesh
• Singh, Gagandeep
• Solar-Lezama, Armando

Department of Study

Siebel School Comp & Data Sci

Discipline

Computer Science

Degree Granting Institution

University of Illinois Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• symbolic learning
• tree automata
• programming languages
• domain-specific languages
• logic
• synthesis
• axioms

Abstract

Symbolic concept learning is a fundamental problem with numerous applications in program testing, verification, synthesis, and discovery of mathematical theorems and physical laws. We investigate in this dissertation the decidability of symbolic learning in different formal languages and provide new decision procedures for their learning problems. We develop an algorithm based on tree automata that can decide the existence of logic formulas which correctly classify a given set of labeled structures, where formulas come from fragments of finite-variable first-order logics defined by regular constraints on formula syntax trees. We show that alternating tree automata can evaluate quantified logic formulas over finite structures and use this to give an exponential time upper bound for learning. We prove a matching lower bound. We show also that finite-variable logics with recursion have decidable learning by moving to two-way tree automata which evaluate recursive definitions by traversing syntax trees up and down several times. We also prove decidable learning results for finite-variable second-order logics and Datalog programs. Next we show that these learning algorithms generalize to languages beyond finite-variable logics. We prove a meta-theorem which says that learning in a language L is decidable if we can devise a restricted program P which evaluates expressions of L over fixed structures. Provided that P does not need more and more memory for larger and larger expressions, it can be translated with a learning instance into a tree automaton that accepts exactly the set of solutions; this reduces learning problems to the emptiness problem for these tree automata. We use the meta-theorem to prove new decidable learning results by exhibiting evaluation programs for several languages: modal logic and computation tree logic over finite Kripke structures, linear temporal logic over ultimately periodic words, regular expressions and context-free grammars over finite words, first-order logic queries over rational numbers, and text-manipulation programs for spreadsheet automation. We next turn to the problem of synthesizing domain-specific languages (DSLs) which succinctly express symbolic concepts in specific domains and thereby enable learning from few examples. We formulate novel DSL synthesis problems involving the synthesis of grammars with and without macros, and we prove decidability results for each. Finally, we formulate an axiom synthesis problem in which the goal is to synthesize a set of logic formulas which precisely characterize a target class of mathematical structures. We propose a general learning-based algorithmic framework for solving axiom synthesis and instantiate it to synthesize axiomatizations in modal logic and Kleene algebra.

Graduation Semester

2025-05

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2025 Paul Krogmeier

Owning Collections