pwc-archive/papers-with-abstracts huggingface dataset:
On Statistical Estimation of Edge-Reinforced Random Walks
Authors: Qinghua, Ding, Venkat Anantharam
Date: 2025-03-08 00:00:00
Tasks: Representation Learning

Reinforced random walks (RRWs), including vertex-reinforced random walks (VRRWs) and edge-reinforced random walks (ERRWs), model random walks where the transition probabilities evolve based on prior visitation history~\cite{mgr, fmk, tarres, volkov}. These models have found applications in various areas, such as network representation learning~\cite{xzzs}, reinforced PageRank~\cite{gly}, and modeling animal behaviors~\cite{smouse}, among others. However, statistical estimation of the parameters governing RRWs remains underexplored. This work focuses on estimating the initial edge weights of ERRWs using observed trajectory data. Leveraging the connections between an ERRW and a random walk in a random environment (RWRE)~\cite{mr, mr2}, as given by the so-called "magic formula", we propose an estimator based on the generalized method of moments. To analyze the sample complexity of our estimator, we exploit the hyperbolic Gaussian structure embedded in the random environment to bound the fluctuations of the underlying random edge conductances.
Biased Federated Learning under Wireless Heterogeneity
Authors: Muhammad Faraz Ul Abrar, Nicolò Michelusi
Date: 2025-03-08 00:00:00
Tasks: Federated Learning

Federated learning (FL) has emerged as a promising framework for distributed learning, enabling collaborative model training without sharing private data. Existing wireless FL works primarily adopt two communication strategies: (1) over-the-air (OTA) computation, which exploits wireless signal superposition for simultaneous gradient aggregation, and (2) digital communication, which allocates orthogonal resources for gradient uploads. Prior works on both schemes typically assume \emph{homogeneous} wireless conditions (equal path loss across devices) to enforce zero-bias updates or permit uncontrolled bias, resulting in suboptimal performance and high-variance model updates in \emph{heterogeneous} environments, where devices with poor channel conditions slow down convergence. This paper addresses FL over heterogeneous wireless networks by proposing novel OTA and digital FL updates that allow a structured, time-invariant model bias, thereby reducing variance in FL updates. We analyze their convergence under a unified framework and derive an upper bound on the model ``optimality error", which explicitly quantifies the effect of bias and variance in terms of design parameters. Next, to optimize this trade-off, we study a non-convex optimization problem and develop a successive convex approximation (SCA)-based framework to jointly optimize the design parameters. We perform extensive numerical evaluations with several related design variants and state-of-the-art OTA and digital FL schemes. Our results confirm that minimizing the bias-variance trade-off while allowing a structured bias provides better FL convergence performance than existing schemes.
L$^2$M: Mutual Information Scaling Law for Long-Context Language Modeling
Authors: Zhuo Chen, Oriol Mayné i Comas, Zhuotao Jin, Di Luo, Marin Soljačić
Date: 2025-03-06 00:00:00
Tasks: Language Modeling, Language Modelling, State Space Models

We rigorously establish a bipartite mutual information scaling law in natural language that governs long-range dependencies. This scaling law, which we show is distinct from and scales independently of the conventional two-point mutual information, is the key to understanding long-context language modeling. Using this scaling law, we formulate the Long-context Language Modeling (L$^2$M) condition, which relates a model's capacity for effective long context length modeling to the scaling of its latent state size for storing past information. Our results are validated through experiments on both transformers and state space models. This work establishes a theoretical foundation that guides the development of large language models toward longer context lengths.
An Information-theoretic Multi-task Representation Learning Framework for Natural Language Understanding
Authors: Dou Hu, Lingwei Wei, Wei Zhou, Songlin Hu
Date: 2025-03-06 00:00:00
Tasks: Natural Language Understanding, Representation Learning

This paper proposes a new principled multi-task representation learning framework (InfoMTL) to extract noise-invariant sufficient representations for all tasks. It ensures sufficiency of shared representations for all tasks and mitigates the negative effect of redundant features, which can enhance language understanding of pre-trained language models (PLMs) under the multi-task paradigm. Firstly, a shared information maximization principle is proposed to learn more sufficient shared representations for all target tasks. It can avoid the insufficiency issue arising from representation compression in the multi-task paradigm. Secondly, a task-specific information minimization principle is designed to mitigate the negative effect of potential redundant features in the input for each task. It can compress task-irrelevant redundant information and preserve necessary information relevant to the target for multi-task prediction. Experiments on six classification benchmarks show that our method outperforms 12 comparative multi-task methods under the same multi-task settings, especially in data-constrained and noisy scenarios. Extensive experiments demonstrate that the learned representations are more sufficient, data-efficient, and robust.
Interpretable Transformation and Analysis of Timelines through Learning via Surprisability
Authors: Osnat Mokryn, Teddy Lazebnik, Hagit Ben Shoshan
Date: 2025-03-06 00:00:00
Tasks: Time Series

