We investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs with exact rational weights, quantised FNNs whose weights come from a finite-width arithmetic, and dynamically quantised FNNs in which rational networks are evaluated with respect to a given finite-width arithmetic. We consider two types of specifications used in the literature. Linear programming (LP) specifications are conjunctions of linear constraints, while bit-vector (BV) specifications allow reasoning at the bit level and can express non-linear constraints. Our results give a complexity landscape of these verification problems. For quantised FNNs with fixed arithmetic precision, we show that verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, we establish upper bounds, complementing a previously known PSPACE-hardness result.
论文检索
输入标题、作者或关键词，从 990 篇学术成果中精准定位
Algorithmic decision-making in high-stakes settings can have profound impacts on individuals and populations. While much prior work studies fairness in static settings, recent results show that enforcing static fairness constraints may exacerbate long-run disparities. Motivated by this tension, we study a stylized sequential selection problem in which a decision-maker repeatedly selects individuals, affecting both immediate utility and the population distribution over time. We introduce notions of group fairness for both the short and long term and theoretically analyze the trade-off between fairness and utility via the Price of Fairness (PoF). We characterize optimal and fair policies in the short term and show that the PoF can be large even when group distributions are nearly identical. In contrast, we show that long-term disparities can vanish under simple investment policies that achieve a low PoF. We also empirically validate these theoretical observations using both synthetic and real datasets.
The Simple Temporal Problem (STP) is a core framework for quantitative temporal constraints. As STP data can be inconsistent, we study MaxSTP: compute a maximum-cardinality consistent subset of constraints. This extension is NP-hard, and we analyze its parameterized complexity under measures that capture practically relevant instance features: the number of variables n (instance scale), the maximum coefficient magnitude k (numeric range), and structural parameters of the constraint graph such as treewidth tw (decomposability), and vertex cover size vc (density). We show that MaxSTP is W[1]-hard parameterized by n, implying that n and parameters that depend on n (including tw and vc) are insufficient for fixed-parameter tractability. For combined parameters, we give an O^*(k^n)-time algorithm, yielding single-exponential solvability for fixed k. While k+tw remains W[1]-hard, MaxSTP is in XP via an O^*((n * k)^tw) algorithm. Our results suggest that MaxSTP is often computationally harder than optimizing qualitative CSPs - we verify that many such problems (including RCC-8 and Allen's algebra) are FPT when parameterized by n or tw. However, we also demonstrate that FPT algorithms for MaxSTP are indeed possible but with other parameters such as k + vc.
Achieving optimal coordination in multiagent systems involves a trade-off between intractable centralized planning and suboptimal decentralized execution. We bridge this gap by introducing Approximate Recursive Small Step-Semi-Decentralized A* (RS-SDA*), a tree search algorithm that exploits time-varying centralization during periods of available communication conditioned on the environment or joint actions. By interleaving offline planning with online search and using relaxed heuristics, RS-SDA* achieves high solution quality with reduced computational overhead. SDec-POMDP benchmark experiments show that Approximate RS-SDA* often finds near exact optimal solutions in less than 1% of the time required by exact algorithms. We show scalability in six labyrinth environments both deterministic and stochastic state transitions, and demonstrate real-world feasibility with a multi-drone search-and-rescue simulation in the DARPA Subterranean Challenge cave system.
We present a unified framework for modeling agents’ epistemic states and counterfactual conditionals. The novelty of our approach lies at the semantic level. We introduce a computationally grounded semantics in which an agent’s doxastic accessibility relation, needed to model the standard notion of deductively closed belief, is derived from the agent’s belief base, and in which the notion of comparative similarity between states, needed to interpret counterfactual conditionals, is computed from both the atomic formulas describing the agents’ belief bases and those describing the environment. We use this semantics to interpret a language of beliefs and counterfactuals. We demonstrate the expressiveness of our language and the flexibility of the semantics by formalizing a wide range of notions: counterfactual dependence, counterfactual notions of reason and knowledge, conditional belief. Furthermore, we show that our semantics illuminates the subtle interplay between belief change and counterfactuals. On the computational side, we provide a succinct formulation of model checking for our language and establish a PSPACE complexity result.
Evolutionary Algorithms (EAs) are currently the most popular tool for solving multi-objective optimization problems. Balancing exploration and exploitation is fundamental to the performance of Multi-Objective EAs (MOEAs). Achieving this requires maintaining a set of high-quality solutions for effective exploitation while simultaneously enabling exploration of diverse regions of the search space. In MOEAs, these two roles are typically fulfilled by a single evolutionary population. However, high-quality solutions that are promising for exploitation may lack the potential to guide the search toward different regions of the search space. Conversely, solutions with high exploratory potential that can lead the search toward more promising regions may themselves be of low quality. To address this issue, this paper proposes a dual-population MOEA with Exploration and Exploitation Decoupled (MOEA/EED): the exploration population uses a simple aging mechanism, while the exploitation population preserves the currently optimal solutions. We theoretically prove the benefits of MOEA/EED, i.e., it achieves the upper bounds, O(n^(k+1) · min{1, (e ln(3e) / k)^k}) and O((5e ln(3e))^(n/5)), on the expected running time for solving two commonly studied bi-objective problems OneJumpZeroJump and bi-objective RealRoyalRoad, which are significantly better (even exponentially smaller) than that of the popular SMS-EMOA, NSGA-II, and their non-elitist variants. Lastly, we empirically show its effectiveness on a wide range of practical optimization problems.
Compression techniques such as quantization and low-rank approximation enable large language models (LLMs) to run on current edge hardware with limited computing power, but the key challenge lies in balancing the allocation of precision and low rank within a fixed memory limit. We propose a training-free framework, BALANCER, which achieves global budget allocation for mixed-precision quantization and low-rank correction through information-guided subspace matrices. BALANCER collects a small set of calibration signals—activation statistics, reference gradient magnitudes, and a diagonal curvature proxy—and converts them into information-guided subspace matrices. Instead of relying on coarse-grained layer-wise importance allocation, BALANCER transforms these signals into gain curves for each weight in the matrix singular subspace, allowing a principled greedy allocator to distribute compression bits and ranks across the entire model. On the LLaMA-3.1-8B model, with an average of 3.6 bits per parameter, BALANCER only increases the perplexity from 6.63 to 6.78 (+0.15), while reducing memory from 16 GB to 3.9 GB, and enabling the model to be deployed on edge GPUs such as the Jetson Orin Nano (8 GB).
Knowledge Graphs (KGs) are extensively used across different domains and in several applications. Often, these KGs are very large in size. Such KGs become unwieldy for tasks such as question answering and visualization. Summarization of KGs offers a viable alternative in such cases. Furthermore, personalized KG summarization is crucial in the current data-driven world as it captures the specific requirements of users based on their query patterns. Since it only maintains relevant information, the personalized summaries of KG are small, resulting in significantly smaller storage requirements and query runtime. In this work, we adapt the coreset theory to create personalized KG summaries. For a given dataset and a user-specific query workload, we present an approach that samples a relevant subset of triples using sensitivity-based importance sampling. We ensure that the subset approximates the characteristics of the full dataset with bounded approximation error. We define sensitivity scores that measure the importance of a triple with respect to a user’s query workload, which are then used by our coreset construction algorithm. We explicitly focus on personalized knowledge graph summarization by constructing summaries independently for each user based on their query behaviour. Our evaluation on Freebase, WikiData, and DBpedia shows that COREKG delivers higher query-answering accuracy and structural coverage than the state-of-the-art methods, such as GLIMPSE, PPR, PEGASUS and APEX² while requiring only a tiny fraction of the original graph.
An index is a function that measures the extent to which an election has a particular feature. We seek indices that capture agreement, diversity, and polarization among voters in approval elections, normalized with respect to saturation. The latter means that if two elections differ by the fraction of candidates approved by an average voter, but otherwise are of similar nature, then they should have similar index values. We propose several indices, analyze their properties, and use them to derive a new map of approval elections, and compare various real-life elections from Pabulib, Preflib and other sources.
Achieving visual coordination between egocentric (ego) and exocentric (exo) perspectives is a cornerstone of augmented reality and human-machine collaboration. However, extreme viewpoint shifts and occlusions often cause semantic drift in existing methods, making robust cross-view correspondence a formidable challenge. In this paper, we propose SARA (Semantic-Anchored Referential Alignment), a framework designed to bridge the ego-exo gap by leveraging viewpoint-invariant, high-level semantic information as region-level semantic anchors for robust feature mapping. Specifically, our approach incorporates: (1) the Semantic Anchoring Module extracts cross-view category priors and invariant features to provide stable region-level references across perspectives, and (2) the Multimodal Semantic Vector Fusion mechanism achieves language-guided manifold fusion of semantic vectors to synthesize unified embeddings, effectively establishing representational correspondence across disparate perspectives. Extensive experiments across diverse, complex scenarios demonstrate SARA’s superior performance in establishing stable mappings,validating the effectiveness of semantic-invariant features and multimodal fusion in addressing the core hurdles of cross-view understanding.
It has been shown that a neural network's Lipschitz constant can be leveraged to derive robustness guarantees, to improve generalizability via regularization or even to construct invertible networks. Therefore, a number of methods varying in the tightness of their bounds and their computational cost have been developed to approximate the Lipschitz constant for different classes of networks. However, comparatively little research exists on methods for exact computation, which has been shown to be NP-hard. Nonetheless, there are applications where one might readily accept the computational cost of an exact method. These applications could include the benchmarking of new methods or the computation of robustness guarantees for small models on sensitive data. Unfortunately, existing exact algorithms restrict themselves to only ReLU-activated networks, which are known to come with severe downsides in the context of Lipschitz-constrained networks. We therefore propose a generalization of the LipBaB algorithm to compute exact Lipschitz constants for arbitrary continuous piecewise linear neural networks and p-norms. With our method, networks may contain traditional activations like ReLU or LeakyReLU, activations like GroupSort or the related MaxMin and FullSort, which have been of increasing interest in the context of Lipschitz-constrained networks, or other piecewise linear functions like MaxPool.
Graph Neural Networks (GNNs) have become increasingly central to several analysis tasks in various domains, ranging, e.g., from social networks to molecular analysis. Understanding the decision-making process of GNNs is a critical challenge in machine learning, particularly when post-hoc explanations, attempting to answer why specific inputs are classified in a certain way by a given model, are required for specific input predictions. Existing post-hoc explainability methods for GNNs often rely on counterfactual reasoning, grounded in the `if this had not occurred' thinking, that typically identifies minimal subgraphs perturbations that would change a prediction. Notably, less attention has been posed on the equally important semifactual reasoning, grounded in the `even if this has not occurred' thinking, that results in identifying maximal subgraphs perturbations that would not change a prediction. In this paper, we introduce a novel technique for post-hoc explainability queries in GNNs by focusing on the semifactual reasoning. We first thoroughly investigate the computational complexity of several reasoning and optimization problems related to the computation of semifactuals, and then propose a novel learning architecture for addressing their computation. Finally, we experimentally evaluate the proposed approach in a variety of settings, showing its effectiveness in generating high-quality semifactual explanations.
We study the problem of allocating a set of indivisible items among agents whose preferences include externalities. Unlike the standard fair division model, agents may derive positive or negative utility not only from items allocated directly to them, but also from items allocated to other agents. Since exact envy-freeness cannot be guaranteed, prior work has focused on its relaxations. However, two central questions remained open: does there always exist an allocation that is envy-free up to one item (EF1), and if not, what is the optimal relaxation EF-k that can always be attained? We settle both questions by deriving tight asymptotic bounds on the number of items sufficient to eliminate envy. We show that for any instance with n agents, an allocation that is envy-free up to O(√n) items always exists and can be found in polynomial time. Additionally, via a reduction from fair division with externalities to discrepancy theory combined with recent discrepancy lower bounds, we prove a matching Ω(√n) lower bound showing that this result is tight even when the valuations are binary and satisfy the no-chores condition, which refutes a conjecture from previous work and resolves the main open question in the area, ruling out the existence of EF1 allocations when agents have externalities.
Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and thereby replace some of the manual work %alleviating some of the manual effort done by Formal Verification engineers and deliver value to industry. We present a neurosymbolic approach that includes two prompting frameworks to generate candidate invariants, which are checked using a formal symbolic tool. Our results indicate that with sufficient reprompting, LLMs are able to generate inductive arguments for mid-size open-source RTL designs. For 90% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument.
In this paper, we prove the existence of an envy-free up to one item (EF1) division for a discrete chore. Our approach builds upon the powerful Simmons-Su framework, which leverages Sperner’s lemma to guarantee the existence of a simplex corresponding to a sequence of similar fractional divisions, ensuring that each agent is satisfied with a different bundle. For allocations of goods, existing works have introduced rounding techniques that convert an envy-free fractional division into a connected integral EF1 division for any number of agents with monotone valuations. However, the analogous problem for chores has remained unresolved, and existing rounding techniques fail due to the asymmetric definitions of EF1 for goods and chores. To overcome this asymmetry, we refine the existing rounding techniques and show that connected EF1 divisions exist for a discrete chore.
Incomplete Abstract Argumentation Frameworks (iAAFs) extend Abstract Argumentation Frameworks (AAFs) by allowing arguments and attacks to be specified as uncertain, enabling a compact representation of alternative argumentation scenarios. Despite extensive work on reasoning with iAAFs, their expressive power relative to standard AAFs is still unclear. We address this question by studying whether the reasoning based on possible-extensions in iAAFs can be reduced to classical reasoning on AAFs. Our analysis relates iAAFs and AAFs via two comparison notions: equivalence, where an AAF yields as extensions exactly the possible extensions of an iAAF, and projection-equivalence, where such extensions are obtained by projecting away auxiliary arguments. We characterize the semantics under which these relationships hold, and, in these cases, provide constructive transformations from iAAFs to AAFs, thus also enabling classical argumentation tools to be applied to qualitative-uncertainty reasoning.
This paper studies cross-domain/species action recognition from low-resolution videos with sharp appearance variations and domain-specific biases. Its attractive viewpoint is mining domain-invariant representations of cross-domain/species features under rough spatial details to enhance recognition and generalization, overcoming the significant decline of existing methods. To address this, we propose a generalized Action recognition framework for Low-resolution conditions with Domain-invariant Representation learning, named ActLDR, designed to learn domain-invariant representations. First, it decomposes video understanding into spatial and temporal pathways for explicitly separating domain-dependent appearance cues from robust motion dynamics; Second, it constructs a Spatial-Temporal Feature Exchange module to enable cross-branch refinement and suppress domain bias; Third, we inject Gaussian feature interference to simulate feature corruption and enforce prediction-level consistency to encourage stable representations. Empirical results demonstrate that our proposal outperforms previous methods, significantly improving robustness across resolutions, domains, and species, and demonstrating outstanding generalization and transferability.
Zero-shot transfer for offline reinforcement learning involves generalizing to a wide range of tasks that are often risk-sensitive, without new interaction. We show here that although Successor Features (SFs) provide a principled framework for transfer through abstracting dynamics from rewards, their typical form is restricted to expected cumulative returns and is thus indifferent to variance in returns. We contend that such a mean-centric approach introduces bias by conflating risky and safe trajectories with identical expected outcomes, as it ignores outcome dispersion critical for risk-aware evaluation. Additionally, we note that distributional methods can be employed to model outcome distributions, but frequently do so at a high computational cost due to the need for discretization or elaborate sampling. To overcome this problem, we introduce a form of successor representation that incorporates an uncertainty envelope over states: Gaussian Distributional Successor Features (GDSF). Rather than inferring an implicit generative process, GDSF learns to approximate the distribution of cumulative outcomes with a Gaussian through recursive moment-matching. We present this framework for efficient representation of aleatoric uncertainty, without resorting to computationally expensive existing distributional methods. We also introduce Latent Outcome Optimization, an inference procedure which finds high-reward outcomes in the data support and drives a goal-conditioned policy. This dual-mode design allows the agent to transfer to non-linear objectives in a zero-shot way while preserving closed-form efficiency for linear tasks. Experiments on the D4RL benchmark show that GDSF yields better performance in risk-sensitive tasks while achieving at least competitive results in standard linear regimes.
Reinforcement learning (RL) is commonly used to learn reward-optimizing policies. However, RL policies are not always trained with ethical behavior in mind, which can lead an agent to violate social or legal norms in pursuit of its goal. Retraining agents with additional norms is not always feasible, especially in complex stochastic environments. To mitigate this issue, we present a probabilistic policy fixing framework that adapts norm-agnostic policies online. Using Answer Set Programming (ASP), we generate policy fixes that minimize deviations from the RL policy while optimizing for norm adherence against a set of sampled worlds. Based on the Rule of Three and Hoeffding's inequality, we provide guarantees that fixed policies are near optimal, given a specified level of confidence.
Chain-of-Thought (CoT) reasoning empowers Large Language Models (LLMs) with remarkable capabilities, but typically requires enormous parameter scales. CoT distillation has emerged as a promising paradigm to transfer reasoning prowess into compact student models (SLMs), yet existing approaches often rely on a solitary teacher, capping the student’s potential since individual LLMs often exhibit distinct capability biases and may suffer from catastrophic forgetting. While leveraging diverse teachers seems appealing, effectively fusing their supervisions remains challenging: teacher-student incompatibility risks amplifying hallucinations, and passive supervision fails to ensure genuine logic internalization. To address this, we introduce COMPACT, a framework that adaptively fuses supervisions from different teachers by dynamically weighting teacher gradients based on the student’s real-time compatibility evaluated by a multi-dimensional metric: (1) Graph-based Consensus to filter misleading rationales by identifying mainstream reasoning paths; (2) Mutual-Information-based Adaptability to detect "epiphany moments" for genuinely understanding the reasoning process rather than merely imitating; and (3) Loss-based Difficulty to assess student receptivity to the teacher's guidance and prevent negative transfer. Our experiments and latent space analysis demonstrate that COMPACT effectively integrates diverse reasoning capabilities without damaging the model's original knowledge structure, achieving state-of-the-art performance on various benchmarks while effectively mitigating catastrophic forgetting. Code available: https://github.com/CAG-Research/COMPACT.git.