29 citations · 56 across the 17 of their papers we have counts for
5 papers · 1 filter
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka, Burak Ekici, Cezary Kaliszyk
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of…
First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
We report on our experiments to train deep neural networks that automatically translate informalized LaTeX-written Mizar texts into the formal Mizar language. To the best of our kn…
Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski +1
We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations gui…
Machine Learning Guidance and Proof Certification for Connection Tableaux
Michael Färber, Cezary Kaliszyk, Josef Urban
Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: First, we show opti…
Learning to Reason with HOL4 tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques com…