SearcharxivSearch

arXiv subjects

Alexei Lisitsa

Publications and source records attributed to Alexei Lisitsa.

At least 19 recordsLinked to original sources

Heuristic Transformer: Belief Augmented In-Context Reinforcement Learning

Transformers have demonstrated exceptional in-context learning (ICL) capabilities, enabling applications across natural language processing, computer vision, and sequential decision-making. In reinforcement learning, ICL reframes learning as a supervised problem, facilitating task adaptation without parameter updates. Building on prior work leveraging transformers for sequential decision-making, we propose Heuristic Transformer (HT), an in-context reinforcement learning (ICRL) approach that augments the in-context dataset with a belief distribution over rewards to achieve better decision-making. Using a variational auto-encoder (VAE), a low-dimensional stochastic variable is learned to represent the posterior distribution over rewards, which is incorporated alongside an in-context dataset and query states as prompt to the transformer policy. We assess the performance of HT across the Darkroom, Miniworld, and MuJoCo environments, showing that it consistently surpasses comparable baselines in terms of both effectiveness and generalization. Our method presents a promising direction to bridge the gap between belief-based augmentations and transformer-based decision-making.

cs.LG

Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction

Recent work by Shehper et al. (2024) demonstrated that the well-known Akbulut-Kirby AK(3) balanced presentation of the trivial group is stably AC-equivalent to the trivial presentation. This result eliminates AK(3) as a potential counterexample to the stable Andrews-Curtis conjecture. In this paper, we present an alternative proof of this result using an automated deduction approach. We provide several transformation sequences, derived from two different proofs generated by the automated theorem prover Prover9, that certify the stable AC-equivalence of AK(3) and the trivial presentation. We conclude by proposing a challenge to develop computational methods for searching stable AC-transformations.

cs.LO

Automated reasoning for proving non-orderability of groups

We demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as positive cones, torsions, generalised torsions and cofinal elements.

math.GT

Handling of Past and Future with Phenesthe+

Writing temporal logic formulae for properties that combine instantaneous events with overlapping temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new temporal logic with intuitive temporal modalities specifically tailored for the representation of both instantaneous and durative phenomena. We also provided an implementation of a complex event processing system, Phenesthe, based on this logic, that has been applied and tested on a real maritime surveillance scenario. In this work, we extend our temporal logic with two extra modalities to increase its expressive power for handling future formulae. We compare the expressive power of different fragments of our logic with Linear Temporal Logic and dyadic first-order logic. Furthermore, we define correctness criteria for stream processors that use our language. Last but not least, we evaluate empirically the performance of Phenesthe+, our extended implementation, and show that the increased expressive power does not affect efficiency significantly.

cs.LO

Online Transition-Based Feature Generation for Anomaly Detection in Concurrent Data Streams

In this paper, we introduce the transition-based feature generator (TFGen) technique, which reads general activity data with attributes and generates step-by-step generated data. The activity data may consist of network activity from packets, system calls from processes or classified activity from surveillance cameras. TFGen processes data online and will generate data with encoded historical data for each incoming activity with high computational efficiency. The input activities may concurrently originate from distinct traces or channels. The technique aims to address issues such as domain-independent applicability, the ability to discover global process structures, the encoding of time-series data, and online processing capability.

cs.LG

Machine learning discovers invariants of braids and flat braids

We use machine learning to classify examples of braids (or flat braids) as trivial or non-trivial. Our ML takes form of supervised learning using neural networks (multilayer perceptrons). When they achieve good results in classification, we are able to interpret their structure as mathematical conjectures and then prove these conjectures as theorems. As a result, we find new convenient invariants of braids, including a complete invariant of flat braids.

math.GT

Describing realizable Gauss diagrams using the concepts of parity or bipartate graphs

Two recent publications describe realizable Gauss diagrams using conditions stating that the number of chords in certain sets of chords is even or odd. We demonstrate that these descriptions are incorrect by finding multiple counter-examples. However, the idea of having a parity-based description of realizable Gauss diagrams is attractive. We recall that realizability of Gauss diagrams as touch curves can be described via bipartite graphs. We show that realizable Gauss diagrams can be described via bipartite graphs.

math.GT

Data Querying with Ciphertext Policy Attribute Based Encryption

Data encryption limits the power and efficiency of queries. Direct processing of encrypted data should ideally be possible to avoid the need for data decryption, processing, and re-encryption. It is vital to keep the data searchable and sortable. That is, some information is intentionally leaked. This intentional leakage technology is known as "querying over encrypted data schemes", which offer confidentiality as well as querying over encrypted data, but it is not meant to provide flexible access control. This paper suggests the use of Ciphertext Policy Attributes Based Encryption (CP-ABE) to address three security requirements, namely: confidentiality, queries over encrypted data, and flexible access control. By combining flexible access control and data confidentiality, CP-ABE can authenticate who can access data and possess the secret key. Thus, this paper identifies how much data leakage there is in order to figure out what kinds of operations are allowed when data is encrypted by CP-ABE.

cs.CR

Can process mining help in anomaly-based intrusion detection?

In this paper, we consider the naive applications of process mining in network traffic comprehension, traffic anomaly detection, and intrusion detection. We standardise the procedure of transforming packet data into an event log. We mine multiple process models and analyse the process models mined with the inductive miner using ProM and the fuzzy miner using Disco. We compare the two types of process models extracted from event logs of differing sizes. We contrast the process models with the RFC TCP state transition diagram and the diagram by Bishop et al. We analyse the issues and challenges associated with process mining in intrusion detection and explain why naive process mining with network data is ineffective.

