arXiv subjects

Alexander Maletzky

Publications and source records attributed to Alexander Maletzky.

5 recordsLinked to original sources

arXiv2021

Comparing the Machine Readability of Traffic Sign Pictograms in Austria and Germany

We compare the machine readability of pictograms found on Austrian and German traffic signs. To that end, we train classification models on synthetic data sets and evaluate their classification accuracy in a controlled setting. In particular, we focus on differences between currently deployed pictograms in the two countries, and a set of new pictograms designed to increase human readability. Besides other results, we find that machine-learning models generalize poorly to data sets with pictogram designs they have not been trained on. We conclude that manufacturers of advanced driver-assistance systems (ADAS) must take special care to properly address small visual differences between current and newly designed traffic sign pictograms, as well as between pictograms from different countries.

cs.CV↗

arXiv2020

A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms

We present a generic and executable formalization of signature-based algorithms (such as Faugère's $F_5$) for computing Gröbner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are currently the best known algorithms for computing Gröbner bases in terms of computational efficiency. The formal development attempts to be as generic as possible, generalizing most known variants of signature-based algorithms, but at the same time the implemented functions are effectively executable on concrete input for efficiently computing mechanically verified Gröbner bases. Besides correctness the formalization also proves that under certain conditions the algorithms a-priori detect and avoid all useless reductions to zero, and return minimal signature Gröbner bases. To the best of our knowledge, the formalization presented here is the only formalization of signature-based Gröbner basis algorithms in existence so far.

cs.SC↗

arXiv2018

Gröbner Bases of Modules and Faugère's $F_4$ Algorithm in Isabelle/HOL

We present an elegant, generic and extensive formalization of Gröbner bases in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger's algorithm, Buchberger's criteria for avoiding useless pairs), but also includes more advanced features like reduced Gröbner bases. Particular highlights are the first-time formalization of Faugère's matrix-based $F_4$ algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Gröbner bases and syzygy modules.

cs.LO↗

arXiv2016

Verifying Buchberger's Algorithm in Reduction Rings

In this paper we present the formal, computer-supported verification of a functional implementation of Buchberger's critical-pair/completion algorithm for computing Gröbner bases in reduction rings. We describe how the algorithm can be implemented and verified within one single software system, which in our case is the Theorema system. In contrast to existing formal correctness proofs of Buchberger's algorithm in other systems, e. g. Coq and ACL2, our work is not confined to the classical setting of polynomial rings over fields, but considers the much more general setting of reduction rings; this, naturally, makes the algorithm more complicated and the verification more difficult. The correctness proof is essentially based on some non-trivial results from the theory of reduction rings, which we formalized and formally proved as well. This formalization already consists of more than 800 interactively proved lemmas and theorems, making the elaboration an extensive example of higher-order theory exploration in Theorema.

cs.SC↗

arXiv2016

Mathematical Theory Exploration in Theorema: Reduction Rings

In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchberger's algorithm in reduction rings. Thanks to the seamless integration of proving and computing in Theorema, this implementation can now be used to compute Gröbner bases in various different domains directly within the system. Moreover, a substantial part of our formalization is made up solely by "elementary theories" such as sets, numbers and tuples that are themselves independent of reduction rings and may therefore be used as the foundations of future theory explorations in Theorema. In addition, we also report on two general-purpose Theorema tools we developed for an efficient and convenient exploration of mathematical theories: an interactive proving strategy and a "theory analyzer" that already proved extremely useful when creating large structured knowledge bases.

cs.SC↗