Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
International Conference on Certified Programs and Proofs (CPP 2020), ACM pp. 85 – 98, 2020.
pdf 
doi:10.1145/3372885.3373827
Abstract
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-written mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language. We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages. To train these models we also prepared four informal-to-formal datasets. We compare and analyze our results according to whether the model is supervised or unsupervised. In order to augment the data available for auto-formalization and improve the results, we develop a custom type-elaboration mechanism and integrate it in the supervised translation.
BibTex
@inproceedings{qwcbckju-cpp20, author = {Qingxiang Wang and Chad E. Brown and Cezary Kaliszyk and Josef Urban}, editor = {Jasmin Blanchette and Catalin Hritcu}, title = {Exploration of neural machine translation in autoformalization of mathematics in {M}izar}, booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January 20-21, 2020}, pages = {85--98}, publisher = {{ACM}}, year = {2020}, url = {https://doi.org/10.1145/3372885.3373827}, doi = {10.1145/3372885.3373827}, }
- Details
- Category: Publications 2020
Burak Ekici, Cezary Kaliszyk
Mathematics in Computer Science, 14, pp. 533 – 549, 2020.
pdf doi:10.1007/s11786-020-00450-8
Abstract
(co)Monads are used to encapsulate impure operations of a computation. A (co)monad is determined by an adjunction and further determines a specific type of adjunction called the (co)Kleisli adjunction. Mac Lane introduced the comparison theorem which allows comparing these adjunctions bridged by a (co)monad through a unique comparison functor. In this paper we specify the foundations of category theory in Coq and show that the chosen representations are useful by certifying Mac Lane’s comparison theorem and its basic consequences. We also show that the foundations we use are equivalent to the foundations by Timany. The formalization makes use of Coq classes to implement categorical objects and the axiom uniqueness of identity proofs to close the gap between the contextual equality of objects in a categorical setting and the judgmental Leibniz equality of Coq. The theorem is used by Duval and Jacobs in their categorical settings to interpret the state effect in impure programming languages.
BibTex
@article{beck-mcs20, author = {Burak Ekici and Cezary Kaliszyk}, title = {{M}ac {L}ane's Comparison Theorem for the {K}leisliConstruction Formalized in {C}oq}, journal = {Math. Comput. Sci.}, volume = {14}, number = {3}, pages = {533--549}, year = {2020}, url = {https://doi.org/10.1007/s11786-020-00450-8}, doi = {10.1007/s11786-020-00450-8},}
- Details
- Category: Publications 2020
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Journal of Automated Reasoning 64, pp. 879 – 910, 2020.
pdf doi:10.1007/s10817-020-09545-0
Abstract
This work is a case study of the formal verification and complexity ana- lysis of some famous probabilistic algorithms and data structures in the proof assistant Isabelle/HOL. In particular, we consider the expected number of comparisons in ran- domised quicksort, the relationship between randomised quicksort and average-case deterministic quicksort, the expected shape of an unbalanced random Binary Search Tree, the randomised binary search trees described by Martínez and Roura, and the expected shape of a randomised treap. The last three have, to our knowledge, not been analysed using a theorem prover before and the last one is of particular interest because it involves continuous distributions.
BibTex
@inproceedings{MEMHTN-JAR20, author = "Manuel Eberl and Max W. Haslbeck and Tobias Nipkow", title = "Verified Analysis of Random Binary Tree Structures", series = "J Autom Reasoning", volume = 64, pages = "879--910", year = 2020, doi = "10.1007/s10817-020-09545-0"}
- Details
- Category: Publications 2020
Miroslav Olšák
Algebra universalis 81, pp. 23, 2020.
pdf doi:10.1007/s00012-020-0644-y
Copyright: CC-BY
Abstract
Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an abstract level are conveyed. This paper gives a swift introduction to term rewriting and presents several automatic tools to analyze term rewrite systems which were developed by the Computational Logic Group at the University of Innsbruck. These include the termination tool TTT2, the confluence prover CSI, the completion tools mkbTT and KBCV, the complexity tool TcT, the strategy tool AutoStrat, as well as FORT, an implementation of the decision procedure for the first-order theory for a decidable class of rewrite systems. Besides its applications in research, this software pool has also proved invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting.
BibTex
@Article{Olšák2020, author={Ol{\v{s}}{\'a}k, Miroslav}, title={The local loop lemma}, journal={Algebra universalis}, year={2020}, month={Feb}, day={19}, volume={81}, number={2}, pages={14}, issn={1420-8911}, doi={10.1007/s00012-020-0644-y}, url={https://doi.org/10.1007/s00012-020-0644-y}}
- Details
- Category: Publications 2020
Sarah Winker, Aart Middeldorp
8th International Workshop on Theorem Proving Components for Educational Software, EPTCS 313, pp. 54 – 72, 2020.
Creative Commons License (CC BY 3.0)
Abstract
Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an abstract level are conveyed. This paper gives a swift introduction to term rewriting and presents several automatic tools to analyze term rewrite systems which were developed by the Computational Logic Group at the University of Innsbruck. These include the termination tool TTT2, the confluence prover CSI, the completion tools mkbTT and KBCV, the complexity tool TcT, the strategy tool AutoStrat, as well as FORT, an implementation of the decision procedure for the first-order theory for a decidable class of rewrite systems. Besides its applications in research, this software pool has also proved invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting.
BibTex
@inproceedings{SWAM-ThEdu19, author = "Sarah Winkler and Aart Middeldorp", title = "Tools in Term Rewriting for Education", booktitle = "Proceedings of the 8th International Workshop on Theorem Proving Components for Educational Software" editor = "Pedro Quaresma and Walther Neuper and Jo{\~a}o Marcos", series = "Electronic Proceedings in Theoretical Computer Science", volume = 313, pages = "54--72", year = 2020, doi = "10.4204/EPTCS.313.4"}
- Details
- Category: Publications 2020
Jan Jakubův, Cezary Kaliszyk
Mathematics in Computer Science, 14, pp. 657 – 670, 2020.
pdf doi:10.1007/s11786-020-00474-0
Abstract
We propose an extension of the automated theorem prover E by the weighted path ordering (WPO). Weighted path ordering is theoretically stronger than all the orderings used in E however its parametrization is more involved than those normally used in automated reasoning. Inparticular, it depends on a term algebra. We integrate the ordering in E Prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the onesused in E prover so far.Furthermore, first-time presented here, we propose a relaxed variant of the weighted pathorder as an approximation of the standard WPO definition. A theorem prover strategy with a relaxedorder can be incomplete, which is, however, not an issue as completeness can be easily regainedby switching to a complete strategy. We show that the relaxed weighted path order can have a hugeimpact on an improvement of a theorem prover strategy.
BibTex
@article{jjck-mcs20, author = {Jan Jakubuv and Cezary Kaliszyk}, title = {Relaxed Weighted Path Order in Theorem Proving}, journal = {Math. Comput. Sci.}, volume = {14}, number = {3}, pages = {657--670}, year = {2020}, url = {https://doi.org/10.1007/s11786-020-00474-0}, doi = {10.1007/s11786-020-00474-0},}
- Details
- Category: Publications 2020
Alexander Lochmann, Aart Middeldorp
26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LCNS 12079, pp. 25 – 40, 2020.
pdf doi:10.1007/978-3-030-45237-7_11
The Author(s) 2020
Abstract
We present a formalized proof of the regularity of the infinity predicate on ground terms. This predicate plays an important role in the first-order theory of rewriting because it allows to express the termination property. The paper also contains a formalized proof of a direct tree automaton construction of the normal form predicate, due to Comon.
BibTex
@inproceedings{LM-TACAS20, author = "Alexander Lochmann and Aart Middeldorp", title = "Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting", booktitle = "Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Armin Biere and Dave Parker", series = "Lecture Notes in Computer Science", volume = 12079, pages = "178--194", year = 2020, doi = "10.1007/978-3-030-45237-7_11"}
- Details
- Category: Publications 2020
Julian Parsert, Stephanie Autherith, Cezary Kaliszyk
6th Global Conference on Artificial Intelligence (GCAI 2020), EPiC Series in Computing 72, pp. 70 – 82, 2020.
Abstract
Logical reasoning as performed by human mathematicians involves an intuitive under- standing of terms and formulas. This includes properties of formulas themselves as well as relations between multiple formulas. Although vital, this intuition is missing when supplying atomically encoded formulae to (neural) down-stream models. In this paper we construct continuous dense vector representations of first-order logic which preserve syntactic and semantic logical properties. The resulting neural formula embeddings encode six characteristics of logical expressions present in the training-set and further generalise to properties they have not explicitly been trained on. To facilitate training, evaluation, and comparing of embedding models we extracted and generated data sets based on TPTP’s first-order logic library. Furthermore we examine the expressiveness of our encodings by conducting toy-task as well as more practical deployment tests.
BibTex
@inproceedings{jpsack-gcai20, author = {Julian Parsert and Stephanie Autherith and Cezary Kaliszyk}, title = {Property Preserving Embedding of First-order Logic}, booktitle = {6th Global Conference on Artificial Intelligence (GCAI 2020)}, editor = {Gregoire Danoy and Jun Pang and Geoff Sutcliffe}, series = {EPiC Series in Computing}, volume = {72}, pages = {70--82}, year = {2020}, publisher = {EasyChair}, url = {https://easychair.org/publications/paper/Cwgq}, doi = {10.29007/18t1}}
- Details
- Category: Publications 2020
Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
12th International NASA Formal Methods Symposium (NFM 2020), LNCS 12229, pp. 233 – 250, 2020.
doi:10.1007/978-3-030-55754-6_14 AFP entry
Abstract
We implement a decision procedure for linear mixed integer arithmetic and formally verify its soundness in Isabelle/HOL. We further integrate this procedure into one application, namely into CeTA, a formally verified certifier to check untrusted termination proofs. This checking involves assertions of unsatisfiability of linear integer inequalities; previously, only a sufficient criterion for such checks was supported. To verify the soundness of the decision procedure, we first formalize the proof that every satisfiable set of linear integer inequalities also has a small solution, and give explicit upper bounds. To this end we mechanize several important theorems on linear programming, including statements on integrality and bounds. The procedure itself is then implemented as a branch-and-bound algorithm, and is available in several languages via Isabelle’s code generator. It internally relies upon an adapted version of an existing verified incremental simplex algorithm.
BibTex
@inproceedings{RBMHARRT20, author = {Ralph Bottesch and Max W. Haslbeck and Alban Reynaud and Ren\'e Thiemann}, editor = {Ritchie Lee and Susmit Jha and Anastasia Mavridou}, title = {Verifying a Solver for Linear Mixed Integer Arithmetic in {I}sabelle/{HOL}}, booktitle = {12th International NASA Formal Methods Symposium (NFM 2020)}, series = {LNCS}, volume = {12229}, pages = {233--250}, publisher = {Springer}, year = {2020}, doi = {10.1007/978-3-030-55754-6_14}}
- Details
- Category: Publications 2020
Christian Sternagel, René Thiemann
Archive of Formal Proofs 2020.
Abstract
We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.
BibTex
@article{Knuth_Bendix_Order-AFP, author = {Christian Sternagel and René Thiemann}, title = {A Formalization of Knuth–Bendix Orders}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{https://isa-afp.org/entries/Knuth_Bendix_Order.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2020
René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J.C. Joosten, Akihisa Yamada
Journal of Automated Reasoning 64, pp. 827 – 856, 2020.
pdf doi:10.1007/s10817-020-09552-1
Creative Commons License (CC BY 4.0)
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 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.
BibTex
@inproceedings{RTRBJD-JAR20, author = "René Thiemann and Ralph Bottesch and Jose Divasón and Max W. Haslbeck and Sebastiaan J.C. Joosten and Akihisa Yamada", title = "Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL", series = "J Autom Reasoning", volume = 64, pages = "827--856", year = 2020, doi = "10.1007/s10817-020-09552-1"}
- Details
- Category: Publications 2020
Rene Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 4:1 – 4:20, 2020.
pdf doi:10.4230/LIPIcs.FSCD.2020.4
Abstract
The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.
BibTex
@InProceedings{thiemann_et_al:LIPIcs:2020:12326, author = {Ren{\'e} Thiemann and Jonas Sch{\"o}pf and Christian Sternagel and Akihisa Yamada}, title = {{Certifying the Weighted Path Order (Invited Talk)}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {4:1--4:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Zena M. Ariola}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12326}, URN = {urn:nbn:de:0030-drops-123263}, doi = {10.4230/LIPIcs.FSCD.2020.4}, annote = {Keywords: certification, Isabelle/HOL, reduction order, termination analysis}}
- Details
- Category: Publications 2020
Vincent van Oostrom
9th International Workshop on Confluence (IWC 2020), pp. 5, 2020.
BibTex
@inproceedings{Oost:20, author = {Oostrom, V. van}, title = {Some symmetries of commutation diamonds}, booktitle = {Proceedings of the 9th International Workshop on Confluence (IWC 2020), Paris, France}, pages = {1-5}, editors = {Ayala-Rincón, M. and Mimram, S.}, year = 2020}
- Details
- Category: Publications 2020
Cezary Kaliszyk, Florian Rabe
Intelligent Computer Mathematics (CICM 2020), LNCS 12236, pp. 138 – 156, 2020.
pdf doi:10.1007/978-3-030-53518-6_9
Abstract
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce human-readable documents. These goals are challenging to combine and state-of-the-art tools typically have make difficult compromises. In this paper we discuss languages that have been created for this purpose, including logical languages of proof assistants and other formal systems, semi-formal languages, intermediate languages for exchanging mathematical knowledge, and language frameworks that allow building customized languages. We evaluate their advantages based on our experience in designing and applying languages and tools for formalizing mathematics. We reach the conclusion that no existing language is truly good enough yet and derive ideas for possible future improvements.
BibTex
@inproceedings{ckfr-cicm20, author = {Cezary Kaliszyk and Florian Rabe}, title = {A Survey of Languages for Formalizing Mathematics}, booktitle = {Intelligent Computer Mathematics (CICM 2020)}, year = {2020}, series = {LNCS}, pages = {138--156}, url = {https://doi.org/10.1007/978-3-030-53518-6_9}, doi = {10.1007/978-3-030-53518-6_9}, publisher = {Springer, Cham}, volume = {12236}, editor = {Benzmueller C., Miller B.}, }
- Details
- Category: Publications 2020
Stanisław Purgał
International Joint Conference on Neural Networks (IJCNN), pp. 1 – 7, 2020.
pdf doi:10.1109/IJCNN48605.2020.9206591
Abstract
We propose a Graph Neural Network with greater expressive power than commonly used GNNs – not constrained to only differentiate between graphs that Weisfeiler-Lehman test recognizes to be non-isomorphic. We use a graph attention network with expanding attention window that aggregates information from nodes exponentially far away. We also use partially random initial embeddings, allowing differentiation between nodes that would otherwise look the same. This could cause problem with a traditional dropout mechanism, therefore we use a “head dropout”, randomly ignoring some attention heads rather than some dimensions of the embedding.
BibTex
@Article{Lang2020, author={Lang, Jan and Musil, V{\'{\i}}t and Ol{\v{s}}{\'a}k, Miroslav and Pick, Lubo{\v{s}}}, title={Maximal Non-compactness of Sobolev Embeddings}, journal={The Journal of Geometric Analysis}, year={2020}, month={Oct}, day={12}, issn={1559-002X}, doi={10.1007/s12220-020-00522-y}, url={https://doi.org/10.1007/s12220-020-00522-y}}
- Details
- Category: Publications 2020
Jan Lang, Vít Musil, Miroslav Olšák, Luboš Pick
The Journal of Geometric Analysis 31, pp. 9406 - 9431, 2020.
pdf doi:10.1007/s12220-020-00522-y
BibTex
@Article{Lang2020, author={Lang, Jan and Musil, V{\'{\i}}t and Ol{\v{s}}{\'a}k, Miroslav and Pick, Lubo{\v{s}}}, title={Maximal Non-compactness of Sobolev Embeddings}, journal={The Journal of Geometric Analysis}, year={2020}, month={Oct}, day={12}, issn={1559-002X}, doi={10.1007/s12220-020-00522-y}, url={https://doi.org/10.1007/s12220-020-00522-y}}
- Details
- Category: Publications 2020
Miroslav Olšák, Cezary Kaliszyk, Josef Urban
24th European Conference on Artificial Intelligence (ECAI 2020), Frontiers in Artificial Intelligence and Applications 325, pp. 1395 – 1402, 2020.
pdf doi:10.3233/FAIA200244 IOS Press
Abstract
Automated reasoning and theorem proving have recently become major challenges for machine learning. In other domains, representations that are able to abstract over unimportant transformations, such as abstraction over translations and rotations in vision, are becoming more common. Standard methods of embedding mathematical formulas for learning theorem proving are however yet unable to handle many important transformations. In particular, embedding previously unseen labels, that often arise in definitional encodings and in Skolemization, has been very weak so far. Similar problems appear when transferring knowledge between known symbols. We propose a novel encoding of formulas that extends existing graph neural network models. This encoding represents symbols only by nodes in the graph, without giving the network any knowledge of the original labels. We provide additional links between such nodes that allow the network to recover the meaning and therefore correctly embed such nodes irrespective of the given labels. We test the proposed encoding in an automated theorem prover based on the tableaux connection calculus, and show that it improves on the best characterizations used so far. The encoding is further evaluated on the premise selection task and a newly introduced symbol guessing task, and shown to correctly predict 65% of the symbol names.
BibTex
@inproceedings{mockju-ecai20, author = {Miroslav Ols{\'{a}}k and Cezary Kaliszyk and Josef Urban}, editor = {Giuseppe De Giacomo and Alejandro Catal{\'{a}} and Bistra Dilkina and Michela Milano and Sen{\'{e}}n Barro and Alberto Bugar{\'{\i}}n and J{\'{e}}r{\^{o}}me Lang}, title = {Property Invariant Embedding for Automated Reasoning}, booktitle = {{ECAI} 2020 - 24th European Conference on ArtificialIntelligence}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {325}, pages = {1395--1402}, publisher = {{IOS} Press}, year = {2020}, url = {https://doi.org/10.3233/FAIA200244}, doi = {10.3233/FAIA200244},}
- Details
- Category: Publications 2020