Training large neural network models requires extensive computational resources, often distributed across several nodes and accelerators. Recent findings suggest that it may be sufficient to only exchange the fast moving components of the gradients, while accumulating momentum locally (Decoupled Momentum, or DeMo). However, DeMo assumes that models fit on a single accelerator. We relax this assumption and introduce FlexDeMo, whereby nodes fully shard model parameters locally between different accelerators, while inter-node communication is reduced by synchronizing only fast-moving components instead of the full gradients -- resulting in a hybrid sharded data parallel training strategy. We further introduce a framework, denoted as DeToNATION, that generalizes DeMo, FlexDeMo, and other popular distributed training schemes such as DiLoCo -- introducing new variations of replication schemes and challenging choices made in DeMo. Our results across language and vision domains show that FlexDeMo attains similar validation loss as hybrid sharded data parallel training employing AdamW and full gradient synchronization, while being substantially faster. FlexDeMo is thus a promising distributed training scheme for the largest machine learning models.

We present an enhanced benchmark for evaluating linguistic acceptability in Danish. We first analyze the most common errors found in written Danish. Based on this analysis, we introduce a set of fourteen corruption functions that generate incorrect sentences by systematically introducing errors into existing correct Danish sentences. To ensure the accuracy of these corruptions, we assess their validity using both manual and automatic methods. The results are then used as a benchmark for evaluating Large Language Models on a linguistic acceptability judgement task. Our findings demonstrate that this extension is both broader and more comprehensive than the current state of the art. By incorporating a greater variety of corruption types, our benchmark provides a more rigorous assessment of linguistic acceptability, increasing task difficulty, as evidenced by the lower performance of LLMs on our benchmark compared to existing ones. Our results also suggest that our benchmark has a higher discriminatory power which allows to better distinguish well-performing models from low-performing ones.

Large-scale datasets are foundational for research and development in natural language processing. However, current approaches face three key challenges: (1) reliance on ambiguously licensed sources restricting use, sharing, and derivative works; (2) static dataset releases that prevent community contributions and diminish longevity; and (3) quality assurance processes restricted to publishing teams rather than leveraging community expertise. To address these limitations, we introduce two contributions: the Dynaword approach and Danish Dynaword. The Dynaword approach is a framework for creating large-scale, open datasets that can be continuously updated through community collaboration. Danish Dynaword is a concrete implementation that validates this approach and demonstrates its potential. Danish Dynaword contains over four times as many tokens as comparable releases, is exclusively openly licensed, and has received multiple contributions across industry and research. The repository includes light-weight tests to ensure data formatting, quality, and documentation, establishing a sustainable framework for ongoing community contributions and dataset evolution.

Chatbots based on large language models present a scalable and consistent alternative to human interviewers for collecting qualitative data. In this paper, we introduce the agentic chatbot “Interview Bot”, designed to mimic human adaptability and empathy in an interview setting. We explore to what extent it can handle the nuances and open-ended nature of ethnographic interviews. Our findings indicate that chatbots can engage participants and collect meaningful data, but that they still sometimes fall short of fully replicating human facilitated interviews. Not withstanding challenges with the current state of the art, in the medium term, LLM-based agents hold great potential for scaling qualitative research beyond the confines of geographical, cultural, and language boundaries.

Contemporary machine learning models, such as language models, are powerful, but come with immense resource requirements both at training and inference time. Quantization aware pre-training with ternary weights (1.58 bits per weight) has shown promising results in decoder-only language models and facilitates memoryefficient inference. However, little is known about how quantization-aware training influences the training dynamics beyond such Transformer-based decoder-only language models. Here, we engage in a bottom-up exploration of quantization-aware training, starting with multi-layer perceptrons and graph neural networks. Then, we explore 1.58-bit training in other transformer-based language models: encoder-only and encoderdecoder models. Our results show that in all of these settings, 1.58-bit training is on par with standard 32/16-bit models, yet we also identify challenges specific to 1.58-bit encoder-decoder models. Our results on decoderonly language models hint at a possible regularization effect introduced by quantization-aware training.

Synthetic data is by many expected to have a significant impact on data science by enhancing data privacy, reducing biases in datasets, and enabling the scaling of datasets beyond their original size. However, the current landscape of tabular synthetic data generation is fragmented, with numerous frameworks available, only some of which have integrated evaluation modules. synthesizers is a meta-framework that simplifies the process of generating and evaluating tabular synthetic data. It provides a unified platform that allows users to select generative models and evaluation tools from open-source implementations in the research field and apply them to datasets of any format. The aim of synthesizers is to consolidate the diverse efforts in tabular synthetic data research, making it more accessible to researchers from different sub-domains, including those with less technical expertise such as health researchers. This could foster collaboration and increase the use of synthetic data tools, ultimately leading to more effective research outcomes.

Network embedding has recently attracted attention a lot since networks are widely used in various data mining applications. Attempting to break the limitations of pre-set meta-paths and non-global node learning in existing models, we propose a simple but effective framework for heterogeneous network embedding learning by encoding the original multi-type nodes and relations directly in a self-supervised way. To be more specific, we first learn the relation-based embeddings for global nodes from the neighbor properties under each relation type and exploit an attentive fusion module to combine them. Then we design a multi-hop contrast to optimize the regional structure information by utilizing the strong correlation between nodes and their neighbor-graphs, where we take multiple relationships into consideration by multi-hop message passing instead of pre-set meta-paths. Finally, we evaluate our proposed method on various downstream tasks such as node clustering, node classification, and link prediction between two types of nodes. The experimental results show that our proposed approach significantly outperforms state-of-the-art baselines on these tasks.

