Publications

Does a Hybrid Space-Aware Randomized Defense Improve Empirical and Certified Adversarial Robustness?
Joy Dhar
Manish Kumar Pandey
Behzad Bozorgtabar
Nayyar Zaidi
Wenyu Zhang
Wei-Hong Li
Tingting Mu
Dwarikanath Mahapatra
Mahsa Baktashmotlagh
Trung Le
Chen Chen
Sajib Mistry
Camila Gonzalez
Samira Ebrahimi Kahou
Lina Yao
Piotr Koniusz
Robert Burns Fisher
Dinh Phung
Bohyung Han
Nuno Vasconcelos … (see 1 more)
Pietro Lio
We introduce Hybrid Space-aware Stochastic Convolution Attention Noise (HySCAN), a hybrid randomized defense that helps close the long-stand… (see more)ing gap between provable robustness under ℓ2 certificates and empirical robustness against strong ℓ∞ attacks, while maintaining strong generalization across diverse imaging benchmarks. HySCAN jointly explores complementary sources of stochasticity at both training and inference: (i) implicit weight-space randomness via stochastic-aware Random Weights, and (ii) explicit feature-space randomness via Stochastic Attention Noise Injection modules. By incorporating randomness at both the parameter and representation levels, HySCAN enables meaningful certified guarantees while improving empirical robustness in practice. Comprehensive experiments on diverse imaging datasets, e.g., CelebA, CIFAR-10, and CIFAR-100, ImageNet-1k, HAM10000, and NIH Chest X-ray, demonstrate that HySCAN outperforms existing certified and empirical defenses, improving certified robustness by up to ≈ 9.6% and empirical robustness by up to ≈ 5% without reducing clean accuracy.
2026-04-29
International Conference on Machine Learning (accepted)
openreview.net
openreview.net
FedFit: Federated Dynamic Sparse Training via Fisher Information scoring
Meng Bi
Hong Huang
Jinlong Song
Charles Wang
Chengming Hu
Xi Chen
Ting Yu
Xue Liu
Cross-device Federated Learning (FL) is frequently bottlenecked by the prohibitive memory and communication costs of training deep neural ne… (see more)tworks on resource-constrained edge hardware. While federated dynamic sparse training aims to alleviate these costs by adjusting sparse structures during training, existing methods rely on magnitude-based heuristics that are fundamentally ill-suited for the non-convergent, heterogeneous environments inherent to FL. To address this challenge, we propose FedFit, a federated dynamic sparse training framework that replaces simple heuristics with optimization-centric criteria for structure adjustment. By leveraging a second-order approximation of the loss landscape via the Fisher Information Matrix, FedFit enables precise and efficient structure adjustment without the overhead of explicit Hessian computation. Empirical evaluations across computer vision and natural language processing benchmarks demonstrate that FedFit significantly narrows the sparse-to-dense accuracy gap, outperforming state-of-the-art methods while maintaining high communication efficiency. Our code is available at https://github.com/Serena-28/Fedfit.git.
2026-04-29
International Conference on Machine Learning (accepted)
openreview.net
openreview.net
From Lyapunov Analysis to Algorithm Design in two-sided PL Minimax Optimization
Mansi Rankawat
Michael Muehlebach
Simon Lacoste-Julien
Damien Scieur
We derive algorithms for smooth nonconvex nonconcave minimax optimization and establish linear convergence rates for problems that satisfy t… (see more)he two-sided Polyak-Lojasiewicz (PL) inequality. At the core of our approach is the observation that Lyapunov functions can be used not only to certify convergence a posteriori, but also to design algorithms. By replacing an idealized, intractable Lyapunov function with a computable surrogate based on gradient information, we derive TALDA (Tri-Action Lyapunov Descent Ascent), a single-loop algorithm that enforces Lyapunov descent by construction. TALDA guarantees linear convergence under the two-sided PL condition, with a rate that depends explicitly on the cross-smoothness constant. This recovers existing worst-case guarantees while yielding sharper convergence rates in weakly coupled min–max problems.
2026-04-29
International Conference on Machine Learning (accepted)
openreview.net
openreview.net
Large Language Models Are Good Term Extractors: A Systematic Evaluation
Ayla Rigouts Terryn
2026-04-29
Language Resources and Evaluation Conference (published)
doi.org
Position: Theory-Level Autoformalization, From Isolated Statements to Unified Formal Knowledge Bases
Marcus J. Min
Mike He
Zhaoyu Li
Zixuan Yi
Sharad Malik
Aarti Gupta
Xujie Si
Osbert Bastani
Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual stat… (see more)ements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward.
2026-04-29
Position Paper Track @ International Conference on Machine Learning (spotlight)
openreview.net
openreview.net
Predictive Spatio-Temporal Scene Graphs for Semi-Static Scenes
Miguel Saavedra-Ruiz
Charlie Gauthier
Kumaraditya Gupta
Shima Shahfar
Kirsty Ellis
Steven Parkison
Liam Paull
We have seen tremendous recent progress in our ability to build "spatio-semantic" representations that enable robots to perform complex reas… (see more)oning across geometry and semantics. However, the vast majority of these methods lack any ability to perform reasoning across time. This is a desirable property in situations where a robot repeatedly observes an environment where instances may change in between observations, but in a structured way. Consider as an example a home environment where the location of a mug typically moves from the cupboard to a countertop to the sink and then back to the cupboard on a daily basis. We should be able to learn this cyclic behavior and use it to predict the state of the mug in the future. In this work, we propose a method that is able to perform this type of tempo-spatio-semantic reasoning. Underpinning the method is a filter, Perpetua
2026-04-29
arXiv (preprint)
doi.org
arxiv.org
SAD-Flower: Flow Matching for Safe, Admissible, and Dynamically Consistent Planning
Tzu-Yuan Huang
Armin Lederer
Dai-Jie Wu
Xiaobing Dai
Sihua Zhang
Hsiu-Chin Lin
Shao-Hua Sun
Stefan Sosnowski
Sandra Hirche
Flow matching (FM) has shown promising results in data-driven planning. However, it inherently lacks formal guarantees for ensuring state an… (see more)d action constraints, whose satisfaction is a fundamental and crucial requirement for the safety and admissibility of planned trajectories on various systems. Moreover, existing FM planners do not ensure the dynamical consistency, which potentially renders trajectories inexecutable. We address these shortcomings by proposing SAD-Flower, a novel framework for generating
2026-04-29
International Conference on Machine Learning (accepted)
doi.org
openreview.net
Search-R2: Enhancing Search-Integrated Reasoning via Actor-Refiner Collaboration
Bowei He
Minda Hu
Zenan Xu
Hongru Wang
Licheng Zong
Yankai Chen
Chen Ma
Xue Liu
Pluto Zhou
Irwin King
Search-integrated reasoning enables language agents to transcend static parametric knowledge by actively querying external sources. However,… (see more) training these agents via reinforcement learning is hindered by the *multi-scale credit assignment* problem: existing methods typically rely on sparse, trajectory-level rewards that fail to distinguish between high-quality reasoning and fortuitous guesses, leading to redundant or misleading search behaviors. To address this, we propose Search-R2, a novel Actor–Refiner collaboration framework that enhances reasoning through targeted intervention, with both components jointly optimized during training. Our approach decomposes the generation process into an Actor, which produces initial reasoning trajectories, and a Meta-Refiner, which selectively diagnoses and repairs flawed steps via a ``cut-and-regenerate'' mechanism. To provide fine-grained supervision, we introduce a hybrid reward design that couples outcome correctness with a dense process reward quantifying the information density of retrieved evidence. Theoretically, we formalize the Actor–Refiner interaction as a smoothed mixture policy, proving that selective correction yields strict performance gains over strong baselines. Extensive experiments across various general and multi-hop QA datasets demonstrate that Search-R2 consistently outperforms strong RAG and RL-based baselines across model scales, achieving superior reasoning accuracy with minimal overhead.
2026-04-29
International Conference on Machine Learning (accepted)
doi.org
openreview.net
$\tau^2$-Bench: Evaluating Conversational Agents in a Dual-Control Environment
Victor Barres
Honghua Dong
Soham Ray
Xujie Si
Karthik R Narasimhan
Existing benchmarks for conversational AI agents simulate _single-control_ environments, where only the AI agent can use tools to interact w… (see more)ith the world, while the user remains a passive information provider. This differs from real-world scenarios like technical support, where users need to actively participate in modifying the state of the (shared) world. In order to address this gap, we introduce
2026-04-29
International Conference on Machine Learning (spotlight)
openreview.net
openreview.net
The Cost of Commitment in Option-Based Hierarchical RL
Randy Lefebvre
Audrey Durand
Empirically, option-based hierarchical reinforcement (HRL) learning often produces longer and more diverse options when a deliberation cost … (see more)is charged at option boundaries. However, when options are executed for many steps under an approximate dynamics model, small model errors compound along the option, degrading the quality of the resulting plan. In this work, we introduce the commitment loss to formalize the tradeoff between deliberation cost and model error as a function of option duration. We characterize how optimal termination probabilities vary with this tradeoff under two model-error mechanisms. First, the model is learned from finite data via maximum-likelihood estimation, producing statistical error that interacts with option duration. Second, we consider an input-driven setting where an exogenous input is only observed at option boundaries and evolves unobserved between them, creating a drift-induced mismatch between planned and realized dynamics. In both cases, we solve for the optimal termination behavior as a function of deliberation cost and the error scale, clarifying the behavior of some popular HRL algorithms that approach the deliberation cost as a heuristic.
2026-04-29
International Conference on Machine Learning (accepted)
openreview.net
openreview.net
The $\textit{Silicon Society}$ Cookbook: Design Space of LLM-based Social Simulations
Aurélien Bück-Kaeffer
Sneheel Sarangi
Maximilian Puelma Touzel
Reihaneh Rabbany
Zachary Yang
Jean-François Godbout
Studies attempting to simulate human behavior with …
2026-04-29
arXiv (preprint)
doi.org
arxiv.org
DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
Youyuan Zhang
Jialiang Sun
Hangrui Bi
Chuqin Geng
Wenjie Ma
Zhaoyu Li
Xujie Si
We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for form… (see more)al theorem proving. Existing approaches either rely on fixed lemma libraries, which limit adaptability, or synthesize highly specific intermediate lemmas tailored to individual theorems, thereby lacking generality. DreamProver addresses this gap through an iterative two-stage process. In the wake stage, DreamProver attempts to prove theorems from a training set using the current lemma library while proposing new candidate lemmas. In the "sleep" stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library. Through this alternating cycle, DreamProver progressively evolves a compact set of high-level, transferable lemmas that can be effectively used to prove unseen theorems in related domains. Experimental results demonstrate that DreamProver substantially improves proof success rates across a diverse set of mathematical benchmarks, while also producing more concise proofs and reducing computational cost.
2026-04-28
arXiv (preprint)
doi.org
arxiv.org