OpenRaiser/Intern-Atlas huggingface dataset:
Many-Valued Modal Logic
Venue: arXiv cs.LO 2024
Year: 2024

We combine the concepts of modal logics and many-valued logics in a general and comprehensive way. Namely, given any finite linearly ordered set of truth values and any set of propositional connectives defined by truth tables, we define the many-valued minimal normal modal logic, presented as a Gentzen-like sequent calculus, and prove its soundness and strong completeness with respect to many-valued Kripke models. The logic treats necessitation and possibility independently, i.e., they are not defined by each other, so that the duality between them is reflected in the proof system itself. We also prove the finite model property (that implies strong decidability) of this logic and consider some of its extensions. Moreover, we show that there is exactly one way to define negation such that De Morgan's duality between necessitation and possibility holds. In addition, we embed many-valued intuitionistic logic into one of the extensions of our many-valued modal logic.
Kamide is in America, Moisil and Leitgeb are in Australia
Venue: arXiv cs.LO 2024
Year: 2024

It is not uncommon for a logic to be invented multiple times, hinting at its robustness. This trend is followed also by the expansion BD+ of Belnap-Dunn logic by Boolean negation. Ending up in the same logic, however, does not mean that the semantic interpretations are always the same as well. In particular, different interpretations can bring us to different logics, once the basic setting is moved from a classical one to an intuitionistic one. For BD+, two such paths seem to have been taken; one (BDi) by N. Kamide along the so-called American plan, and another (HYPE) by G. Moisil and H. Leitgeb along the so-called Australian plan. The aim of this paper is to better understand this divergence. This task is approached mainly by (i) formulating a semantics for first-order BD+ that provides an Australian view of the system; (ii) showing connections of the less explored (first-order) BDi with neighbouring systems, including an intermediate logic and variants of Nelson's logics.
The Disjunction-Free Fragment of D2 is Three-Valued
Venue: arXiv cs.LO 2024
Year: 2024

In this article, the disjunction-free fragment of Jaśkowski's discussive logic D2 in the language of classical logic is shown to be complete with respect to three- and four-valued semantics. As a byproduct, a rather simple axiomatization of the disjunction-free fragment of D2 is obtained. Some implications of this result are also discussed.
PyMilo: A Python Library for ML I/O
Venue: arXiv cs.LG 2024
Year: 2024

PyMilo is an open-source Python package that addresses the limitations of existing Machine Learning (ML) model storage formats by providing a transparent, reliable, and safe method for exporting and deploying trained models. Current formats, such as pickle and other binary formats, have significant problems, such as reliability, safety, and transparency issues. In contrast, PyMilo serializes ML models in a transparent non-executable format, enabling straightforward and safe model exchange, while also facilitating the deserialization and deployment of exported models in production environments. This package aims to provide a seamless, end-to-end solution for the exportation and importation of pre-trained ML models, which simplifies the model development and deployment pipeline.
Sinhala Transliteration: A Comparative Analysis Between Rule-based and Seq2Seq Approaches
Venue: arXiv cs.CL 2024
Year: 2024

Due to reasons of convenience and lack of tech literacy, transliteration (i.e., Romanizing native scripts instead of using localization tools) is eminently prevalent in the context of low-resource languages such as Sinhala, which have their own writing script. In this study, our focus is on Romanized Sinhala transliteration. We propose two methods to address this problem: Our baseline is a rule-based method, which is then compared against our second method where we approach the transliteration problem as a sequence-to-sequence task akin to the established Neural Machine Translation (NMT) task. For the latter, we propose a Transformer-based Encode-Decoder solution. We witnessed that the Transformer-based method could grab many ad-hoc patterns within the Romanized scripts compared to the rule-based method. The code base associated with this paper is available on GitHub - https://github.com/kasunw22/Sinhala-Transliterator/
Rapid Learning in Constrained Minimax Games with Negative Momentum
Venue: arXiv cs.LG 2024
Year: 2024

In this paper, we delve into the utilization of the negative momentum technique in constrained minimax games. From an intuitive mechanical standpoint, we introduce a novel framework for momentum buffer updating, which extends the findings of negative momentum from the unconstrained setting to the constrained setting and provides a universal enhancement to the classic game-solver algorithms. Additionally, we provide theoretical guarantee of convergence for our momentum-augmented algorithms with entropy regularizer. We then extend these algorithms to their extensive-form counterparts. Experimental results on both Normal Form Games (NFGs) and Extensive Form Games (EFGs) demonstrate that our momentum techniques can significantly improve algorithm performance, surpassing both their original versions and the SOTA baselines by a large margin.
Unbiased GNN Learning via Fairness-Aware Subgraph Diffusion
Venue: arXiv cs.LG 2024
Year: 2024