Embedding learning in multiplex networks has drawn increasing attention in recent years and achieved outstanding performance in many downstream tasks. However, most existing network embedding methods either only focus on the structured information of graphs, rely on the human-annotated data, or mainly rely on multi-layer GCNs to encode graphs at the risk of learning ill-posed spectral filters. Moreover, it is also challenging in multiplex network embedding to learn consensus embeddings for nodes across the multiple views by the inter-relationship among graphs. In this study, we propose a novel and flexible unsupervised network embedding method for attributed multiplex networks to generate more precise node embeddings by simplified Bernstein encoders and alternate contrastive learning between local and global. Specifically, we design a graph encoder based on simplified Bernstein polynomials to learn node embeddings of a specific graph view. During the learning of each specific view, local and global contrastive learning are alternately applied to update the view-specific embedding and the consensus embedding simultaneously. Furthermore, the proposed model can be easily extended as a semi-supervised model by adding additional semi-supervised cost or as an attention-based model to attentively integrate embeddings from multiple graphs. Experiments on three publicly available real-world datasets show that the proposed method achieves significant improvements on downstream tasks over state-of-the-art baselines, while being faster or competitive in terms of runtime compared to the previous studies.

Approximate Dictionary Searching refers to the problem of finding entries in a dictionary that match a search word either exactly or with a certain allowed distance between entry and search word. Extant computationally efficient data structures and algorithms addressing this problem typically do not scale well to large alphabets and/or dictionaries, often requiring prohibitive amounts of memory as the sizes of alphabets and dictionaries increase. This paper presents a data structure and an algorithm for approximate dictionary searching that rely on ternary search trees and implicit Levenshtein automata and scale well with the sizes of both alphabets and dictionaries.

This paper presents an approach for retrofitting pre-trained word representations into sense level representations to improve semantic distinction of words. We use semantic relations as positive and negative examples to refine the results of a pre-trained model instead of integrating them into the objective functions used during training. We experimentally evaluate our approach on two word similarity tasks by retrofitting six datasets generated from three widely used techniques for word representation using two different strategies. Our approach significantly and consistently outperforms three state-of-the-art retrofitting approaches.

Unmanned Aerial Vehicles (UAV) are increasingly gaining interest in Internet of Drones (IoD) applications for automatizing the labor-intensive tasks. They are used in various areas such as infrastructure inspection. However, UAVs have limited energy resources and computational processing capabilities, which prevents them from running applications onboard and accessing the internet for gaining knowledge about their mission. In order to address these challenges imposed by limited resource on the drone, we propose a new cloud system infrastructure for building open-source IoD applications. We have designed a client-server architecture which hosts the drone as a client and the cloud as a scalable server. For validating the developed IoD application, an open-source drone simulator and flight controller are adopted to perform the tests. The overall architecture of a drone-cloud framework is presented along with a use case to show the applicability of the proposed framework.

In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

Abstract In this paper, we show how the theory of sorting networks can be applied to synthesize optimized general-purpose sorting libraries. Standard sorting libraries are often based on combinations of the classic Quicksort algorithm, with insertion sort applied as base case for small, fixed, numbers of inputs. Unrolling the code for the base case by ignoring loop conditions eliminates branching, resulting in code equivalent to a sorting network. By replacing it with faster sorting networks, we can improve the performance of these algorithms. We show that by considering the number of comparisons and swaps alone we are not able to predict any real advantage of this approach. However, significant speed-ups are obtained when taking advantage of instruction level parallelism and non-branching conditional assignment instructions, both of which are common in modern CPU architectures. Furthermore, a close control of how often registers have to be spilled to memory gives us a complete explanation of the performance of different sorting networks, allowing us to choose an optimal one for each particular architecture. Our experimental results show that using code synthesized from these efficient sorting networks as the base case for Quicksort libraries results in significant real-world speed-ups.

This paper describes a computer-assisted non-existence proof of 9-input sorting networks consisting of 24 comparators, hence showing that the 25-comparator sorting network found by Floyd in 1964 is optimal. As a corollary, we obtain that the 29-comparator network found by Waksman in 1969 is optimal when sorting 10 inputs. This closes the two smallest open instances of the optimal-size sorting network problem, which have been open since the results of Floyd and Knuth from 1966 proving optimality for sorting networks of up to 8 inputs. The proof involves a combination of two methodologies: one based on exploiting the abundance of symmetries in sorting networks, and the other based on an encoding of the problem to that of satisfiability of propositional logic. We illustrate that, while each of these can single-handedly solve smaller instances of the problem, it is their combination that leads to the more efficient solution that scales to handle 9 inputs.

There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). In this paper, we present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program.

There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages. We present a new approach which permits the application of existing techniques from term rewriting to prove termination of most functions defined in Haskell programs. In particular, we show how termination techniques for ordinary rewriting can be used to handle those features of Haskell which are missing in term rewriting (e.g., lazy evaluation, polymorphic types, and higher-order functions). We implemented our results in the termination prover AProVE and successfully evaluated them on existing Haskell libraries.

Abstract Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

Abstract Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.

There are two kinds of approaches for termination analysis of logic programs: “transformational” and “direct” ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a Term Rewrite System (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this article we improve these transformations such that they become applicable for any definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check , which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.