Colloquia and Seminars

Space telescopes maintain optical alignment through periodic, resource-intensive wavefront calibration, leaving their optical state unobserved between measurements. In this work, we explore whether engineering telemetry already collected by the James Webb Space Telescope (JWST) can serve as a virtual wavefront sensor.

We propose a machine learning framework that uses thermal and pointing telemetry to estimate spatially resolved optical path difference (OPD) at nanometer precision, without requiring dedicated wavefront measurements at inference time. Our approach combines principal component analysis (PCA) with a two-stage gradient boosting regressor, trained and evaluated on six months of on-orbit JWST data.

Despite the limited number of available measurements, the method achieves statistically significant results in 13 of the 18 mirror segments, with 7 segments exceeding 50% explained variance and the best reaching 91.1%.

These findings demonstrate the potential of telemetry-driven wavefront estimation to support continuous optical monitoring and more efficient calibration scheduling for future space observatories.

Lahav Buzi is an M.Sc. candidate in Electrical Engineering at the Technion, under the supervision of Prof. Yoav Schechner. His research focuses on computational imaging, machine learning, and data-driven wavefront estimation for space telescopes.

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.

Hardware performance counters are widely used to detect malicious behaviour. However, they count only microarchitectural events, and the link between those events and a program’s high-level actions is indirect and noisy. Arm and Intel offer only limited forms of software-defined events: Arm provides a single software-increment event tied directly to individual counters with no event routing, and Intel writes software values into a trace stream rather than into its counters. Ratified RISC-V offers no such mechanism.

This thesis introduces security counters, a counter peripheral for the CVA6 core of the open-source Cheshire SoC. Each counter can be switched at run time between microarchitectural events and event lines driven by software, and each has its own on-chip sampling buffer. A kernel profiling engine drives the software lines when a monitored program makes selected system calls, so the program itself needs no changes. We implemented the complete system on an FPGA running Linux, at a small fraction of the device’s resources, and characterised the counters’ fidelity and overhead.

We then evaluated security counters across trojaned authentication modules, file-hiding kernel rootkits, and malicious inputs to library code. Combining software-defined and hardware counters achieved strong detection at low false-alarm rates, outperforming either source alone. Together, the two sources provide complementary coverage across user space and the kernel, demonstrating the advantage of run-time configurable security counters.

The general-purpose nature of Large Language Models (LLMs) presents a significant challenge for domain-specific applications, often leading to out-of-domain (OOD) interactions that undermine the provider's intent. Existing methods for detecting such scenarios treat the LLM as an uninterpretable black box and overlook the internal processing of inputs. In this work we show that layer transitions provide a promising avenue for extracting domain-specific signature. Specifically, we present several lightweight ways of learning on internal dynamics encoded using a sparse autoencoder (SAE) that exhibit great capability in distinguishing OOD texts. Building on top of SAEs representation transitions enables us to better interpret the LLM internal evolution of input processing and shed light on its decisions. We provide a comprehensive analysis of the method and benchmark it with the gemma-2 2B and 9B models. Our results emphasize the efficacy of the internal process in capturing fine-grained input-related details

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.

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.