From finance and healthcare to criminal justice and transportation, many domains that involve high-stakes decisions, traditionally made by humans, are increasingly integrating artificial intelligence (AI) systems into their decision making pipelines. While recent advances in machine learning and optimization have given rise to AI systems with unprecedented capabilities, fully automating such decisions is often undesirable. Instead, a promising direction lies in AI-assisted decision making, where AI informs or complements human decisions without completely removing human oversight. In this talk, I will present my PhD work on AI-assisted decision making in settings where humans rely on two core cognitive capabilities: strategic reasoning and counterfactual reasoning. First, I will introduce game-theoretic methods for supporting policy design in strategic environments, enabling a decision maker to allocate resources (e.g., loans) to individuals who adapt their behavior in response to transparency regarding the decision policy. Next, I will present methods to enhance a decision maker’s counterfactual reasoning process— identifying key past decisions (e.g., in clinical treatments) which, if changed, could have improved outcomes and, hence, serve as valuable learning signals. Finally, I will discuss a computational model of how people attribute responsibility between humans and AI systems in collaborative settings, such as semi-autonomous driving, evaluated through a human subject study. I will conclude with key takeaways and future directions for designing AI systems that effectively support and interact with humans.

Linear recurrence sequences (LRS) are among the most fundamental and easily definable classes of number sequences, encompassing many classical sequences such as polynomials, powers of two, and the Fibonacci numbers. They also describe the dynamics of iterated linear maps and arise naturally in numerous contexts within computer science, mathematics, and other quantitive sciences. However, despite their simplicity, many easy-to-state decision problems for LRS have stubbornly remained open for decades despite considerable and sustained attention. Chief among these are the Skolem problem and the Positivity problem, which ask to determine, for a given LRS, whether it contains a zero term and whether it contains only positive terms, respectively. For both problems, decidability is currently open, i.e., whether they are algorithmically solvable.

In this thesis, we present the following results. For the Skolem problem, we introduce an algorithm for simple LRS whose correctness is unconditional but whose termination relies on two classical, widely-believed number-theoretic conjectures. This algorithm is implementable in practice, and we report on experimental results. For the Positivity problem, we introduce the notion of reversible LRS, which enables us to carve out a large decidable class of sequences. We also examine various expansions of classical logics by predicates obtained from LRS. In particular, we study expansions of monadic second-order logic of the natural numbers with order and present major advances over the seminal results of Büchi, Elgot, and Rabin from the early 1960s. Finally, we investigate fragments of Presburger arithmetic, where, among others, we establish the decidability of the existential fragment of Presburger arithmetic expanded with powers of 2 and 3.

From LLMs Algorithmic ranking systems shape online interactions and are linked to engagement misinformation and polarization. This talk explores the unintended consequences of popularity-based rankings drawing on two studies that combine observational data mathematical modeling and experimental validation. The first examines how engagement-driven algorithms may fuel polarization and ideological extremism. The second reveals a "few-get-richer" effect where ranking dynamics amplify minority signals. Together these insights highlight the societal impact of human-AI feedback loops.

•Ranking for engagement: How social media algorithms fuel misinformation and polarization. F Germano V Gómez F Sobbrio. CESifo Working Paper •The few-get-richer: a surprising consequence of popularity-based rankings. F Germano V Gómez GL MensThe Web Conference WWW' 19

As we shall see, LLMs like GPT4 can model group behavior — or stereotypical patterns — fairly well, but their performance drops when it comes to smaller groups, below a certain threshold. This limitation has interesting implications not just for personalization systems, but also for questions in social science, including how we define culture, interpret collective behavior, and think about individual agency.

Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a multitude of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, before my thesis work, none of the tools produced foundational proofs (machine-checkable with a small trusted computing base), and all of them were restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points: either indirectly through libraries, which are often implemented with unsafe code, or directly, which is particularly common for low-level systems code.

With my thesis, I will present work on RefinedRust, a foundational verification tool, aiming to semi-automatically establish functional correctness of both safe and unsafe Rust code. RefinedRust builds a refinement type system for Rust that extends Rust's type system for safe Rust to functional correctness reasoning and unsafe Rust, and, inspired by previous work on RefinedC, automates proofs in this type system inside the Rocq Prover. RefinedRust's type system is semantically proven sound using the Iris separation logic framework, providing high assurances about its correctness. In the process, RefinedRust significantly advances the state of the art of semantic soundness proofs for Rust, scaling previous work on RustBelt to a much more practical and realistic model.

One particularly interesting application for RefinedRust is low-level systems code, which is inherently unsafe and deserving of high-assurance foundational verification. In my thesis, I will present work on verifying interesting parts of the ACE security monitor, which is part of the ACE trusted execution environment (TEE) developed by IBM Research and thus a low-level security-critical component. For the final part of my thesis, I propose to work on one of two projects that will advance our capabilities in verifying systems code like ACE. I will either show how to extend RefinedRust to prove non-interference (a security property) of systems code, or show how to link up RefinedRust with hardware models to prove a fundamental isolation property that ACE should guarantee.

There is growing awareness that the statistical analysis of personal data, such as individual mobility, financial, and health data, could be of immense benefit to society. However, liberal societies have refrained from such analysis, arguably due to the lack of trusted analytics platforms that scale to billions of records and reliably prevent the leakage and misuse of personal data. The first part of this proposal presents CoVault, an analytics platform that leverages secure multi-party computation (MPC) and trusted execution environments (TEEs) to perform analytics securely at scale. CoVault co-locates MPC's independent parties in the same datacenter, providing high bisection bandwidth without reducing security, allowing analytics to scale horizontally to the datacenter’s available resources. CoVault's empirical evaluation shows that nation-scale, secure analytics is feasible with modest resources. For example, country-scale epidemic analytics on a continuous basis requires only one pair of CPU cores for every 30,000 people. The second part of the proposal discusses how to add support for semantic queries to CoVault by building on secure similarity search on high-dimensional vector embeddings.