The analysis of high-dimensional timeline data and the identification of outliers and anomalies is critical across diverse domains, including sensor readings, biological and medical data, historical records, and global statistics. However, conventional analysis techniques often struggle with challenges such as high dimensionality, complex distributions, and sparsity. These limitations hinder the ability to extract meaningful insights from complex temporal datasets, making it difficult to identify trending features, outliers, and anomalies effectively. Inspired by surprisability -- a cognitive science concept describing how humans instinctively focus on unexpected deviations - we propose Learning via Surprisability (LvS), a novel approach for transforming high-dimensional timeline data. LvS quantifies and prioritizes anomalies in time-series data by formalizing deviations from expected behavior. LvS bridges cognitive theories of attention with computational methods, enabling the detection of anomalies and shifts in a way that preserves critical context, offering a new lens for interpreting complex datasets. We demonstrate the usefulness of LvS on three high-dimensional timeline use cases: a time series of sensor data, a global dataset of mortality causes over multiple years, and a textual corpus containing over two centuries of State of the Union Addresses by U.S. presidents. Our results show that the LvS transformation enables efficient and interpretable identification of outliers, anomalies, and the most variable features along the timeline.
Ambiguity Function Analysis and Optimization of Frequency-Hopping MIMO Radar with Movable Antennas
Authors: Xiang Chen, Ming-Min Zhao, Min Li, Liyan Li, Min-Jian Zhao, Jiangzhou Wang
Date: 2025-03-06 00:00:00

In this paper, we propose a movable antenna (MA)-enabled frequency-hopping (FH) multiple-input multiple-output (MIMO) radar system and investigate its sensing resolution. Specifically, we derive the expression of the ambiguity function and analyze the relationship between its main lobe width and the transmit antenna positions. In particular, the optimal antenna distribution to achieve the minimum main lobe width in the angular domain is characterized. We discover that this minimum width is related to the antenna size, the antenna number, and the target angle. Meanwhile, we present lower bounds of the ambiguity function in the Doppler and delay domains, and show that the impact of the antenna size on the radar performance in these two domains is very different from that in the angular domain. Moreover, the performance enhancement brought by MAs exhibits a certain trade-off between the main lobe width and the side lobe peak levels. Therefore, we propose to balance between minimizing the side lobe levels and narrowing the main lobe of the ambiguity function by optimizing the antenna positions. To achieve this goal, we propose a low-complexity algorithm based on the Rosen's gradient projection method, and show that its performance is very close to the baseline. Simulation results are presented to validate the theoretical analysis on the properties of the ambiguity function, and demonstrate that MAs can reduce the main lobe width and suppress the side lobe levels of the ambiguity function, thereby enhancing radar performance.
Training-Free Graph Filtering via Multimodal Feature Refinement for Extremely Fast Multimodal Recommendation
Authors: Yu-Seung Roh, Joo-Young Kim, Jin-Duk Park, Won-Yong Shin
Date: 2025-03-06 00:00:00
Tasks: Multimodal Recommendation, Recommendation Systems

Multimodal recommender systems improve the performance of canonical recommender systems with no item features by utilizing diverse content types such as text, images, and videos, while alleviating inherent sparsity of user-item interactions and accelerating user engagement. However, current neural network-based models often incur significant computational overhead due to the complex training process required to learn and integrate information from multiple modalities. To overcome this limitation, we propose MultiModal-Graph Filtering (MM-GF), a training-free method based on the notion of graph filtering (GF) for efficient and accurate multimodal recommendations. Specifically, MM-GF first constructs multiple similarity graphs through nontrivial multimodal feature refinement such as robust scaling and vector shifting by addressing the heterogeneous characteristics across modalities. Then, MM-GF optimally fuses multimodal information using linear low-pass filters across different modalities. Extensive experiments on real-world benchmark datasets demonstrate that MM-GF not only improves recommendation accuracy by up to 13.35% compared to the best competitor but also dramatically reduces computational costs by achieving the runtime of less than 10 seconds.
Generalization in Federated Learning: A Conditional Mutual Information Framework
Authors: Ziqiao Wang, Cheng Long, Yongyi Mao
Date: 2025-03-06 00:00:00
Tasks: Federated Learning, Privacy Preserving

