Learning symbolic concepts and domain-specific languages

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois Urbana-Champaign

Year dc:date

2025

Author dc:creator

• Krogmeier, Paul M

Contributors dc:contributor

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

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

Statement dc:rights

• Copyright 2025 Paul Krogmeier

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

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