Dennis Müller and Cezary Kaliszyk
International Conference on Learning Representations (ICLR), pp. 16, 2021
- Details
- Category: Publications 2021
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 250 – 263, 2021.
pdf 
doi:10.1145/3437992.3439918
Abstract
The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems, implemented in FORT. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a more expressive theory and is based on the concept of anchored ground tree transducers. The correctness of the decision procedure is verified by a formalization in Isabelle/HOL on top of the Isabelle Formalization of Rewriting (IsaFoR).
BibTex
@inproceedings{ALAMFMBF-CPP21, author = "Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer", title = "A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems", booktitle = "Proceedings of the 10th International {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs", publisher = "ACM", editors = "Cătălin Hriţcu and Andrei Popescu", pages = "250--263", doi = "10.1145/3437992.3439918", year = 2021}
- Details
- Category: Publications 2021
Max Haslbeck, Rene Thiemann
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 238 – 249, 2021.
pdf doi:10.1145/3437992.3439935
Abstract
AProVE is a powerful termination prover for various programming languages, including a termination analysis method for imperative programs specified in the LLVM intermediate representation (IR). The method internally works in three steps: first, it transforms LLVM IR code into a symbolic execution graph; second, the graph is translated into an integer transition system; finally, termination of the transition system is proved by the back end of AProVE. Since AProVE is unverified software, our aim is to increase its reliability by certifying the generated proofs. To this end, we require formal semantics of all program representations, i.e., for LLVM IR, for symbolic execution graphs and for integer transition systems. As the latter is already available, we define the former ones. We note that our semantics for LLVM IR use arithmetic with unbounded integers. We further verify the first and the second step of AProVE’s termination method, including verified algorithms to check concrete proofs. Since the third step can already be certified, we obtain a complete formally verified method for certifying AProVE’s termination proofs of LLVM IR programs. The whole formalization has been done in Isabelle/HOL and our certifier is available as a Haskell program via code generation.
BibTex
@inproceedings{10.1145/3437992.3439935, author = {Haslbeck, Max W. and Thiemann, Ren\'{e}}, title = {An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR}, year = {2021}, isbn = {9781450382991}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3437992.3439935}, doi = {10.1145/3437992.3439935}, pages = {238–249}, numpages = {12}, keywords = {static program analysis, Isabelle/HOL, termination analysis, formal verification}, location = {Virtual, Denmark}, series = {CPP 2021}}
- Details
- Category: Publications 2021
Miroslav Olšák
The Journal of Symbolic Logic pp. 20, 2021.
BibTex
@article{olšák_2021, title={MALTSEV CONDITIONS FOR GENERAL CONGRUENCE MEET-SEMIDISTRIBUTIVE ALGEBRAS}, DOI={10.1017/jsl.2021.14}, journal={The Journal of Symbolic Logic}, publisher={Cambridge University Press}, author={OLŠÁK, MIROSLAV}, year={2021}, pages={1–20}}
- Details
- Category: Publications 2021
Stanisław Purgał, Julian Parsert, Cezary Kaliszyk
Journal of Logic and Computation pp. 27, 2021.
pdf doi:10.1093/logcom/exab006
BibTex
@article{spjpck-jlc21, author = {Purgał, Stanisław and Parsert, Julian and Kaliszyk, Cezary}, title = {A study of continuous vector representations for theorem proving}, journal = {Journal of Logic and Computation}, month = {02}, year = {2021}, issn = {0955-792X}, doi = {10.1093/logcom/exab006}, url = {https://doi.org/10.1093/logcom/exab006},}
- Details
- Category: Publications 2021
René Thiemann
Archive of Formal Proofs 2021.
Abstract
We formally define sunflowers and provide a formalization of the sunflower lemma of Erdős and Rado: whenever a set of size-k-sets has a larger cardinality than (r – 1)^k * k!, then it contains a sunflower of cardinality r.
BibTex
@article{Sunflowers-AFP, author = {René Thiemann}, title = {The Sunflower Lemma of Erdős and Rado}, journal = {Archive of Formal Proofs}, month = feb, year = 2021, note = {\url{https://isa-afp.org/entries/Sunflowers.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2021
Ralph Bottesch, Jose Divasón, René Thiemann
Archive of Formal Proofs 2021.
Abstract
We verify two algorithms for which modular arithmetic plays an essential role: Storjohann’s variant of the LLL lattice basis reduction algorithm and Kopparty’s algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann’s paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.
BibTex
@article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP, author = {Ralph Bottesch and Jose Divasón and René Thiemann}, title = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation}, journal = {Archive of Formal Proofs}, month = mar, year = 2021, note = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2021
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer
27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), LNCS 12652, pp. 127 – 144, 2021.
pdf doi:10.1007/978-3-030-72013-1_7
Abstract
The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify.
BibTex
@inproceedings{MLMF-TACAS21, author = "Fabian Mitterwallner and Alexander Lochmann and Aart Middeldorp and Bertram Felgenhauer", title = "Certifying Proofs in the First-Order Theory of Rewriting", booktitle = "Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Jan Friso Groote and Kim Guldstrand Larsen", series = "Lecture Notes in Computer Science", volume = 12652, pages = "127--144", year = 2021, doi = "10.1007/978-3-030-72013-1_7"}
- Details
- Category: Publications 2021
Yutaka Nagashima
PhD thesis, University of Innsbruck 2021.
pdf doi:10.1016/j.jlamp.2021.100699
Copyright: the author
BibTex
@phdthesis{YN18, author = "Yutaka Nagashima", title = "Artificial Intelligence andDomain-Specific Languagesfor Interactive Theorem Proving", school = "University of Innsbruck", year = 2021 }
- Details
- Category: Publications 2021
René Thiemann
Journal of Logical and Algebraic Methods in Programming 123, 2021.
doi:10.1016/j.jlamp.2021.100699
Abstract
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. There exists a conceptually simple algorithm to determine the growth rate, but this algorithm has the disadvantage that it is based on algebraic number computations. In this work we present an even simpler algorithm to compute the growth rate. Its soundness is based on a variant of a Perron–Frobenius theorem that has been conjectured in earlier work. So far it only has been proven for small matrices, and here we present a proof for the general case. We further verify both the algorithm and the new Perron–Frobenius theorem in the proof assistant Isabelle/HOL, and integrate it into CeTA, a verified certifier for various properties, including complexity proofs. Because of the new results, CeTA no longer requires a verified implementation of algebraic numbers.
BibTex
@article{Thi21, author = {Ren\'e Thiemann}, title = {A {P}erron--{F}robenius theorem for deciding matrix growth}, journal = {J. Log. Algebraic Methods Program.}, volume = {123}, year = {2021}, doi = {10.1016/j.jlamp.2021.100699}}
- Details
- Category: Publications 2021
Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, Josef Urban
International Joint Conference on Automated Reasoning (IJCAR), pp. 448 - 463, 2020.
pdf doi:10.1007/978-3-030-51054-1_29
BibTex
@InProceedings{10.1007/978-3-030-51054-1_29, author="Jakub{\r{u}}v, Jan and Chvalovsk{\'y}, Karel and Ol{\v{s}}{\'a}k, Miroslav and Piotrowski, Bartosz and Suda, Martin and Urban, Josef", editor="Peltier, Nicolas and Sofronie-Stokkermans, Viorica", title="ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)", booktitle="Automated Reasoning", year="2020", publisher="Springer International Publishing", address="Cham", pages="448--463", isbn="978-3-030-51054-1"}
- Details
- Category: Publications 2021
Vincent van Oostrom
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Leibniz International Proceedings in Informatics (LIPIcs) 195, pp. 24:1 - 24:22, 2021.
pdf doi:10.4230/LIPIcs.FSCD.2021.24
BibTex
@InProceedings{vanoostrom:LIPIcs.FSCD.2021.24, author = {van Oostrom, Vincent}, title = {{Z; Syntax-Free Developments}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {24:1--24:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14262}, URN = {urn:nbn:de:0030-drops-142620}, doi = {10.4230/LIPIcs.FSCD.2021.24}, annote = {Keywords: rewrite system, confluence, normalisation, recurrence}}
- Details
- Category: Publications 2021
Qingxiang Wang, Cezary Kaliszyk
Frontiers of Combining Systems – 13th International Symposium, FroCoS 2021, pp. 154-170, 2021.
pdf doi:10.1007/978-3-030-86205-3_9
Abstract
The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them difficult. In this paper, we compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts. Our approach is based on the fasttext implementation of Word2Vec, on top of which a tree traversal module is added to adapt its algorithm to the representation format of our data export pipeline. We compare the explainability, customizability, and online-servability of the approaches and argue that the neural embedding approach has more potential to be integrated into an interactive proof assistant.
BibTex
@inproceedings{qwck-frocos21, author = {Qingxiang Wang and Cezary Kaliszyk}, editor = {Boris Konev and Giles Reger}, title = {{JEFL:} {J}oint Embedding of Formal Proof Libraries}, booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021}, series = {LNCS}, volume = {12941}, pages = {154--170}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-86205-3\_9}, doi = {10.1007/978-3-030-86205-3\_9},}
- Details
- Category: Publications 2021
Miroslav Olšák
International Congress on Mathematical Software (ICMS 2020), pp. 263 - 271, 2020.
pdf doi:10.1007/978-3-030-52200-1_26
BibTex
@InProceedings{10.1007/978-3-030-52200-1_26, author="Ol{\v{s}}{\'a}k, Miroslav", editor="Bigatti, Anna Maria and Carette, Jacques and Davenport, James H. and Joswig, Michael and de Wolff, Timo", title="GeoLogic -- Graphical Interactive Theorem Prover for Euclidean Geometry", booktitle="Mathematical Software -- ICMS 2020", year="2020", publisher="Springer International Publishing", address="Cham", pages="263--271", abstract="Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the human-imitation approach: ATPs often use human-unfriendly logical foundations while ITPs are meant for formalizing existing proofs rather than problem solving. We aim to create a simple human-friendly logical system for mathematical problem solving. We picked the case study of Euclidean geometry as it can be easily visualized, has simple logic, and yet potentially offers many high-school problems of various difficulty levels. To make the environment user friendly, we abandoned strict logic required by ITPs, allowing to infer topological facts from pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar to GeoGebra, which allows users to interactively study and prove properties about the geometrical setup.", isbn="978-3-030-52200-1"}
- Details
- Category: Publications 2021
Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 17th International Workshop on Termination (WST 2021), pp. 21 - 26, 2021
BibTex
@inproceedings{FMAM-WST21, author = "Fabian Mitterwallner and Aart Middeldorp", title = "Polynomial Termination over {N} is Undecidable", booktitle = "Proceedings of the 17th International Workshop on Termination", pages = "21--26", year = 2021}
- Details
- Category: Publications 2021
Jan Jakubův, Mikoláš Janota, Andrew Reynolds
International Workshop on Satisfiability Modulo Theories (SMT), CEUR Workshop Proceedings 2908, 2021.
pdf doi:10.1007/978-3-030-81097-9_5
Copyright: authors, CC BY 4.0
Abstract
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician’s machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq’s standard library.
BibTex
@inproceedings{JJMJAR-CEURWS21, author = {Jan Jakubuv and Mikol{\'{a}}s Janota and Andrew Reynolds}, editor = {Alexander Nadel and Aina Niemetz}, title = {Characteristic Subsets of {SMT-LIB} Benchmarks}, booktitle = {Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), Online (initially located in Los Angeles, USA), July 18-19, 2021}, series = {{CEUR} Workshop Proceedings}, volume = {2908}, pages = {53--63}, publisher = {CEUR-WS.org}, year = {2021}, url = {http://ceur-ws.org/Vol-2908/paper7.pdf},}
- Details
- Category: Publications 2021
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Intelligent Computer Mathematics – 14th International Conference, CICM 2021, pp. 67-83, 2021.
pdf doi:10.1007/978-3-030-81097-9_5
Abstract
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician’s machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq’s standard library.
BibTex
@inproceedings{lzlbbppcckju-cicm21, author = {Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop Cern{\'{y}} and Cezary Kaliszyk and Josef Urban}, editor = {Fairouz Kamareddine and Claudio Sacerdoti Coen}, title = {Online Machine Learning Techniques for {C}oq: {A} Comparison}, booktitle = {Intelligent Computer Mathematics - 14th International Conference, {CICM} 2021}, series = {LNCS}, volume = {12833}, pages = {67--83}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-81097-9\_5}, doi = {10.1007/978-3-030-81097-9\_5},}
- Details
- Category: Publications 2021
Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 10th International Workshop on Confluence (IWC 2021), pp. 25 - 30, 2021.
BibTex
@inproceedings{ALFMAM-IWC21, author = "Alexander Lochmann and Fabian Mitterwallner and Aart Middeldorp", title = "Formalized Signature Extension Results for Confluence, Commutation and Unique Normal Forms", booktitle = "Proceedings of the 10th International Workshop on Confluence", pages = "25--30", year = 2021}
- Details
- Category: Publications 2021
Vincent van Oostrom
10th International Workshop on Confluence (IWC 2021), pp. 7, 2021.
BibTex
@InProceedings{Oost:21:mr, author = "Oostrom, V. van", title = "Multi-redexes and multi-treks induce residual systems; least upper bounds and left-cancellation up to homotopy", booktitle = {Proceedings of the 10th International Workshop on Confluence (IWC 2021)}, pages = {1-7} month = jul, editors = {Ayala-Rincón, M. and Mimram, S.}, year = 2021}
- Details
- Category: Publications 2021
Thibault Gauthier,Cezary Kaliszyk,Josef Urban,Ramana Kumar,Michael Norrish
Journal of Automated Reasoning 65, pp. 257 - 286, 2021.
pdf doi:10.1007/s10817-020-09580-x
BibTex
@article{tgckjurkmn-jar21, author = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban and Ramana Kumar and Michael Norrish}, title = {{TacticToe}: {L}earning to Prove with Tactics}, journal = {J. Autom. Reason.}, volume = {65}, number = {2}, pages = {257--286}, year = {2021}, url = {https://doi.org/10.1007/s10817-020-09580-x}, doi = {10.1007/s10817-020-09580-x},}
- Details
- Category: Publications 2021
Michael Färber, Cezary Kaliszyk, Josef Urban
Journal of Automated Reasoning 65, pp. 287 - 320, 2021.
pdf doi:10.1007/s10817-020-09576-7
BibTex
@article{mfckju-jar21, author = {Michael F{\"{a}}rber and Cezary Kaliszyk and Josef Urban}, title = {Machine Learning Guidance for Connection Tableaux}, journal = {J. Autom. Reason.}, volume = {65}, number = {2}, pages = {287--320}, year = {2021}, url = {https://doi.org/10.1007/s10817-020-09576-7}, doi = {10.1007/s10817-020-09576-7},}
- Details
- Category: Publications 2021