Deep networks are integrated directly into automated theorem-prover search

What happened?

Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk trained deep neural networks on existing automated proofs of Mizar statements and used them to guide processed-clause selection inside E prover. The paper reported finding first-order proofs for a subset of translated Mizar theorems that previously lacked ATP-generated proofs, increasing the corpus coverage with ATP proofs from about 56% to 59%.

The system learns from clause-level traces of successful automated proofs and ranks generated clauses during saturation-style proof search. Because neural evaluation is slower than hand-engineered heuristics, the authors used hybrid guidance and a two-phase search strategy that lets the learned model improve the search trajectory before faster conventional heuristics finish the proof attempt.

Why it matters

The work demonstrated that neural models could influence the inner loop of a mature automated theorem prover rather than acting only as an upstream filter. That distinction became important in later work on learned clause guidance, reinforcement-learning proof search and search-in-the-loop theorem proving.

Significance rationale: Deep Network Guided Proof Search was an important early step from learned premise selection toward learned control inside the proof search itself. By training neural models on Mizar-derived proof traces and inserting their predictions into E prover's processed-clause selection, the work established a concrete deep-learning route for internal automated-theorem-prover guidance before later reinforcement-learning and proof-assistant-native systems.

Historical context

Primary evidence

• Deep Network Guided Proof Search
  S1 · Primary research · Paper · 2017-01-24
• Deep Network Guided Proof Search — LPAR-21
  S1 · Primary research · Paper · 2017-05-04