Graph Neural Networks (GNNs) have demonstrated remarkable efficacy in tackling a wide array of graph-related tasks across diverse domains. However, a significant challenge lies in their propensity to generate biased predictions, particularly with respect to sensitive node attributes such as age and gender. These biases, inherent in many machine learning models, are amplified in GNNs due to the message-passing mechanism, which allows nodes to influence each other, rendering the task of making fair predictions notably challenging. This issue is particularly pertinent in critical domains where model fairness holds paramount importance. In this paper, we propose a novel generative Fairness-Aware Subgraph Diffusion (FASD) method for unbiased GNN learning. The method initiates by strategically sampling small subgraphs from the original large input graph, and then proceeds to conduct subgraph debiasing via generative fairness-aware graph diffusion processes based on stochastic differential equations (SDEs). To effectively diffuse unfairness in the input data, we introduce additional adversary bias perturbations to the subgraphs during the forward diffusion process, and train score-based models to predict these applied perturbations, enabling them to learn the underlying dynamics of the biases present in the data. Subsequently, the trained score-based models are utilized to further debias the original subgraph samples through the reverse diffusion process. Finally, FASD induces fair node predictions on the input graph by performing standard GNN learning on the debiased subgraphs. Experimental results demonstrate the superior performance of the proposed method over state-of-the-art Fair GNN baselines across multiple benchmark datasets.
Enabling New HDLs with Agents
Venue: arXiv cs.AR 2024
Year: 2024

Large Language Models (LLMs) based agents are transforming the programming language landscape by facilitating learning for beginners, enabling code generation, and optimizing documentation workflows. Hardware Description Languages (HDLs), with their smaller user community, stand to benefit significantly from the application of LLMs as tools for learning new HDLs. This paper investigates the challenges and solutions of enabling LLMs for HDLs, particularly for HDLs that LLMs have not been previously trained on. This work introduces HDLAgent, an AI agent optimized for LLMs with limited knowledge of various HDLs. It significantly enhances off-the-shelf LLMs.
Titans: Learning to Memorize at Test Time
Venue: arXiv cs.LG 2024
Year: 2024

Over more than a decade there has been an extensive research effort on how to effectively utilize recurrent models and attention. While recurrent models aim to compress the data into a fixed-size memory (called hidden state), attention allows attending to the entire context window, capturing the direct dependencies of all tokens. This more accurate modeling of dependencies, however, comes with a quadratic cost, limiting the model to a fixed-length context. We present a new neural long-term memory module that learns to memorize historical context and helps attention to attend to the current context while utilizing long past information. We show that this neural memory has the advantage of fast parallelizable training while maintaining a fast inference. From a memory perspective, we argue that attention due to its limited context but accurate dependency modeling performs as a short-term memory, while neural memory due to its ability to memorize the data, acts as a long-term, more persistent, memory. Based on these two modules, we introduce a new family of architectures, called Titans, and present three variants to address how one can effectively incorporate memory into this architecture. Our experimental results on language modeling, common-sense reasoning, genomics, and time series tasks show that Titans are more effective than Transformers and recent modern linear recurrent models. They further can effectively scale to larger than 2M context window size with higher accuracy in needle-in-haystack tasks compared to baselines.
TERA: A Simulation Environment for Terrain Excavation Robot Autonomy
Venue: arXiv cs.RO 2024
Year: 2024

Developing excavation autonomy is challenging given the environments where excavators operate, the complexity of physical interaction and the degrees of freedom of operation of the excavator itself. Simulation is a useful tool to build parts of the autonomy without the complexity of experimentation. Traditional excavator simulators are geared towards high fidelity interactions between the joints or between the terrain but do not incorporate other challenges such as perception required for end to end autonomy. A complete simulator should be capable of supporting real time operation while providing high fidelity simulation of the excavator(s), the environment, and their interaction. In this paper we present TERA (Terrain Excavation Robot Autonomy), a simulator geared towards autonomous excavator applications based on Unity3D and AGX that provides the extensibility and scalability required to study full autonomy. It provides the ability to configure the excavator and the environment per the user requirements. We also demonstrate realistic dynamics by incorporating a time-varying model that introduces variations in the system's responses. The simulator is then evaluated with different scenarios such as track deformation, velocities on different terrains, similarity of the system with the real excavator and the overall path error to show the capabilities of the simulation.
Toi uu hieu suat toc do dong co Servo DC su dung bo dieu khien PID ket hop mang no-ron
Venue: arXiv cs.RO 2024
Year: 2024

