Colloquia and Seminars

Real-world deployment of deep learning violates the assumptions of i.i.d. training data and aggregate-metric evaluation: observations are dependent in time, space, and across users; decision latency is bounded by milliseconds; and the cost of a wrong prediction is rarely symmetric. My doctoral research argues that the structural priors hardest for a deep network to recover from data are precisely the ones that should be encoded into its architecture. The position can be stated in one line: what I cannot afford to learn, I encode.

The eleven papers in the dissertation span communication systems, physiological monitoring, physics-informed learning, clinical decision support, and large language models. Across them I make three claims. First, architectural priors generalize when they match the structure of the data: the dissertation traces a continuum from priors in the problem formulation, to priors in features and representations, to priors in the architecture, to priors that are the governing equation. Second, this claim is Pareto rather than monotone: aligned priors dominate where parameters are scarce and are dominated where they are not, a scope condition anchored at a clean empirical crossover in the language-model chapters. Third, aggregate metrics are the wrong audit: calibrated diagnostics (matched effective sample size, effective residual-stream depth, the shuffle gap, cost-conditional thresholds) repeatedly reorder conclusions drawn from AUC, perplexity, and fixed-length comparisons.

The seminar develops the first claim through three case studies, one at each depth of the continuum: AARL, a DRL scheduler for 5G millimeter-wave networks (prior in the problem formulation); Lab to Wrist, a neural-ODE and neural-Kalman framework that embeds cardiovascular physics architecturally for heart-rate and oxygen-consumption prediction on wearables (prior in the architecture); and a differentiable Randers-Finsler eikonal solver applied to cross-scene wildfire propagation (prior is the governing PDE itself)

Paul Erdős was a Hungarian mathematician with a remarkable talent for formulating challenging open problems across many areas of mathematics. Several of these problems have recently been resolved either with the assistance of AI systems or, in some cases, through work carried out independently by such models.
 
I will discuss a number of examples, with particular emphasis on the recent solution of the Unit Distance Problem by an internal model of OpenAI. This problem has long been regarded as one of the central open questions in discrete geometry and was among Erdős’s favorite problems.
 
Motivated by these developments, I will also speculate on the future capabilities of AI models and their expected impact on mathematical research.
 
The technical aspects of the lecture will be kept light, and no substantial mathematical background will be assumed

DAG-based Byzantine Fault Tolerant (BFT) protocols provide high-throughput consensus under partial synchrony, but existing DAG protocols still require at least a three-message delay to commit decisions. 
In contrast, existing Fast-Path BFT protocols can achieve optimal termination with a two-message delay under favorable conditions, though they do not naturally extend to DAGs.

In this seminar we present FinWhale, the first DAG-based BFT protocol with a two-message delay fast path. 
FinWhale extends the Mysticeti protocol with a novel fast-path commit mechanism that safely coexists with the protocol’s original slow-path rules. 
To preserve safety across different local DAG views, we introduce new commit structures based on fast-path evidence blocks that enable validators to combine fast-path and slow-path reasoning consistently.

FinWhale operates in the partially synchronous model with $n=3f+2p-1$ validators; this matches the known lower-bound for fast Byzantine consensus. 
The protocol tolerates up to $f$ Byzantine faults and achieves fast termination whenever at most $p$ validators fail during the fast path ($1 \leq p\leq f$).
Our results show that optimal-latency fast paths can be integrated into uncertified DAG consensus protocols.

The diversity of workloads, performance metrics, and potential system optimizations makes designing an optimal caching middleware a daunting task. For example, cache replacement policies can exhibit widely varying hit ratios depending on workload characteristics and cache sizes. Moreover, the choice of cache replacement policy may impact the computational complexity and meta-data size required for cache management, which may also be impacted by the internal cache organization (e.g., fully associative vs. k-way) and supporting data structures. Consequently, state-of-the-art caching libraries are still hand-crafted by experts and carefully tuned to narrow workload classes and design goals. Adapting a cache to a new setting, or improving it as a robust general-purpose solution, still requires a labor-intensive redesign process that does not scale to the diversity of modern workloads and deployment constraints. We present Evolve, an agentic framework for automatically improving caching middleware implementations.

Starting from an existing design, Evolve searches for superior variants under two regimes: refinement over a fixed workload suite, and workload specialization against a deployment-specific trace distribution. Each cycle proposes a cohort of LLM-implemented variants, validates them through deterministic correctness gates, scores survivors on a multi-dimensional plugin-based fitness vector, retains a Pareto front under a held-out trace suite to control for overfitting.

The framework also stores LLM-generated insights in a knowledge ledger that supports cross-iteration learning and guides future exploration. As a case study, we apply Evolve on a Dash-inspired associative cache, run it across diverse traces in both regimes, and characterize the variants it produces along each chosen fitness dimension.

Constrained Horn Clauses (CHCs) have emerged as a powerful framework for formal verification, enabling reasoning about program safety, invariant synthesis, model checking, and related verification tasks. Their combination of logical expressiveness and algorithmic solvability has made CHCs a central foundation for modern verification techniques. However, despite significant advances in CHC solving, reasoning about low-level bit-precise program semantics remains a major challenge for existing solvers.

Traditionally, a set of CHCs is encoded with respect to a single background theory. In the context of bit-precise verification, program semantics can naturally be encoded as CHCs modulo the theory of fixed-size bit-vectors. Alternatively, bit-precise semantics can be encoded using integer arithmetic by modeling modular and bit-wise behavior through arithmetic constraints. However, neither approach consistently yields an efficient verification procedure: reasoning directly in the bit-vector theory often limits the scalability and generalization capabilities of CHC solvers, whereas arithmetic encodings produce complex constraints that are expensive to process, especially in the presence of bit-wise operations.

To address this limitation, I will present a novel theory-modular framework for CHC satisfiability that enables coordinated reasoning across multiple background theories. The framework decomposes a CHC system into complementary fragments interpreted over different background theories and coordinates reasoning between them through sound cross-theory transformations. This modular approach combines efficient arithmetic reasoning with precise handling of bit-level operations, leveraging the strengths of both theories within a unified CHC-solving framework.

I will describe the theoretical foundations of the approach, including theory transformations, modular CHC encodings, and a satisfiability procedure for coordinated reasoning across theories. I will also present experimental results on bit-manipulating verification benchmarks, demonstrating substantial improvements over monolithic single-theory approaches. Finally, I will discuss how theory-modular reasoning can contribute to future directions in scalable and expressive CHC solving.