Colloquia and Seminars

Granular synchrony assigns a timing type to each communication link, and existing solvability results prove both safety and liveness under the promise that the synchronous subgraph satisfies a graph-theoretic reachability condition. That condition is global and hard to verify, and a protocol that silently relies on it can violate agreement when it fails. We ask instead whether agreement and validity can be made to hold on every timing graph, with the graph condition confined to termination — a guarantee we call condition-independent safety.

We show that the answer depends sharply on topology knowledge and fault type. For crash faults with f >= n/2, no graph-agnostic protocol can be safe on every timing graph while terminating on every graph meeting the CFT condition, but knowing only the identities of one's synchronous neighbors is enough to break this impossibility. For Byzantine faults with 2f + 1 <= n <= 3f − 2, even local knowledge fails: faulty processes can hide the topology that distinguishes a good graph from a bad one.

We then give deterministic and randomized locally graph-aware CFT protocols with condition-independent safety. Both replace quorum intersection with a specialized collection primitive. A process disseminates its safety-relevant state to its synchronous neighbors before participating, so intersecting collections share not merely an identity but the value it contributed.

LLMs are known to exhibit highly sparse computation patterns during training and inference, with multiple works exploiting these for improved model performance or reduced compute costs.

We present PAMM, a simple matrix-multiply approximation algorithm which enables runtime memory compression during both training and inference of LLMs.
Using PAMM we show that the QKV linear maps of the attention mechanism are extremely sparse during model pretraining, enabling as high as 512x memory compression for these modules.

We also demonstrate that PAMM can be used to compress the KV cache of an LLM during inference, by up to 20x with near-zero induced error on the model's performance.

Generative diffusion models can produce realistic images and videos, but making a specific edit or directing a particular movement remains challenging. This PhD seminar explores how to develop these capabilities, progressing from constructing useful training examples to using and controlling pretrained generative models. The research begins with improving visual supervision by connecting images with geometry and detailed language descriptions. It then turns to image editing, where suitable training examples are difficult to collect. By removing objects from photographs and reversing the resulting examples, we can train a model to add objects from written instructions. Keeping image editing as the goal, I next explore a different resource: the ability of pretrained video diffusion models to generate coherent changes over time. From a geometric perspective, these models implicitly represent the manifold of natural images—the space of plausible visual content. Expressing an edit as a gradual path along this manifold allows us to produce the requested change. Finally, video becomes the output we want to control. We develop a method that uses rough animations to specify the intended movement and a pretrained model to supply realistic detail and dynamics, enabling control over motion and appearance without additional training.

Large language models increasingly translate and explain politically contested events, yet their outputs can introduce narrative bias while preserving the underlying facts.

We create two datasets covering the Russia–Ukraine war and the Israel–Palestine conflict, pairing neutral event descriptions with competing narratives curated from news outlets and Telegram channels.

We introduce a framework for measuring perspectival divergence: systematic alignment with competing narratives about the same events. We characterize model-specific tendencies through narrative framing, emotional manipulation, source credibility, social identity, and contested naming.

Across both datasets and four languages, we show that apparent neutrality varies with the conflict, language, and prompting context. To mitigate these effects, we adapt self-distancing, a psychological intervention that prompts models to adopt a distant observer’s perspective.

Across eight models, self-distancing reduces measured divergence by 45% on average while preserving event content in 93% of outputs. We further introduce Self-Distancing Activation Steering (SDAS), which extracts the internal representational shift induced by self-distancing and applies it during generation without fine-tuning or modifying the original prompt.

Across five open-weight models, SDAS reduces divergence by 58% while preserving event content in 91% of outputs. Steering directions also transfer between conflicts without additional tuning, offering a practical approach to measuring and reducing narrative bias without prescribing a preferred political viewpoint.

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.

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.