text: We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.
  @cite_18: In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner. Hence, they provide an opportunity to explore theorem proving with human supervision. We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem. We address position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step) tasks, which arise naturally in tactic-based theorem proving.
  @cite_34: The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.
  @cite_22: A photographic copying machine of the type in which exposure radiation is transmitted through a transparent original onto a photosensitive medium. Arranged in the exposure radiation path is an array of multitudinous controllable-transmissivity elements, the individual transmissivity values of which are individually controllable. A control electronics, preferably incorporating a computer and multiplexer, controls the transmissivity values of the multitude of controllable-transmissivity elements of the array. The transmissivity values to which the multitude of elements are set can be equal, but in accordance with the present invention are not; instead, the array is employed to establish a two-dimensional controllably non-uniform distribution of exposure radiation onto the photosensitive medium. This is done to implement non-uniform density and or color correction during printing, or to superimpose onto the image projected onto the photosensitive medium images of symbols, text, or the like, which are to be appear on the final copy, or to implement border effects, by way of example.
  @cite_20: Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences com- bined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39 percent of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32 percent in the same amount of time.
summary: The earliest work of applying machine learning on reasoning in large theories is @cite_22 . The most most similar works to ours are TacticToe @cite_20 and GamePad @cite_18 . TacticToe is the first published result on machine learning tackling higher-order theorem proving at a relatively large scale at tactic level @cite_20 . Although TacticToe is a great success that came with significant improvements over previous automated theorem proving systems, they do not propose an easy to use benchmark or environment for machine learning researchers. TacticToe does not employ deep learning nor reinforcement learning. They rely on the HOL4 @cite_34 system that has a significantly less theorems with more complex human proof scripts with a larger number of more elementary tactics.