Colloquia and Seminars

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

Optical imaging of biological tissues at depth presents a significant challenge due to strong light scattering within the tissue, which distorts the wavefront and limits the ability to focus light deep inside the sample. One of the main strategies to address this issue is wavefront shaping (WFS), a powerful technique for deep tissue imaging that physically corrects scattering aberrations to maximize the signal-to-noise ratio. However, its practical utility is severely limited by a highly localized correction field. Current efforts to extend the field of view (FoV) rely on the optical memory effect to tile local corrections, but this two-dimensional approximation degrades rapidly in thick, heterogeneous tissue. In this thesis, we investigate algorithms that could allow WFS corrections to apply to a larger tissue volume. We present a comprehensive roadmap for extended FoV WFS by formulating it as a sparse Transmission Matrix (TM) interpolation problem. Using a rigorous synthetic dataset of 3D tissue structures, we systematically benchmark computational approaches ranging from physical multi-scattering inversions (diffraction tomography) to physics-informed deep learning. We demonstrate that transitioning from 2D memory effects to any 3D volumetric prior yields significant performance gains. Furthermore, we reveal a critical ”generalization gap” in deep wavefront shaping. While physics-informed networks effectively learn visually plausible 3D tissue structures to stabilize TM interpolation in highly scattering regimes, their inductive bias fundamentally struggles to estimate the pseudo-random, high-frequency speckle patterns required for accurate optical phase reconstruction. By characterizing this bottleneck between structural regularization and phase fidelity, our benchmark establishes the necessity of hybrid neuro-physical architectures for generalized deep tissue imaging.

MSc student under the supervision of Prof. Anat Levin.

People generate rich signals as they communicate, search, review, and transact. My research asks how such signals can be harnessed to connect users with the right information, products, and decisions. In the enterprise, I study how social signals can reveal informal knowledge networks in large organizations. On the web, my work explores how people express and pursue information needs through text, voice, and visual queries, and how product knowledge can be extracted and structured at marketplace scale. My current focus is on trustworthy AI for personalized information access. To illustrate this agenda, the talk will present recent work addressing the challenge of training machine learning models when ground-truth labels are delayed by weeks or months in a non-stationary, adversarial environment. This setting creates a fundamental tension between learning from fresh but incomplete feedback and relying on older, more reliable labels that may no longer reflect the current environment. I will show how we formalize these tradeoffs, develop methods to address them, and demonstrate measurable gains through both offline experiments and online A/B tests on live user traffic.

Bio: Ido Guy is a Senior Research Science Manager at Meta and an Adjunct Full Professor at Ben-Gurion University's Institute for Applied AI Research. His research focuses on information retrieval, recommender systems, personalization, and applied AI. Before Meta, he was Chief Scientist and Applied Research Director at eBay Israel, where he established and led four applied science teams in AI for e-commerce. Earlier, he was a Principal Researcher at Yahoo Labs and an STSM/Manager at IBM Research, where he founded and managed the Social Technologies group. Ido has authored over 100 publications and holds 20 granted patents. His work has received multiple best paper and honorable mention awards, an IBM Corporate Award, and the AI-2000 distinction as a top-100 scholar in information retrieval and recommender systems. He currently serves as Program Co-Chair of the ACM Web Conference 2026 and has been a member of the ACM RecSys Steering Committee since 2012.

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.

High-performance computing software must be ported among serial C++, OpenMP, and CUDA as platforms and deployment constraints change. Such translation requires preserving program behavior while satisfying target-specific constraints on parallel execution, synchronization, memory movement, and API use. Although large language models are flexible code generators, plausible parallel-code translations can fail at compilation, execution, or validation.

We study guidance and adaptation methods that make existing LLMs more reliable without training a generator from scratch. The central method is latent PRM guidance, which guides a frozen latent-reasoning model before code is emitted. A small process reward model scores alternative continuous hidden-state branches during latent reasoning and selects branches expected to lead to executable, behaviorally correct programs. The evaluation also includes lighter-weight assistance methods such as prompting, fine-tuning, and iterative repair with compiler and execution feedback.

On the ParaTrans dataset, LLMs struggle as standalone executable translators, but their reliability improves significantly through task-aware assistance. Latent PRM guidance improves validation over unguided latent reasoning while remaining compatible with iterative repair. The best results are achieved through the cumulative and compounding effects of combining guidance, prompting, and iterative repair to improve executable correctness and validation performance.