Federated learning (FL) is a widely adopted privacy-preserving distributed learning framework, yet its generalization performance remains less explored compared to centralized learning. In FL, the generalization error consists of two components: the out-of-sample gap, which measures the gap between the empirical and true risk for participating clients, and the participation gap, which quantifies the risk difference between participating and non-participating clients. In this work, we apply an information-theoretic analysis via the conditional mutual information (CMI) framework to study FL's two-level generalization. Beyond the traditional supersample-based CMI framework, we introduce a superclient construction to accommodate the two-level generalization setting in FL. We derive multiple CMI-based bounds, including hypothesis-based CMI bounds, illustrating how privacy constraints in FL can imply generalization guarantees. Furthermore, we propose fast-rate evaluated CMI bounds that recover the best-known convergence rate for two-level FL generalization in the small empirical risk regime. For specific FL model aggregation strategies and structured loss functions, we refine our bounds to achieve improved convergence rates with respect to the number of participating clients. Empirical evaluations confirm that our evaluated CMI bounds are non-vacuous and accurately capture the generalization behavior of FL algorithms.
Lawful and Accountable Personal Data Processing with GDPR-based Access and Usage Control in Distributed Systems
Authors: L. Thomas van Binsbergen, Marten C. Steketee, Milen G. Kebede, Heleen L. Janssen, Tom M. van Engers
Date: 2025-03-10 00:00:00

Compliance with the GDPR privacy regulation places a significant burden on organisations regarding the handling of personal data. The perceived efforts and risks of complying with the GDPR further increase when data processing activities span across organisational boundaries, as is the case in both small-scale data sharing settings and in large-scale international data spaces. This paper addresses these concerns by proposing a case-generic method for automated normative reasoning that establishes legal arguments for the lawfulness of data processing activities. The arguments are established on the basis of case-specific legal qualifications made by privacy experts, bringing the human in the loop. The obtained expert system promotes transparency and accountability, remains adaptable to extended or altered interpretations of the GDPR, and integrates into novel or existing distributed data processing systems. This result is achieved by defining a formal ontology and semantics for automated normative reasoning based on an analysis of the purpose-limitation principle of the GDPR. The ontology and semantics are implemented in eFLINT, a domain-specific language for specifying and reasoning with norms. The XACML architecture standard, applicable to both access and usage control, is extended, demonstrating how GDPR-based normative reasoning can integrate into (existing, distributed) systems for data processing. The resulting system is designed and critically assessed in reference to requirements extracted from the GPDR.
Can Proof Assistants Verify Multi-Agent Systems?
Authors: Julian Alfredo Mendez, Timotheus Kampik
Date: 2025-03-10 00:00:00

This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level programming language, but also to Lean, a proof assistant and programming language. Given these capabilities, Soda can implement multi-agent systems, or parts thereof, that can then be integrated into a mainstream software ecosystem on the one hand and formally verified with state-of-the-art tools on the other hand. We provide a brief and informal introduction to Soda and the aforementioned interoperability capabilities, as well as a simple demonstration of how interaction protocols can be designed and verified with Soda. In the course of the demonstration, we highlight challenges with respect to real-world applicability.
On the Logical Content of Logic Programs
Authors: Alexader V. Gheorghiu
Date: 2025-03-07 00:00:00
Tasks: Negation

Logic programming (LP) is typically understood through operational semantics (e.g., SLD-resolution) or model-theoretic interpretations (e.g., the least Herbrand model). This paper introduces a novel perspective on LP by defining a ``support'' relation that explicates what a program ``knows''. This interpretation is shown to express classical and intuitionistic logic, as well as an intermediate logic, depending on certain choices regarding LP and the meanings of disjunction and negation. These results are formalized using the idea of base-extension semantics within proof-theoretic semantics. Our approach offers new insights into the logical foundations of LP and has potential applications in knowledge representation, automated reasoning, and formal verification.
Matrix Factorization for Inferring Associations and Missing Links
Authors: Ryan Barron, Maksim E. Eren, Duc P. Truong, Cynthia Matuszek, James Wendelberger, Mary F. Dorn, Boian Alexandrov
Date: 2025-03-06 00:00:00
Tasks: Dimensionality Reduction, Information Retrieval, Knowledge Graphs, Link Prediction, Prediction, Recommendation Systems, Uncertainty Quantification

