Colloquia and Seminars

Cancer treatment often fails due to acquired resistance. Evidence suggests that adaptive protocols may outperform standard protocols in delaying resistance. However, current adaptive strategies primarily focus on preventing resistant mutant takeover, while overlooking adaptive mechanisms of resistance — feedback and bypass pathways that reestablish the tumor’s pathological set-points. Instead of searching for drug combinations that exhaust the redundant pathways, we ask a different question: assuming we are limited to treatments the physiology can adapt to, is there still a way to eliminate the tumor by precisely timing treatment? We formulated this challenge using dynamical systems theory, and utilized optimal control to reveal dosing strategies capable of eliminating the tumor despite adaptation. We found that treatments failing in a constant regime can become effective when timed appropriately. The resulting strategies are surprising — examples include induction of resonance in tissues or applying a preliminary drug with the opposite of the intended effect. Finally, we show how to use our strategies to simultaneously overcome both mutational and adaptive resistance. Our work establishes a conceptual framework as well as practical strategies for overcoming the main modes of resistance, relevant across a wide range of cancers and therapeutic modalities.

Inspecting code changes in source-control commits is an important task for developers. Professional best practice is to maintain a “compiling-commit” policy, where each commit is buildable. In practice, a single change can introduce cascading changes that must be committed together to keep the project compiling. Such commits are unwieldy to navigate and laborintensive to understand, especially in the commonly used line diff tools that present them as deletions from the old version and additions to the new version. We present Diffmagic, a new algorithm and interface that leverages the compiling-commit policy to organize diffs according to causality. Since commits must remain buildable, changes to a definition lead to changes to its uses, forming a causal structure that Diffmagic uses to find change batches, i.e., changes with a shared root cause. Diffmagic uses semantic information from running just the compiler’s front-end, on only the changed files (i.e., it requires neither full compilation nor whole-project analysis) to recover these use-definition  connections that imply the causality. Within each change batch, Diffmagic assigns a causality score to prioritize changes that are likely to trigger other downstream changes. A user study with 14 participants performing two tasks on realworld commits suggests that Diffmagic makes diffs easier to understand and helps users complete diff inspection tasks faster.

Causal inference is increasingly used in high-stakes domains to support decision-making and policy design. However, causal conclusions may be sensitive to the composition of the observed data, raising an important question: could a small number of additional, plausible observations substantially change the estimated causal effect? Answering this question is essential for assessing the robustness of causal conclusions and identifying underrepresented subpopulations whose inclusion could meaningfully affect the estimates, thereby guiding future data collection. In this work, we introduce the problem of causal effect steering via synthetic data augmentation: given a user-defined target range, identify a minimal-size set of realistic synthetic tuples whose addition shifts the estimated effect into that range. By searching for small augmentations that induce substantial changes in the estimated effect, this approach provides a systematic way to probe the sensitivity of causal conclusions to plausible changes in the observed population. To this end, we present CURATE, a framework for causal sensitivity analysis through synthetic data augmentation. CURATE leverages recent advances in synthetic tabular data generation and adapts a top-performing diffusion model to generate realistic candidate tuples. It then employs a heuristic search method to identify small augmentations that steer the estimated causal effect toward the target range. Experiments on six real-world datasets demonstrate that CURATE efficiently identifies small, realistic data augmentations that reveal the robustness of causal conclusions and expose influential underrepresented populations.

AI is driving unprecedented growth in data center compute, with the market projected to approach $2 trillion by 2030 and revenue growth averaging approximately 24% annually from 2025 to 2030. As AI adoption progresses from infrastructure and physical systems to scientific discovery, it is creating a major opportunity for verification and in particular formal verification - the crown of design. Natural-language interfaces and AI-driven productivity are introducing a new level of abstraction, while emerging examples of AI-assisted mathematical reasoning demonstrate the potential to extend scientific and engineering capabilities.

This keynote traces the evolution from the man–machine communication vision presented at DAC 1964, through collective intelligence and human-in-the-loop formal methods presented at JUG 2013, to today’s agentic verification workflows in Cadence ChipStack. These workflows combine specialized formal agents, proof engines, machine learning, and expert guidance to address properties that remain difficult to prove manually. By interleaving design and verification, and using platforms such as Cadence ChipStack, the Formal Verification AI Flywheel can transform productivity at scale into greater proof power, enabling engineers to build increasingly complex systems with higher confidence and much less manual effort.

Short bio:  Ziyad Hanna is a Corporate Vice President at Cadence Design Systems and R&D General Manager of Cadence Israel. He leads system verification products and Cadence-wide AI initiatives for autonomous chip-design development. Previously, he served as Senior Vice President of Jasper and senior PE and management roles at Intel, where he developed three generations of formal-verification suites widely deployed since the start of Pentium. Hanna earned degrees from Tel Aviv University and a PhD from Oxford University, where he is a visiting professor. An IEEE Senior Member, he has published over 30 articles, 20 patents, and delivered hundreds of industrial and academic presentations and talks. His honors include Intel IAA awards and an honorary doctorate from Ruppin Collage. Ziyad initiated a formal-verification course at the Technion that attracts hundreds of students interested in pursuing advanced studies in the field.

