Cloud systems are composed of multiple inter-connected independent subsystems. These systems are complex in nature as they are made of heterogeneous components rife with complicated interactions, operate in dynamic conditions, and exhibit unpredictable behaviors. Developers expend significant manual effort to efficiently design, implement, optimize, operate, and improve these systems throughout the cloud system lifecycle.

This dissertation proposes Human-in-the-loop Specification-Driven Automation (HITLSDA) techniques for reducing the manual effort required by developers for carrying out tasks across the cloud lifecycle. HITLSDA techniques reduce the manual effort by the decoupling the creative component of cloud lifecycle tasks that require human insight from their corresponding mechanical component which can be automated.

We instantiate this HITLSDA approach through two systems targeting different phases of the cloud lifecycle: (i) Blueprint, a toolchain for generating and reconfigurable microservice systems that streamlines exploration of the cloud system design space; and (ii) Iridescent, a framework for online, workload-driven runtime specialization that continuously optimizes system performance by adapting code to observed execution behavior. Together, these systems demonstrate that HITLSDA provides a general and effective paradigm for reducing developer burden in cloud system design, implementation, and optimization while maintaining flexibility and performance.

The remarkable advances in AI have given rise to a growing interest in AI-assisted decision support in domains ranging from medicine and drug-discovery, to criminal justice and education. The ultimate goal in AI-assisted decision support is to optimally combine the complementary strengths of humans and AI models to achieve greater outcomes than either can achieve on their own, in short human-AI complementarity. Achieving this goal, however, has shown to be a major challenge as it typically requires human experts to understand when they can rely on the AI model for their decision—a highly non-trivial task. In this thesis, I show that it is possible to circumvent this challenge and achieve human-AI complementarity under an alternative design of decision support systems. The key innovation in this design lies in adaptively controlling the level of human agency by using an AI model to narrow down the decisions a human can take to a subset. I introduce algorithmic methods to construct as well as optimize these subsets to provably improve performance in decision-making tasks compared to the performance of the AI model used by the system or the human deciding on their own. To empirically evaluate these methods, I conduct two large-scale human subject studies that show that the proposed decision support system leads to human-AI complementarity in practice.

Reinforcement learning (RL) has emerged as a fundamental approach to decision-making in machine learning, with applications across a wide range of real-world domains, and several practical extensions, such as multi-agent RL (MARL) and RL from human feedback (RLHF). Despite the growing successful applications of these systems, there exists an inherent threat when it comes to applying them in the real world, where ill-intentioned third parties may intervene in both their training process and deployment. This typically has catastrophic consequences, where even small and inexpensive perturbations to the environment may cause the system to substantially diverge from the desired behavior. The purpose of this thesis is to provide a thorough investigation of various adversarial attacks and robustness against such attacks to (MA)RL and (MA)RLHF systems. In particular, we study training-time and test-time attacks in MARL and propose algorithms that are shown to be provably robust against such attacks. Beyond MARL, we establish fundamental statistical results for RLHF, provide a rigorous characterization of poisoning attacks to RLHF, and develop robust extensions for MARLHF. Our work is centered around robust algorithmic approaches with provable guarantees under common assumptions.