Searcharxiv⌕ Search

arXiv subjects

Kirill Krinkin

Publications and source records attributed to Kirill Krinkin.

13 recordsLinked to original sources

The Unit Gap: How Sharing Works in Boolean Circuits

We study the gap between the minimum size of a Boolean circuit (DAG) and the minimum size of a formula (tree circuit) over the And-Inverter Graph (AIG) basis {AND, NOT} with free inversions. We prove that this gap is always 0 or 1 (Unit Gap Theorem), that sharing requires opt(f) >= n essential variables (Threshold Theorem), and that no sharing is needed when opt(f) <= 3 (Tree Theorem). Gate counts in optimal circuits satisfy an exact decomposition formula with a binary sharing term. When the gap equals 1, it arises from exactly one gate with fan-out 2, employing either dual-polarity or same-polarity reuse; we prove that no other sharing structure can produce a unit gap.

cs.CC↗

A Simple Constructive Bound on Circuit Size Change Under Truth Table Perturbation

The observation that optimum circuit size changes by at most $O(n)$ under a one-point truth table perturbation is implicit in prior work on the Minimum Circuit Size Problem. This note states the bound explicitly for arbitrary fixed finite complete bases with unit-cost gates, extends it to general Hamming distance via a telescoping argument, and verifies it exhaustively at $n = 4$ in the AIG basis using SAT-derived exact circuit sizes for 220 of 222 NPN equivalence classes. Among 987 mutation edges, the maximum observed difference is $4 = n$, confirming the bound is tight at $n = 4$ for AIG.

cs.CC↗

Equivalence and Divergence of Bayesian Log-Odds and Dempster's Combination Rule for 2D Occupancy Grids

We introduce a pignistic-transform-based methodology for fair comparison of Bayesian log-odds and Dempster's combination rule in occupancy grid mapping, matching per-observation decision probabilities to isolate the fusion rule from sensor parameterization. Under BetP matching across simulation, two real lidar datasets, and downstream path planning, Bayesian fusion is consistently favored (15/15 directional consistency, p = 3.1e-5) with small absolute differences (0.001-0.022). Under normalized plausibility matching, the direction reverses, confirming the result is matching-criterion-specific. The methodology is reusable for any future Bayesian/belief function comparison.

cs.RO↗

"Flipped" University: LLM-Assisted Lifelong Learning Environment

The rapid development of artificial intelligence technologies, particularly Large Language Models (LLMs), has revolutionized the landscape of lifelong learning. This paper introduces a conceptual framework for a self-constructed lifelong learning environment supported by LLMs. It highlights the inadequacies of traditional education systems in keeping pace with the rapid deactualization of knowledge and skills. The proposed framework emphasizes the transformation from institutionalized education to personalized, self-driven learning. It leverages the natural language capabilities of LLMs to provide dynamic and adaptive learning experiences, facilitating the creation of personal intellectual agents that assist in knowledge acquisition. The framework integrates principles of lifelong learning, including the necessity of building personal world models, the dual modes of learning (training and exploration), and the creation of reusable learning artifacts. Additionally, it underscores the importance of curiosity-driven learning and reflective practices in maintaining an effective learning trajectory. The paper envisions the evolution of educational institutions into "flipped" universities, focusing on supporting global knowledge consistency rather than merely structuring and transmitting knowledge.

cs.CY↗

Cognitive Architecture for Co-Evolutionary Hybrid Intelligence

This paper questions the feasibility of a strong (general) data-centric artificial intelligence (AI). The disadvantages of this type of intelligence are discussed. As an alternative, the concept of co-evolutionary hybrid intelligence is proposed. It is based on the cognitive interoperability of man and machine. An analysis of existing approaches to the construction of cognitive architectures is given. An architecture seamlessly incorporates a human into the loop of intelligent problem solving is considered. The article is organized as follows. The first part contains a critique of data-centric intelligent systems. The reasons why it is impossible to create a strong artificial intelligence based on this type of intelligence are indicated. The second part briefly presents the concept of co-evolutionary hybrid intelligence and shows its advantages. The third part gives an overview and analysis of existing cognitive architectures. It is concluded that many do not consider humans part of the intelligent data processing process. The next part discusses the cognitive architecture for co-evolutionary hybrid intelligence, providing integration with humans. It finishes with general conclusions about the feasibility of developing intelligent systems with humans in the problem-solving loop.

cs.AI↗

Co-evolutionary hybrid intelligence

Artificial intelligence is one of the drivers of modern technological development. The current approach to the development of intelligent systems is data-centric. It has several limitations: it is fundamentally impossible to collect data for modeling complex objects and processes; training neural networks requires huge computational and energy resources; solutions are not explainable. The article discusses an alternative approach to the development of artificial intelligence systems based on human-machine hybridization and their co-evolution.

cs.AI↗

Correlation Filter of 2D Laser Scans For Indoor Environment

