Symbolic constraints and quantitative extensions of equality
ABSTRACT. Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are some prominent examples that play an important role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Such problems arise in working with imprecise information requiring results “within tolerance”. Examples include fuzzy proximity and similarity relations, multi-valued logics, quantitative algebras.
Our algorithms solve unification and anti-unification problems modulo crisp and fuzzy tolerance (i.e., reflexive and symmetric) relations where mismatches between symbol names/arities are permitted, as well as modulo multiple similarity relations. We will discuss general principles behind these techniques, show examples, present some of the algorithms, and characterize their properties.
BronchoX-Cloud: A Diagnostic as a Service Cloud Platform for Planning and Navigation Bronchoscopy
ABSTRACT. Cloud computing claims lower cost, high scalability, availability raised as a more attractive option to standalone solutions. Cloud-based services are being used in numerous areas such as education, engineering, healthcare, and more. In Healthcare, these services could deliver on-demand, self-service Internet infrastructure for medical imaging, entitled from healthcare practitioners to patients. One service that can be supported by cloud-based solutions is bronchoscopy planning. The bronchoscopy endoscopic solutions allow the visualization inside the airways for the diagnostic of possible pulmonary lesions. The infrastructure to support this kind of application might not fit precisely in existing architectures. In this paper, we present an infrastructure to deliver computing resources and services for planning and exploration of reconstructed virtual bronchoscopies using CTs. Our approach for bronchoscopy exploration is intended to support the Diagnosis as a Service (DaaS) concept using backend services, with a simple frontend. Like so, it will contribute and cover two main shortcomings: the performance improvement of our methods by gathering, and testing new data and to make research more accessible to the clinical community. Our tests demonstrate the flexibility, efficiency, and elasticity to supply a bronchoscopy on-demand service.
Convolutional Neural Network Training System For Eye Location On Infrared Driver Recordings Using Automatically Generated Ground Truth Data
ABSTRACT. One of the most important factors in being able to train neural networks with good accuracy is the quality of training data. This is the reason why in every project with such purpose a very big part of the effort is to label data, double check and clean the labeled data and finally select the datasets which will be used for training of the neural networks. This paper presents promising results of an automatic system which selects and uses the data from a ground truth data generator for eye location on infrared driver recordings to train neural networks. The quality of the training data is based on the quality of the generator and it is not altered in any way by any human factor. All the selection of the training dataset is done automatically and the system outputs different neural networks, some of them with very good accuracy of eye detection. This paper presents an automatic system that reduces the human effort for labeling and selection of datasets and outputs neural networks with good accuracy for eye location on infrared driver recordings.
Extracting football players video sprites from broadcast video
ABSTRACT. The main focus of this paper is to explore an alternative method in video sprite extraction. For the case of this work, the priority is creating a dataset of football player’s video sprites - directly from footage of broadcast football matches. The quality of the generated dataset is essential, considering that the obtained dataset can be used for further accurate 2D and 3D reconstructions.
At its core, our approach relies on Mask R-CNN to get the player’s image masks. The process is prone to multiple errors, depending on the player’s pose and position. If we have a semi- supervised dataset collecting process, we can leverage the curated images, and then we use a variational autoencoder (VAE). In the reconstruction phase, many uncommon image masks will be converted to more generic ones, thus, improving the process of creating the dataset.
Methods of acceleration for feature extractions in medical imaging using GPU processing
ABSTRACT. Healthcare routine is defined by many medical images: one-dimensional, two-dimensional, and higher dimensional. Nowadays, computers can scale the workload of domain experts in many medical areas and even outmatch the human interpretation of data. Important information is extracted from medical images with analysis methods. This information can be presented in a perceivable way to the medical experts through visualization.
The present work will contribute to medical image analysis and processing with applications in pulmonary oncology. Our contribution consists in new approaches of accelerating the investigation of radiographic images which performs processing by applying feature extraction algorithms as Canny Edge Detection and Hough Transform for lines and circles. Our research proposes new ways to reduce the computing times of several feature extraction algorithms, either through parallel implementations with CUDA or based on the particularities of the investigated images.
A Fractional Mathematical Model of the ongoing Coronavirus Disease (COVID-19) Pandemic: A Case Study in Turkey
ABSTRACT. Since the outbreak of the deadly virus COVID-19 in Wuhan, China, which was subsequently declared a pandemic at the beginning of December 2019. Cases in America, Europe have risen rapidly in the last few months which increases the need to monitor the spread of the virus. Besides, the cure and vaccine for COVID-19 have largely remained unknown. Turkey reported the first case of COVID-19 on 11 March 2020 and the first virus death four years later since the outbreak of the deadly coronavirus pandemic. COVID-19 spread rapidly in Turkey, where about a total of 3,208,173 cases of infected persons were registered by 29 March 2021 with 2,957,093 cases of recovered persons and 31,076 reported deaths. A new mathematical COVID-19 model containing six classes is presented. Also, the positive invariant region of the solutions, basic reproductive number, disease-free equilibrium, and its stability was highlighted. Afterward, the disease-free equilibrium is locally asymptotically stable when $\mathit{R}_{0}<1.$ Moreover, the proposed model was further generalized to the fractional-order derivative in the Atangana-Baleanu context (ABC) for a more successful realization. Besides, the existence and uniqueness of solutions via techniques of Schaefer's and Banach fixed point theorems were established. Based on the publicly recorded number of infected people from 1-31 July 2020 in Turkey and least-squares curve fitting techniques with $\textit{fminsearch}$ function the fractional proposed model has been validated and can better fit the data compare with the integer-order model. Also, using the Atangana-Toufik scheme, numerical solutions, as well as simulations, were presented for different values of fractional order.
ABSTRACT. In this talk, we will present two shrinking inertial extragradient algorithms for finding a solution of the split equilibrium and fixed point problems involving nonexpansive mappings and pseudomonotone bifunctions that satisfy Lipschitz-type continuous in real Hilbert spaces. The strong convergence theorems of the introduced algorithms are showed either with or without the prior knowledge of the Lipschitz-type constants of bifunctions under some constraint qualifications of the scalar sequences. Some numerical experiments are performed to demonstrate the computational effectiveness of the established algorithms.
ABSTRACT. In this work, we propose a novel algorithm for finding a common fixed point of an infinite family of nonexpansive mappings. We then prove strong convergence of the proposed algorithm under some suitable conditions. Moreover we apply our algorithm to solving regression and classification problems. We also compare convergence behavior of our algorithm with the others in the literature.
An accelerated common fixed point algorithm for a countable family of $G$-nonexpansive mappings with applications to image recovery
ABSTRACT. In this paper, we define a new concept of left and right coordinate affine of a directed graph and then employ it to introduce a new accelerated common fixed point algorithm for a countable family of $G$-nonexpansive mappings in a real Hilbert space with a graph. We prove, under some certain conditions, weak convergence theorems of the proposed algorithm. As applications, we also applied our results to solve convex minimization and image restoration problems. Moreover, it is shown that our algorithm provides better convergence behavior than other methods in the literature.
ABSTRACT. Unification, matching and generalization problems play an important role in various areas of mathematics, computer science and artificial intelligence. Unification and matching are central computational mechanisms in automated reasoning, rewriting, declarative programming.
Generalization is closely related to detecting similarities between objects and to learning general structures from concrete instances. Anti-unification is a logic-based method for computing generalizations, with a wide range of applications. In the first-order syntactic case, solutions of unification and matching problems make two given terms identical, and in anti-unification, common parts of two terms should be exactly the same. While in many situations this is the desired outcome, there are cases when some tolerance with respect to the mismatches would offer a better result. The type of the accepted difference may vary, and many types of mismatches were explored in the fuzzy context.
In this tutorial we present algorithms for the above techniques by representing the imprecise information mainly by proximity relations. They are fuzzy counterparts of tolerance (reflexive, symmetric, but not necessarily transitive) relations and generalize similarity relations (fuzzy equivalences). The presented unification, matching and anti-unification algorithms operate in languages whose signatures tolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures).
One of the challenges in these algorithms is the non-transitivity, that forces a very specific treatment of variable elimination in unification and matching, and working with symbol neighborhoods in anti-unification. Another challenge is the arity mismatch, which requires to explicitly specify the related argument pairs for proximal symbols. These relations between argument pairs affect the algorithms. In the tutorial, we discuss how these challenges can be addressed.
ABSTRACT. Federated Learning (FL) is an approach to conduct machine learning without centralizing training data in a single place, for reasons of privacy, confidentiality or data volume. However, solving federated machine learning problems raises issues above and beyond those of centralized machine learning. These issues include setting up communication infrastructure between parties, coordinating the learning process, integrating party results, understanding the characteristics of the training data sets of different participating parties, handling data heterogeneity, and operating with the absence of a verification data set. IBM Federated Learning provides infrastructure and coordination for federated learning. This presentation will show how data scientists can design and run federated learning jobs based on existing, centralized machine learning models and can provide high-level instructions on how to run the federation. The framework applies to both Deep Neural Networks as well as “traditional” approaches for the most common machine learning libraries.
Continuous Operations and Fully Autonomous of a Social Service Robotic System.
ABSTRACT. Service robots will be a necessity for humans in
many areas where robots will provide varied daily services that
will become more sophisticated and superior to the capabilities of
robots. We show how our robotic system can handle multiple re-
quired tasks either sequentially, simultaneously, or concurrently.
These tasks can be requested from internal processes or even
from any external systems. Moreover, the robotic system can
perform tasks in a discrete way or in a more intelligent way as
the case of overlapping tasks based on the available resources.
Regardless of the presence of the cloud, where the proposed
architecture follows a fog paradigm to somehow enable the robot
to achieve human-like capabilities, but this system works and
is only partially affected if the cloud is lost. In this paper, we
provide an overview of how this system outperforms while we
are assuming that this architecture could be one of the most
systems that can raising the bar for tasks demanded from a
social service robot in the near future. However, the planning
system is integrated with such a system as a service or as a
black box to fully comply with the fog paradigm, and at the
same time, an innovative method is presented to generate plans
and carry out more than one task. Finally, a use case scenario
describes how the system accepts and handles sequential tasks,
and at the same time, how the system creates and executes plans
to achieve these required tasks. We describe the most relevant
terminology required to understand the proposed system.
ABSTRACT. 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 braid
ABSTRACT. Incremental learning is a class of machine learning algorithms dealing with streams of data arriving in sequential order over time. As such, these algorithms are vulnerable to catastrophic forgetting, which is the tendency of the deep networks to forget past information when new data is added.
This phenomenon could be attenuated with the use of knowledge distillation loss and with the support of a sample memory from past classes. In here, we propose a double distillation class incremental learning recipe, starting from the iCaRL algorithm and remodeling the last classification layer with a relaxed SoftMax function by varying the temperature parameter. We performed extensive experiments to show the advantages of using our method compared to the standard algorithm.
Some fixed point theorems on equivalent metric spaces
ABSTRACT. The aim of this paper is to analyze the existence
of fixed points for mappings defined on complete metric spaces
satisfying almost contractive condition and a general contractive
inequality of integral type. The existence of fixed point is ensure
by hypotheses formulated in terms of equivalent metric spaces.
FIXED POINT THEOREM FOR MAPPINGS SATISFYING A GENERAL CONTRACTIVE CONDITION OF INTEGRAL TYPE VIA THE EQUIVALENT METRIC SPACE
ABSTRACT. The aim of this paper is to analyze the existence
of fixed points for mappings defined on complete metric spaces
satisfying almost contractive condition and a general contractive
inequality of integral type. The existence of fixed point is ensure
by hypotheses formulated in terms of equivalent metric spaces.
A Centralized Three-Term Conjugate Gradient Method for Variational Inequality Problem over the Common Fixed-Point Constraints
ABSTRACT. In this paper we propose a centralized three-term conjugate gradient method for solving the variational inequality over the intersection of nonempty closed and convex constraints which are represented in the form of the fixed-point sets of firmly nonexpansive operators. The method allows not only computation of a single firmly nonexpansive operator, but also application in the situation when the computation of metric projection onto the constrained set cannot be done easily. Under some suitable conditions on corresponding parameters, we show a strong convergence of the iterate to the unique solution of such a variational inequality problem. Finally, in order to show the effectiveness of the theoretical result, we present some numerical experiments on the image classification problem via support vector machine learning.
Convergence Results for Inertial Krasnoselskii-Mann Iterations in Hilbert Spaces with Applications
ABSTRACT. In this paper, we consider inertial iteration methods for Fermat-Weber location problem and primal-dual three-operator splitting in real Hilbert spaces. To do these, we first obtain weak convergence analysis and nonasymptotic O(1/n) convergence rate of the inertial Krasnoselskii-Mann iteration for fixed point of nonexpansive operators in infinite dimensional real Hilbert spaces under some seemingly easy to implement conditions on the iterative parameters. The convergence analysis and rate of convergence results are obtained using conditions which appear not complicated and restrictive as assumed in other previous related results in the literature. We then show that Fermat-Weber location problem and primal-dual three-operator splitting are special cases of fixed point problem of nonexpansive mapping and consequently obtain the convergence analysis of inertial iteration methods for Fermat-Weber location problem and primal-dual three-operator splitting in real Hilbert spaces. Some numerical implementations are drawn from primal-dual three-operator splitting to support the theoretical analysis.
ABSTRACT. In a series of recent papers \cite{Abbas}-\cite{Ber21c}, the authors used the technique of enriching contractive type operators by means of convex averaging, introduced in \cite{Ber19}, to extend some well known classes of operators, thus obtaining {\it enriched nonexpansive operators}, {\it enriched contractions}, {\it enriched Kannan operators}, {\it enriched Chatterjea operators}, {\it enriched \' Ciri\' c-Reich- Rus contractions},{\it enriched multivalued contractions} etc. for which existence, uniqueness and approximation of fixed points were established in various settings.
The main aim of the presentation is to survey some of the above mentioned results, to highlight their potential in applications and indicate some further developments.
An Efficient Maude Formalization of (Rewritable) PT Nets
ABSTRACT. Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems, though not ad-equately expressive to represent (self-)adaptation or reconfig-uration capabilities. Rewriting Logic is a natural frameworkfor several formal models of concurrent/distributed systems. We propose a compact, efficient Maude formalization of “rewritable”Place-Transition nets (with inhibitor arcs) using as a runningexample a manufacturing system that adapts itself upon faultoccurrence. We discuss the advantages of this (hybrid) approach,as well as some concerns that it raises
Equivalence Classes in Performance Evaluation Programming
ABSTRACT. In recent work we have introduced performance evaluation programming - a programming paradigm providing support for performance analysis and formal verification of concurrent programs. For the purpose of software verification the ranges of variables must be bounded, and (bounded versions of) programs are translated into finite state continuous time Markov chains that are verified formally by using probabilistic model checking techniques. Our present aim is to increase the size of the state space of programs that can be verified formally. The solution investigated in this paper is inspired by equivalence partitioning - a well-known software testing technique. We provide experimental results showing that, by partitioning the state space of concurrent programs into behavioral equivalence classes, the performance evaluation programming paradigm can be used to design and verify formally concurrent programs with large state spaces.