Topological image analysis is a powerful tool for understanding the structure and topology of images, being persistent homology one of its most popular methods. However, persistent homology requires a chain of inclusions of topological spaces, which can be challenging for digital images. In this article, we explore the use of zigzag persistence, a recent variant of traditional persistence, for digital image processing. To this end, new algorithms are developed to build a simplicial complex associated to a digital image and to compute the relationships between homology classes of a sequence of binary images via zigzag persistence. Additionally, we provide a simple software to use them. We demonstrate its effectiveness by applying it to a real-world problem of analyzing honey bee sperm videos.

We use a monomial ideal I to model a discrete preference function on a set of n factors. We can measure the sensitivity of each point represented by a monomial m by calculating its formal partial derivatives with respect to each variable. These derivatives can be used to define the Koszul simplicial complex of the ideal I at m. We refer to points at which the homology of their Koszul complex is not null as sensitive corners. In the context of preference analysis, the ranks of the homology groups are not precise enough to distinguish between sensitive corners that have the same homology but correspond to different sensitivity behaviors. To address this issue, we propose using a filtration on the Koszul complexes of the sensitive corners based on the lcm-lattice of the ideal I. This filtration induces a persistent homology at each corner m. We then use unsupervised Machine Learning methods to classify the corners based on the distance between their persistence diagrams.

We present PSO-PARSIMONY, a new methodology to search for parsimonious and highly accurate models by means of particle swarm optimization. PSO-PARSIMONY uses automatic hyperparameter optimization and feature selection to search for accurate models with low complexity. To evaluate the new proposal, a comparative study with multilayer perceptron algorithm was performed with public datasets and by applying it to predict two important parameters of the force–displacement curve in T-stub steel connections: initial stiffness and maximum strength. Models optimized with PSO-PARSIMONY showed an excellent trade-off between goodness-of-fit and parsimony. The new proposal was compared with GA-PARSIMONY, our previously published methodology that uses genetic algorithms in the optimization process. The new method needed more iterations and obtained slightly more complex individuals, but it performed better in the search for accurate models.

The PSO-PARSIMONY methodology (a heuristic for finding accurate and low-complexity models with particle swarm optimization (PSO)) allows obtaining machine learning models with a good balance between accuracy and complexity. However, when the datasets are of high dimensionality, the methodology does not sufficiently reduce the complexity of the models. This paper presents a new hybrid methodology, called HYB-PARSIMONY, that combines PSO with genetic algorithm (GA) based methods. In the early stages of the optimization process, GA methods have a preponderance to accelerate the search for parsimony. Later, PSO becomes more relevant to improve accuracy. This new methodology obtains significant improvements in the search for more accurate and low-complexity models in high-dimensional datasets.

This work presents formal correctness proofs in Isabelle/HOL of algorithms to transform a matrix into Smith normal form, a canonical matrix form, in a general setting: the algorithms are written in an abstract form and parameterized by very few simple operations. We formally show their soundness provided the operations exist and satisfy some conditions, which always hold on Euclidean domains. We also provide a formal proof on some results about the generality of such algorithms as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out by switching conveniently between two different existing libraries by means of the lifting and transfer package and the use of local type definitions, a sound extension to HOL.

We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field $$\mathrm {GF}(p){}$$ and then performs computations in the ring of integers modulo $$p^k$$, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

In their original setting, both spectral sequences and persistent homology are algebraic topology tools defined from filtrations of objects (e.g. topological spaces or simplicial complexes) indexed over the set \Z of integer numbers. Recently, generalizations of both concepts have been proposed which originate from a different choice of the set of indices of the filtration, producing the new notions of multipersistence and spectral system. In this paper, we show that these notions are related, generalizing results valid in the case of filtrations over \Z. By using this relation and some previous programs for computing spectral systems, we have developed a new module for the Kenzo system computing multipersistence. We also present a new invariant providing information on multifiltrations and applications of our algorithms to spaces of infinite type.

Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations.

Formal verification of algorithms is traditionally taught in Computer Science studies in a theoretical way by means of the Hoare logic axioms and doing (by hand) exercises of verification of small programs. This work shows our experience with Krakatoa, an automatic theorem prover which allows students to interactively visualize the steps required to prove the correctness of a program.

Abstract The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography. In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

We formalize the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions. Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.

Abstract In this contribution we present a formalised algorithm in the Isabelle/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over Bézout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the Bézout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.

Abstract In this paper, we present a formalisation in a proof assistant, Isabelle/HOL, of a naive version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications; and, additionally, a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The aim of this research is not to compete with specialised numerical implementations of Gauss-like algorithms, but to show that formal proofs in this area can be used to generate usable functional programs. The obtained programs show compelling performance in comparison to some other verified and functional versions, and accomplish some challenging tasks, such as the computation of determinants of matrices of big integers and the computation of the homology of matrices representing digital images.