DC motors have been widely used in many industrial applications, from small jointed robots with multiple degrees of freedom to household appliances and transportation vehicles such as electric cars and trains. The main function of these motors is to ensure stable positioning performance and speed for mechanical systems based on pre-designed control methods. However, achieving optimal speed performance for servo motors faces many challenges due to the impact of internal and external loads, which affect output stability. To optimize the speed performance of DC Servo motors, a control method combining PID controllers and artificial neural networks has been proposed. Traditional PID controllers have the advantage of a simple structure and effective control capability in many systems, but they face difficulties when dealing with nonlinear and uncertain changes. The neural network is integrated to adjust the PID parameters in real time, helping the system adapt to different operating conditions. Simulation and experimental results have demonstrated that the proposed method significantly improves the speed tracking capability and stability of the motor while ensuring quick response, zero steady-state error, and eliminating overshoot. This method offers high potential for application in servo motor control systems requiring high precision and performance.
Towards Sustainable Large Language Model Serving
Venue: arXiv cs.LG 2024
Year: 2024

In this work, we study LLMs from a carbon emission perspective, addressing both operational and embodied emissions, and paving the way for sustainable LLM serving. We characterize the performance and energy of LLaMA with 1B, 3B, and 7B parameters using two Nvidia GPU types, a latest-generation RTX6000 Ada and an older-generation T4. We analytically model operational carbon emissions based on energy consumption and carbon intensities from three grid regions -- each representing a different energy source mix, and embodied carbon emissions based on chip area and memory size. Our characterization and modeling provide us with an in-depth understanding of the performance, energy, and carbon emissions of LLM serving. Our findings highlight the potential for optimizing sustainable LLM serving systems by considering both operational and embodied carbon emissions simultaneously.
Performance Comparison of Security Credential Management Systems for V2X: North American Standard IEEE 1609.2.1 and European Standard ETSI TS 102 941
Venue: arXiv cs.CR 2024
Year: 2024

This study examines the performance and structural differences between the two primary standards for Security Credential Management Systems (SCMS) in Vehicular-to-Everything (V2X) communication: the North American IEEE standards and the European ETSI standards. It focuses on comparing their respective Public Key Infrastructure (PKI) architectures, certificate application workflows, and the formats of request/response messages used during certificate applications. The research includes a theoretical analysis of message length and security features inherent in each standard. Additionally, practical implementations of both systems are conducted to evaluate their efficiency in certificate management processes. Based on the findings, the study provides recommendations to guide future development of SCMS.
Advanced Displacement Magnitude Prediction in Multi-Material Architected Lattice Structure Beams Using Physics Informed Neural Network Architecture
Venue: arXiv cs.AI 2024
Year: 2024

This paper proposes an innovative method for predicting deformation in architected lattice structures that combines Physics-Informed Neural Networks (PINNs) with finite element analysis. A thorough study was carried out on FCC-based lattice beams utilizing five different materials (Structural Steel, AA6061, AA7075, Ti6Al4V, and Inconel 718) under varied edge loads (1000-10000 N). The PINN model blends data-driven learning with physics-based limitations via a proprietary loss function, resulting in much higher prediction accuracy than linear regression. PINN outperforms linear regression, achieving greater R-square (0.7923 vs 0.5686) and lower error metrics (MSE: 0.00017417 vs 0.00036187). Among the materials examined, AA6061 had the highest displacement sensitivity (0.1014 mm at maximum load), while Inconel718 had better structural stability.
Advancing Similarity Search with GenAI: A Retrieval Augmented Generation Approach
Venue: arXiv cs.IR 2024
Year: 2024

This article introduces an innovative Retrieval Augmented Generation approach to similarity search. The proposed method uses a generative model to capture nuanced semantic information and retrieve similarity scores based on advanced context understanding. The study focuses on the BIOSSES dataset containing 100 pairs of sentences extracted from the biomedical domain, and introduces similarity search correlation results that outperform those previously attained on this dataset. Through an in-depth analysis of the model sensitivity, the research identifies optimal conditions leading to the highest similarity search accuracy: the results reveals high Pearson correlation scores, reaching specifically 0.905 at a temperature of 0.5 and a sample size of 20 examples provided in the prompt. The findings underscore the potential of generative models for semantic information retrieval and emphasize a promising research direction to similarity search.
Proof Recommendation System for the HOL4 Theorem Prover
Venue: arXiv cs.LO 2024
Year: 2024

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s).
A Computational Model of Learning and Memory Using Structurally Dynamic Cellular Automata
Venue: arXiv cs.AI 2024
Year: 2024