Modern laser SLAM (simultaneous localization and mapping) and structure from motion algorithms face the problem of processing redundant data. Even if a sensor does not move, it still continues to capture scans that should be processed. This paper presents the novel filter that allows dropping 2D scans that bring no new information to the system. Experiments on MIT and TUM datasets show that it is possible to drop more than half of the scans. Moreover thepaper describes the formulas that enable filter adaptation to a particular robot with known speed and characteristics of lidar. In addition, the indoor corridor detector is introduced that also can be applied to any specific shape of a corridor and sensor.

cs.RO↗

Media Content Delivery Protocols Performance and Reliability Evaluation in Cellular Mobile Networks

Currently, tens of millions of devices around the world communicate with/ each other via cellular networks. In this paper, we study the stability of network content delivery protocols to the effects of network interference. To conduct the research, a tool was developed that allows testing of protocols, such as TCP, UDP, and QUIC. The analysis and comparison of the obtained test results were carried out. In the conclusion, the best protocols for content delivery were shown

cs.NI↗

Imitation Learning Approach for AI Driving Olympics Trained on Real-world and Simulation Data Simultaneously

In this paper, we describe our winning approach to solving the Lane Following Challenge at the AI Driving Olympics Competition through imitation learning on a mixed set of simulation and real-world data. AI Driving Olympics is a two-stage competition: at stage one, algorithms compete in a simulated environment with the best ones advancing to a real-world final. One of the main problems that participants encounter during the competition is that algorithms trained for the best performance in simulated environments do not hold up in a real-world environment and vice versa. Classic control algorithms also do not translate well between tasks since most of them have to be tuned to specific driving conditions such as lighting, road type, camera position, etc. To overcome this problem, we employed the imitation learning algorithm and trained it on a dataset collected from sources both from simulation and real-world, forcing our model to perform equally well in all environments.

cs.LG↗

A Stricter Heap Separating Points-To Logic

Dynamic memory issues are hard to locate and may cost much of a development project's efforts and was repeatedly reported similarly afterwards independently by different persons. Verification as one formal method may proof a given program's heap matches a specified dynamic behaviour. Dynamic (or heap) memory, is the region within main memory that is manipulated by program statements like alloc, free and pointer manipulation during program execution. Usually, heap memory is allocated for problems where the amount of used memory is unknown prior to execution. Regions within the heap may be related "somehow" with each other, often, but not always, by pointers containing absolute addresses of related heap cells. The data structure described by all valid pointer variables manifests heap graphs. A heap graph is a directed connected simple graph within the dynamic memory which may contain cycles, and where each vertex represents an unique memory address and every edge links two heap vertices. The heap graph must be pointed by at least one variable from the local stack or a chain of other heap graphs which is finally pointed by at least one stacked variable. Heap vertices may not overlap. A heap formula expresses the assertion on dynamic memory and can either be a heaplet, or a recursively defined heap-spatial or logical formula.

cs.LO↗

Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition

Abstract predicates are considered in this paper as abstraction technique for heap-separated configurations, and as genuine Prolog predicates which are translated straight into a corresponding formal language grammar used as validation scheme for intermediate heap states. The approach presented is rule-based because the abstract predicates are rule-based, the parsing technique can be interpreted as an automated fold/unfold of the corresponding heap graph.

cs.LO↗

A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and Disjunction

In this paper, we review existing points-to Separation Logics for dynamic memory reasoning and we find that different usages of heap separation tend to be an obstacle. Hence, two total and strict spatial heap operations are proposed upon heap graphs, for conjunction and disjunction -- similar to logical conjuncts. Heap conjunction implies that there exists a free heap vertex to connect to or an explicit destination vertex is provided. Essentially, Burstall's properties do not change. By heap we refer to an arbitrary simple directed graph, which is finite and may contain composite vertices representing class objects. Arbitrary heap memory access is restricted, as well as type punning, late class binding and further restrictions. Properties of the new logic are investigated, and as a result group properties are shown. Both expecting and superficial heaps are specifiable. Equivalence transformations may make denotated heaps inconsistent, although those may be detected and patched by the two generic linear canonization steps presented. The properties help to motivate a later full introduction of a set of equivalences over heap for future work. Partial heaps are considered as a useful specification technique that help to reduce incompleteness issues with specifications. Finally, the logic proposed may be considered for extension for the Object Constraint Language.

cs.LO↗

2D SLAM Quality Evaluation Methods

SLAM (Simultaneous Localization and mapping) is one of the most challenging problems for mobile platforms and there is a huge amount of modern SLAM algorithms. The choice of the algorithm that might be used in every particular problem requires prior knowledge about advantages and disadvantages of each algorithm. This paper presents the approach for comparison of SLAM algorithms that allows to find the most accurate one. The accent of research is made on 2D SLAM algorithms and the focus of analysis is 2D map that is built after algorithm performance. Three metrics for evaluation of maps are presented in this paper

cs.RO↗