Mechanistic interpretability (MI) enables monitoring and steering LLMs by
operating on their internal state during inference. MI applications
remain difficult to develop, expensive to execute, and challenging to manage
at runtime.

We present xMIx, a system that integrates MI applications as
first-class components of LLM serving, enabling simplified development,
efficient execution, and flexible deployment. Guided by a comprehensive
analysis of modern MI applications, xMIx streamlines the MI apps
development via a simple Python-based Domain Specific Language (DSL) for
accessing intra- and inter-layer runtime model state at well-defined trigger
points during inference. xMIx enables efficient access to ephemeral attention
scores via a novel FlashInspect kernel that retains the performance benefits of
FlashAttention.

xMIx's compiler integrates multiple MI applications into the performance-optimized inference execution flow while ensuring conflict-free coexistence. xMIx's
runtime supports dynamic, per-request activation and deactivation of MI apps
without service interruption or performance degradation when inactive,
leveraging xMIx' dynamic memory management and CUDA graph-compatible
execution.

We integrate xMIx with vLLM and evaluate ten MI apps, including sparse
autoencoders, steering, and jailbreak detection, across four
state-of-the-art LLMs. xMIx incurs negligible execution overhead, up to two
orders of magnitude lower than existing frameworks, while enabling per-request
activation and deactivation up to 1,000 times faster than alternatives.
These results demonstrate that xMIx makes MI applications practical for
deployment in production LLM serving systems.

Decisions in healthcare, public policy, economics, and many other fields often rest on causal conclusions drawn from observational data. These conclusions can be surprisingly fragile: ordinary data problems such as duplicate records, entry mistakes, or corrupted subsets can substantially change, or even reverse, an estimated causal effect. This raises a basic question: how robust is a causal claim to small, targeted changes in the data? We address this question through the lens of cardinality repairs and introduce SubCure, a framework for auditing causal robustness. Given a causal query and a desired range for the estimated effect, SubCure finds a small set of records, or a compact subpopulation described by attribute-value predicates, whose removal moves the estimate into that range. The size of this repair is an intuitive, data-centric, model-agnostic measure of how fragile a conclusion is. The removed data reveals which parts of the dataset are responsible for the observed effect. We formalize the problem for both individual records and subpopulations. To handle large datasets, we design scalable search algorithms that update causal estimates incrementally, rather than recomputing them from scratch after every deletion. Experiments on four real-world datasets and a synthetic benchmark show that SubCure finds smaller and more influential subsets than eight baseline methods, scales to datasets with millions of records, and exposes vulnerabilities that traditional sensitivity analyses miss.

While digital AI and large multimodal models have achieved massive scaling laws in virtual spaces, grounding artificial intelligence in the unstructured, non-deterministic physical world exposes severe foundational bottlenecks. Physical AI -the synthesis of embodied robotics, multi-modal perception, foundation world models, and real-time control- cannot rely merely on scaling compute or self-supervised text scraping. The transition to embodied agents operating safely at human-level dexterity and situational reasoning presents acute open problems: closing the sim-to-real gap, formulating verifiable neural world models, scaling physics-grounded reinforcement learning under sparse supervision, and developing low-latency edge inference capable of deterministic safety guarantees.

This talk bypasses off-the-shelf industrial deployments to outline the critical scientific and algorithmic roadblocks where industry and public frameworks stall without academic intervention. We will dissect the open research questions Israel must tackle to pioneer embodied autonomy: How do we construct mathematically rigorous bounds for agent safety in unstructured physical environments? What new paradigms in spatial reasoning and tactile-proprioceptive sensor fusion can replace sample-inefficient learning?

Short bio: Guy Altagar is the Vice President and Head of Physical AI at the Israeli National AI Directorate within the Prime Minister's Office, where he leads national strategy, infrastructure development, and R&D testbed initiatives for embodied artificial intelligence and robotics. Prior to his government role, he was the founder and Chief Executive Officer of Unlimited Robotics, leading the development of autonomous service robot platforms and software operating systems for embodied devices. With an interdisciplinary background spanning deep-tech entrepreneurship, engineering leadership, and law, Guy works closely with academic research institutions, government bodies, and international industry leaders to accelerate national-scale computing infrastructure, physical test environments, and cross-disciplinary research in physical autonomy.

Modern computer vision systems achieve strong performance, but often depend on extensive manual annotations and substantial computational resources. This PhD seminar explores how the structure of visual data can help overcome these limitations, focusing on learning segmentation with limited supervision and enabling efficient visual processing.

I will begin with semi-supervised semantic segmentation, showing how spatial relationships between neighboring predictions can improve pseudo-label reliability and make better use of unlabeled images. I will then turn to instance segmentation for robotic grasping; beyond annotation scarcity, I will examine annotation quality, introducing controlled benchmarks that reveal how spatial errors and automatically generated masks affect segmentation performance.

The second part extends this efficiency perspective to vision–language models (VLMs). I will present approaches that predict sufficient input resolution, retrieve high-resolution regions when additional evidence is needed, and progressively encode visual detail using wavelet representations and computation reuse. These approaches adapt visual processing to the requirements of each task, offering control over the trade-off between accuracy and computational cost.

Together, these studies investigate how visual structure and task-dependent information can support effective learning and inference with fewer resources.