Elamur Research⌕
☰
home / papers / 2019 / Guiding Inferences in Connection Tableau by Recurrent Neural Networks

Guiding Inferences in Connection Tableau by Recurrent Neural Networks

Paper · 2019 · Bartosz Piotrowski and Josef Urban

Summary

Connection-style theorem provers such as leanCoP must repeatedly decide which input clause to use when extending an open branch of the proof tree. Poor choices lead to wasted search and backtracking. The authors treat this decision as a sequence-to-sequence problem. They extracted 13,822 connection proofs of Mizar Mathematical Library (MML) problems, translated to TPTP. From these proofs they built training pairs that map either the literals or the clauses along a branch to the clause that was actually used next. Variables and Skolem functions were normalized to the tokens VAR and SKLM. A neural machine translation model (Luong et al.) encodes the branch into a hidden state and decodes one or more clause choices. The literal-based input performed best, and accuracy increased with branch length. The model clearly outperformed a feature-based XGBoost baseline on longer paths. A further experiment had the model generate the next literal symbol by symbol, which ranking methods cannot do. The results suggest that encoding the evolving proof state with recurrent networks is a promising basis for internal prover guidance.

Key points

  • The dataset contains 567,273 (path, next clause) pairs for each input type, plus variants that predict 2–3 consecutive clauses. Proofs were split 0.6/0.1/0.3 for train/validation/test, and the data is released on GitHub (BartoszPiotrowski/guiding-connection-tableau-by-RNNs).
  • Predicting the next clause from literal paths reached 0.64 accuracy (top-1) and 0.72 (top-10). Clause paths gave only 0.17 and 0.36. Predicting two or three steps ahead was much weaker, at 0.11 and 0.05 top-1.
  • NMT accuracy grew with input length and reached 0.85 for paths of length 8.
  • The XGBoost multilabel baseline was trained on the MPTP2078 subset, which has 1383 clause labels. It averaged 0.43 and never exceeded 0.51. It did better than NMT only on very short paths.
  • Conjecturing literals from 6442 available symbols achieved 0.08 accuracy overall and up to 0.34 on longer inputs. Long literals were often wrong or syntactically malformed.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of WarsawWarsaw · Poland14 works · 774 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Bartosz Piotrowski and Josef Urban. 2019. Guiding Inferences in Connection Tableau by Recurrent Neural Networks. arXiv:1905.07961.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1905.07961 · arXiv 1905.07961

@misc{piotrowski2019guiding,
  title = {{Guiding Inferences in Connection Tableau by Recurrent Neural Networks}},
  author = {Bartosz Piotrowski and Josef Urban},
  year = {2019},
  doi = {10.48550/arxiv.1905.07961},
  eprint = {1905.07961},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.07961}
}

References

16 references, 9 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: ACM SIGKDD 2016, pp. 785–794 (2016) find
  2. Cho, K., van Merrienboer, B., Gülçehre, Ç., Bahdanau, D., Bougares, F., Schwenk, H., Bengio, Y.: Learning phrase representations using RNN encoder-decoder for statistical machine translation. In: EMNLP 2014, pp. 1724–1734 (2014) — Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation
  3. Chvalovský, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E. In: CADE 27, pp. 197–215 (2019)
  4. Evans, R., Saxton, D., Amos, D., Kohli, P., Grefenstette, E.: Can neural networks understand logical entailment? In: ICLR 2018 (2018)
  5. Freitag, M., Al-Onaizan, Y.: Beam search strategies for neural machine translation. In: NMT@ACL 2017, pp. 56–60 (2017)
  6. Gauthier, T.: Deep reinforcement learning for synthesizing functions in higher-order logic. CoRR (2019), http://arxiv.org/abs/1910.11797 ↗
  7. Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153–245 (2010) find
  8. Kaliszyk, C., Chollet, F., Szegedy, C.: Holstep: A machine learning dataset for higher-order logic theorem proving. In: ICLR 2017 (2017)
  9. Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS 2018, pp. 8836–8847 (2018)
  10. Lample, G., Charton, F.: Deep learning for symbolic mathematics. CoRR (2019), http://arxiv.org/abs/1912.01412 ↗
  11. Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableau calculi. J. Autom. Reasoning 13, 297–337 (1994) find
  12. Luong, M., Brevdo, E., Zhao, R.: Neural machine translation (seq2seq) tutorial (2017), https://github.com/tensorflow/nmt ↗
  13. Otten, J., Bibel, W.: leanCoP: Lean connection-based theorem proving. J. Symbolic Computation 36(1-2), 139–161 (2003) find
  14. Piotrowski, B., Urban, J., Brown, C.E., Kaliszyk, C.: Can neural networks learn symbolic rewriting? CoRR (2019), https://arxiv.org/pdf/1911.04873.pdf — [arXiv:1911.04873](https://arxiv.org/abs/1911.04873) ↗
  15. Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Automated Reasoning 37(1-2), 21–43 (2006) find
  16. Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: CICM 2018, pp. 255–270 (2018)

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/piotrowski-2019-guiding-inferences-connection-tableau-recurrent/