cs.CR

Process Mining Algorithm for Online Intrusion Detection System

In this paper, we consider the applications of process mining in intrusion detection. We propose a novel process mining inspired algorithm to be used to preprocess data in intrusion detection systems (IDS). The algorithm is designed to process the network packet data and it works well in online mode for online intrusion detection. To test our algorithm, we used the CSE-CIC-IDS2018 dataset which contains several common attacks. The packet data was preprocessed with this algorithm and then fed into the detectors. We report on the experiments using the algorithm with different machine learning (ML) models as classifiers to verify that our algorithm works as expected; we tested the performance on anomaly detection methods as well and reported on the existing preprocessing tool CICFlowMeter for the comparison of performance.

cs.CR

Logic Rules Meet Deep Learning: A Novel Approach for Ship Type Classification

The shipping industry is an important component of the global trade and economy, however in order to ensure law compliance and safety it needs to be monitored. In this paper, we present a novel Ship Type classification model that combines vessel transmitted data from the Automatic Identification System, with vessel imagery. The main components of our approach are the Faster R-CNN Deep Neural Network and a Neuro-Fuzzy system with IF-THEN rules. We evaluate our model using real world data and showcase the advantages of this combination while also compare it with other methods. Results show that our model can increase prediction scores by up to 15.4\% when compared with the next best model we considered, while also maintaining a level of explainability as opposed to common black box approaches.

cs.AI

Untangling Braids with Multi-agent Q-Learning

We use reinforcement learning to tackle the problem of untangling braids. We experiment with braids with 2 and 3 strands. Two competing players learn to tangle and untangle a braid. We interface the braid untangling problem with the OpenAI Gym environment, a widely used way of connecting agents to reinforcement learning problems. The results provide evidence that the more we train the system, the better the untangling player gets at untangling braids. At the same time, our tangling player produces good examples of tangled braids.

cs.LG

Proceedings of the 9th International Workshop on Verification and Program Transformation

The previous VPT 2020 workshop was organized in honour of Professor Alberto Pettorossi on the occasion of his academic retirement from Università di Roma Tor Vergata. Due to the pandemic the VPT 2020 meeting was cancelled but its proceeding have already appeared in the EPTCS 320 volume. The joint VPT-20-21 event has subsumed the original programme of VPT 2020 and provided an opportunity to meet and celebrate the achievements of Professor Alberto Pettorossi; its programme was further expanded with the newly submitted presentations for VPT 2021. The aim of the VPT workshop series is to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields.

cs.SC

Representation and Processing of Instantaneous and Durative Temporal Phenomena

Event definitions in Complex Event Processing systems are constrained by the expressiveness of each system's language. Some systems allow the definition of instantaneous complex events, while others allow the definition of durative complex events. While there are exceptions that offer both options, they often lack of intervals relations such as those specified by the Allen's interval algebra. In this paper, we propose a new logic based temporal phenomena definition language, specifically tailored for Complex Event Processing, that allows the representation of both instantaneous and durative phenomena and the temporal relations between them. Moreover, we demonstrate the expressiveness of our proposed language by employing a maritime use case where we define maritime events of interest. Finally, we analyse the execution semantics of our proposed language for stream processing and introduce the `Phenesthe' implementation prototype.

cs.LO

Circle graphs (chord interlacement graphs) of Gauss diagrams: Descriptions of realizable Gauss diagrams, algorithms, enumeration

Chord diagrams, under the name of Gauss diagrams, are used in low-dimensional topology as an important tool for studying curves or knots. Those Gauss diagrams that correspond to curves or knots are called realizable. The theme of our paper is the fact that realizability of a Gauss diagram can be expressed via its circle graph. Accordingly, one can define and study realizable circle graphs (with realizability of a circle graph understood as realizability of any one of chord diagrams corresponding to the graph). Several studies contain theorems purporting to prove the fact. We check several of these descriptions experimentally and find counterexamples to the descriptions of realizable Gauss diagrams in some of these publications. We formulate new descriptions of realizable circle graphs and present an elegant algorithm for checking if a circle graph is realizable. We enumerate realizable circle graphs for small sizes and comment on these numbers. Then we concentrate on one type of curves, called meanders, and study the circle graphs of their Gauss diagrams.

math.GT

Modular Verification of Autonomous Space Robotics

Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each node's assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used.

cs.SE

Agent-based (BDI) modeling for automation of penetration testing

Penetration testing (or pentesting) is one of the widely used and important methodologies to assess the security of computer systems and networks. Traditional pentesting relies on the domain expert knowledge and requires considerable human effort all of which incurs a high cost. The automation can significantly improve the efficiency, availability and lower the cost of penetration testing. Existing approaches to the automation include those which map vulnerability scanner results to the corresponding exploit tools, and those addressing the pentesting as a planning problem expressed in terms of attack graphs. Due to mainly non-interactive processing, such solutions can deal effectively only with static and simple targets. In this paper, we propose an automated penetration testing approach based on the belief-desire-intention (BDI) agent model, which is central in the research on agent-based processing in that it deals interactively with dynamic, uncertain and complex environments. Penetration testing actions are defined as a series of BDI plans and the BDI reasoning cycle is used to represent the penetration testing process. The model is extensible and new plans can be added, once they have been elicited from the human experts. We report on the results of testing of proof of concept BDI-based penetration testing tool in the simulated environment.

cs.CR