Missing link prediction is a method for network analysis, with applications in recommender systems, biology, social sciences, cybersecurity, information retrieval, and Artificial Intelligence (AI) reasoning in Knowledge Graphs. Missing link prediction identifies unseen but potentially existing connections in a network by analyzing the observed patterns and relationships. In proliferation detection, this supports efforts to identify and characterize attempts by state and non-state actors to acquire nuclear weapons or associated technology - a notoriously challenging but vital mission for global security. Dimensionality reduction techniques like Non-Negative Matrix Factorization (NMF) and Logistic Matrix Factorization (LMF) are effective but require selection of the matrix rank parameter, that is, of the number of hidden features, k, to avoid over/under-fitting. We introduce novel Weighted (WNMFk), Boolean (BNMFk), and Recommender (RNMFk) matrix factorization methods, along with ensemble variants incorporating logistic factorization, for link prediction. Our methods integrate automatic model determination for rank estimation by evaluating stability and accuracy using a modified bootstrap methodology and uncertainty quantification (UQ), assessing prediction reliability under random perturbations. We incorporate Otsu threshold selection and k-means clustering for Boolean matrix factorization, comparing them to coordinate descent-based Boolean thresholding. Our experiments highlight the impact of rank k selection, evaluate model performance under varying test-set sizes, and demonstrate the benefits of UQ for reliable predictions using abstention. We validate our methods on three synthetic datasets (Boolean and uniformly distributed) and benchmark them against LMF and symmetric LMF (symLMF) on five real-world protein-protein interaction networks, showcasing an improved prediction performance.
Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
Authors: Ben Goertzel
Date: 2025-02-26 00:00:00

We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional programs. We begin by reviewing well-known homomorphic encryption schemes for arithmetic operations, and then discuss the adaptation of similar concepts to support logical inference steps in intuitionistic logic. Key to our construction are polynomial functors and Bounded Natural Functors (BNFs), which serve as a categorical substrate on which logic formulas and proofs are represented and manipulated. We outline a complexity-theoretic hardness assumption -- the BNF Distinguishing Problem, constructed via a reduction from Subgraph Isomorphism, providing a foundation for cryptographic security. Finally, we describe how these methods can homomorphically encode the execution of total, dependently typed functional programs, and outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
SMT(LIA) Sampling with High Diversity
Authors: Yong Lai, Junjie Li, Chuan Luo
Date: 2025-02-25 00:00:00
Tasks: Diversity

Satisfiability Modulo Linear Integer Arithmetic, SMT(LIA) for short, is pivotal across various critical domains. Previous research has primarily focused on SMT solving techniques. However, in practical applications such as software and hardware testing, there is a need to generate a diverse set of solutions for use as test inputs. We have developed the first sampling framework that integrates local search with CDCL(T) techniques, named HighDiv, capable of generating a highly diverse set of solutions for constraints under linear integer theory. Initially, in the local search phase, we introduced a novel operator called boundary-aware movement. This operator performs random moves by considering the current state's constraints on variables, thereby enhancing the diversity of variables during the search process. Furthermore, we have conducted an in-depth study of the preprocessing and variable initialization mechanisms within the framework, which significantly enhances the efficiency of subsequent local searches. Lastly, we use the solutions obtained from local search sampling as additional constraints to further explore the solution space using the stochastic CDCL(T) method. Experimental results demonstrate that \HighDiv generates solutions with greater diversity compared to the state-of-the-art SMT(LIA) sampling tool, MeGASampler.
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
Authors: David Yin, Jing Gao
Date: 2025-02-16 00:00:00
Tasks: Automated Theorem Proving, Mathematical Proofs

Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate an entire proof. Proof assistants like Lean offer a great remedy. They are designed for verifying each step of a proof in a formal language, and in recent years researchers have created AI models to generate proofs in their languages. However, the scarcity of large-scale datasets of Lean proofs restrict the performance of such Automated Theorem Proving (ATP) models. We developed LeanNavigator, a novel method for generating a large-scale dataset of Lean theorems and proofs by finding new ways to prove existing Lean theorems. By leveraging an interactive Lean client and an efficient method for proof step generation, LeanNavigator efficiently produces new theorems with corresponding proofs. Applying this approach to Mathlib4, we generated 4.7 million theorems totaling 1 billion tokens, surpassing previous datasets by more than an order of magnitude. Using this extensive dataset, we trained an AI model that outperforms the state-of-the-art ReProver model in theorem-proving tasks. These results confirm our hypothesis and demonstrate the critical role of large datasets in improving the performance of automated theorem provers.
MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
Authors: Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias, Marc Lelarge
Date: 2025-02-11 00:00:00
Tasks: Translation

In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq.
A Comprehensive Survey of Fuzzy Implication Functions
Authors: Raquel Fernandez-Peralta
Date: 2025-02-06 00:00:00
Tasks: Survey

Fuzzy implication functions are a key area of study in fuzzy logic, extending the classical logical conditional to handle truth degrees in the interval $[0,1]$. While existing literature often focuses on a limited number of families, in the last ten years many new families have been introduced, each defined by specific construction methods and having different key properties. This survey aims to provide a comprehensive and structured overview of the diverse families of fuzzy implication functions, emphasizing their motivations, properties, and potential applications. By organizing the information schematically, this document serves as a valuable resource for both theoretical researchers seeking to avoid redundancy and practitioners looking to select appropriate operators for specific applications.