Publication Type

PhD Dissertation

Version

publishedVersion

Publication Date

3-2026

Abstract

Artificial Intelligence (AI) has transformed the software landscape, ushering in a new era of intelligent systems that increasingly shape our daily lives. This transformation is evident in various domains, including Software Engineering (SE), where Large Language Models (LLMs) support many development tools, and control systems, where self-driving cars and autonomous drones rely on deep learning models for real-time decision-making. These AI systems are collectively referred to as AI software, with the former categorized as AI4SE software (AI for Software Engineering) and the latter as AI4Control software (AI for Control). As AI software becomes central to modern computing infrastructure, its reliability issues (e.g., bugs, vulnerabilities) and performance bottlenecks (e.g., excessive memory usage, high latency) can lead to severe consequences, ranging from degraded user experience and significant economic and environmental costs to safety violations and system crashes. We refer to these concerns as the emerging AI software crisis, focusing on two dimensions: Efficiency, where large AI models introduce prohibitive latency, and Safety, where opaque neural networks can lead to unpredictable decisions in mission-critical applications.

Addressing this crisis requires a paradigm shift away from traditional monolithic design principles. This dissertation advocates an automated synthesis-guided approach to AI software development and maintenance, grounded in the insight that many challenges in modern AI software can be reframed as the generation of software artifacts, including hyperparameters, configurations, and programs, that must satisfy correctness constraints, safety specifications, or efficiency objectives. Under this framing, search-based synthesis serves as the unifying methodology, systematically exploring structured design spaces to produce artifacts with formal guarantees or explicitly specified performance objectives. This dissertation presents five technical contributions that apply this approach across both the AI4SE and AI4Control domains, complemented by a comprehensive literature review that establishes the research context.

We first conduct a comprehensive literature review on AI4SE software, focusing on LLMs and their applications in software engineering, alongside an overview of AI4Control software. We analyze aspects of AI4SE software requiring further optimization—energy consumption, latency, and environmental impact—and survey key studies on the safety of neural controllers in control systems.

We then introduce three techniques to optimize AI4SE software, each leveraging a distinct synthesis paradigm. Compressor employs genetic algorithm-based hyperparameter synthesis to compress code LLMs into compact variants as small as 3 MB (over 99% size reduction), with only 1.67% effectiveness loss. Avatar formulates model compression and greening as a multi-objective configuration synthesis problem, using an SMT solver with a tailored optimization algorithm to produce Pareto-optimal student model configurations, achieving up to 160× smaller and 184× more energy-efficient models with negligible accuracy degradation. Ditto integrates model compression with synthesis-guided compilation-time optimization: it quantizes parameters to low-bit-width codebook representations while synthesizing optimized inference programs, and introduces an LLVM pass that replaces unoptimized GEMV loops with BLAS kernels, achieving up to 10.5× faster inference and 6.4× lower memory usage with only 0.27% accuracy loss.

We further introduce two techniques to fortify AI4Control software. As the fourth technical contribution, Synthify leverages evolution strategy-based synthesis to generate proxy programs that approximate neural controller behavior, enabling falsification-based safety violation detection. It outperforms state-of-the-art baselines by 83.5% in detecting safety violations with a 12.8× speedup, while covering 137.3% more sub-specifications in conjunctive safety properties. As the fifth, Aegis synthesizes efficient and permissive programmatic runtime shields that intercept unsafe neural controller behaviors in real time, achieving 2.2× lower runtime overhead, 1.5× higher permissiveness, and 3.0× faster synthesis time compared to baselines.

Together, these contributions demonstrate program synthesis as a general-purpose methodology for optimizing and fortifying AI software. By automatically generating model hyperparameters, configurations, proxy programs, and runtime shields, this dissertation shows how synthesis can support the development of efficient, safe, and deployable AI systems, paving the way toward trustworthy AI software by design.

Degree Awarded

PhD in Computer Science

Discipline

Artificial Intelligence and Robotics | Software Engineering

Supervisor(s)

LO, David

First Page

1

Last Page

271

Publisher

Singapore Management University

City or Country

Singapore

Copyright Owner and License

Author

Download

Share

COinS