In the fields of computation and neuroscience, much is still unknown about the underlying computations that enable key cognitive functions including learning, memory, abstraction and behavior. This paper proposes a mathematical and computational model of learning and memory based on a small set of bio-plausible functions that include coincidence detection, signal modulation, and reward/penalty mechanisms. Our theoretical approach proposes that these basic functions are sufficient to establish and modulate an information space over which computation can be carried out, generating signal gradients usable for inference and behavior. The computational method used to test this is a structurally dynamic cellular automaton with continuous-valued cell states and a series of recursive steps propagating over an undirected graph with the memory function embedded entirely in the creation and modulation of graph edges. The experimental results show: that the toy model can make near-optimal choices to re-discover a reward state after a single training run; that it can avoid complex penalty configurations; that signal modulation and network plasticity can generate exploratory behaviors in sparse reward environments; that the model generates context-dependent memory representations; and that it exhibits high computational efficiency because of its minimal, single-pass training requirements combined with flexible and contextual memory representation.
A Novel Task-Driven Method with Evolvable Interactive Agents Using Event Trees for Enhanced Emergency Decision Support
Venue: arXiv cs.AI 2024
Year: 2024

As climate change and other global challenges increase the likelihood of unforeseen emergencies, the limitations of human-driven strategies in critical situations become more pronounced. Inadequate pre-established emergency plans can lead operators to become overwhelmed during complex systems malfunctions. This study addresses the urgent need for agile decision-making in response to various unforeseen incidents through a novel approach, EvoTaskTree (a task-driven method with evolvable interactive agents using event trees for emergency decision support). This advanced approach integrates two types of agents powered by large language models (LLMs): task executors, responsible for executing critical procedures, and task validators, ensuring the efficacy of those actions. By leveraging insights from event tree analysis, our framework encompasses three crucial tasks: initiating event subevent analysis, event tree header event analysis, and decision recommendations. The agents learn from both successful and unsuccessful responses from these tasks. Finally, we use nuclear power plants as a demonstration of a safety-critical system. Our findings indicate that the designed agents are not only effective but also outperform existing approaches, achieving an impressive accuracy rate of up to 100 % in processing previously unencoun32 tered incident scenarios. This paper demonstrates that EvoTaskTree significantly enhances the rapid formulation of emergency decision-making.
Enhancing AI Safety Through the Fusion of Low Rank Adapters
Venue: arXiv cs.CL 2024
Year: 2024

Instruction fine-tuning of large language models (LLMs) is a powerful method for improving task-specific performance, but it can inadvertently lead to a phenomenon where models generate harmful responses when faced with malicious prompts. In this paper, we explore Low-Rank Adapter Fusion (LoRA) as a means to mitigate these risks while preserving the model's ability to handle diverse instructions effectively. Through an extensive comparative analysis against established baselines using recognized benchmark datasets, we demonstrate a 42\% reduction in the harmfulness rate by leveraging LoRA fusion between a task adapter and a safety adapter, the latter of which is specifically trained on our safety dataset. However, we also observe exaggerated safety behaviour, where the model rejects safe prompts that closely resemble unsafe ones
Dynaseal: A Backend-Controlled LLM API Key Distribution Scheme with Constrained Invocation Parameters
Venue: arXiv cs.CR 2024
Year: 2024

Due to the exceptional performance of Large Language Models (LLMs) in diverse downstream tasks,there has been an exponential growth in edge-device requests to cloud-based models.However, the current authentication mechanism using static Bearer Tokens in request headersfails to provide the flexibility and backend control required for edge-device deployments.To address these limitations, we propose Dynaseal,a novel methodology that enables fine-grained backend constraints on model invocations.
Developing an Ontology for AI Act Fundamental Rights Impact Assessments
Venue: arXiv cs.CY 2024
Year: 2024

The recently published EU Artificial Intelligence Act (AI Act) is a landmark regulation that regulates the use of AI technologies. One of its novel requirements is the obligation to conduct a Fundamental Rights Impact Assessment (FRIA), where organisations in the role of deployers must assess the risks of their AI system regarding health, safety, and fundamental rights. Another novelty in the AI Act is the requirement to create a questionnaire and an automated tool to support organisations in their FRIA obligations. Such automated tools will require a machine-readable form of information involved within the FRIA process, and additionally also require machine-readable documentation to enable further compliance tools to be created. In this article, we present our novel representation of the FRIA as an ontology based on semantic web standards. Our work builds upon the existing state of the art, notably the Data Privacy Vocabulary (DPV), where similar works have been established to create tools for GDPR's Data Protection Impact Assessments (DPIA) and other obligations. Through our ontology, we enable the creation and management of FRIA, and the use of automated tool in its various steps.