Elamur Research⌕
☰
home / papers / 2018 / Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

Paper · 2018 · Mitsuru Kusumoto, Keisuke Yahata and Masahiro Sakai

Summary

The authors frame proving theorems in intuitionistic propositional logic (IPL) as a search problem: the prover builds a proof tree bottom-up using the inference rules of the sequent calculus LJT. Neural networks serve as value functions that decide which states to explore next. Public theorem libraries are small, at most a few thousand statements, so the authors train with approximate policy iteration (API) and add a data augmentation step at every iteration. This step turns a small library into millions of training examples. The value functions are graph neural networks (GNNs) that take formulas in a new compact graph encoding. This encoding captures syntactic structure and does not depend on variable names. Formulas in the experiments run to several hundred symbols. The trained prover was evaluated on a held-out exam library against Coq's tauto tactic and an untrained baseline. With a 10-second limit it proved 84% of the theorems, compared with 52% for tauto. This is quantitative evidence that learned search guidance can beat hand-engineered heuristics, a comparison earlier neural ATP work rarely made.

Key points

  • Accuracy of value functions: GNNs reached a test error of about 0.04, while other architectures (e.g., RNN, BoW) stayed above 0.08. GNNs were only about 1.5× slower than RNNs at inference.

  • Design choices: Accuracy kept improving as the GNN step size increased up to T = 6. In the graph input format, term-merging (TM) outperformed variable-merging (VM).

  • Effect of augmentation: The initial policy π0 proved 41% of the training theorems. With augmentation, π2 reached about 85% and π4 86%. Without augmentation, performance fell to 24% and then 14%. The training set D3 held 1,753,080 examples, roughly twice the size of D0.

  • Exam results at 1 s / 3 s / 10 s:

    Prover1 s3 s10 s
    π4 (trained)60%78%84%
    Coq tauto (v8.7.1)35%43%52%
    Baseline π0 (greedy DFS)30%35%40%

  • Beyond the baselines: Under every time limit, the trained prover solved more than 25% of the theorems that neither baseline could prove.

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

 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 Mitsuru Kusumoto, Keisuke Yahata and Masahiro Sakai. 2018. Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning. arXiv:1811.00796.

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

@misc{kusumoto2018automated,
  title = {{Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning}},
  author = {Mitsuru Kusumoto, Keisuke Yahata and Masahiro Sakai},
  year = {2018},
  doi = {10.48550/arxiv.1811.00796},
  eprint = {1811.00796},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1811.00796}
}

References

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

  1. Allamanis, M.; Brockschmidt, M.; and Khademi, M. 2018. Learning to represent programs with graphs. In International Conference on Learning Representations (ICLR). Bertot, Y., and Castéran, P. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Construction…
  2. An EATCS Series. Springer. Bowman, S. R.; Gauthier, J.; Rastogi, A.; Gupta, R.; Manning, C. D.; and Potts, C. 2016. A fast unified model for parsing and sentence understanding. In Proceedings of the Association for Computational Linguistics (ACL), volume 1, 1466–1477. find
  3. Buss, S. R. 1998. An introduction to proof theory. In Buss, S. R., ed., Handbook of proof theory, volume 137. Elsevier, Amsterdam. 1–78. find
  4. Chung, J.; Gulcehre, C.; Cho, K.; and Bengio, Y. 2014. Empirical evaluation of gated recurrent neural networks on sequence modeling. arXiv preprint arXiv:1412.3555. find
  5. Duvenaud, D. K.; Maclaurin, D.; Iparraguirre, J.; Bombarell, R.; Hirzel, T.; Aspuru-Guzik, A.; and Adams, R. P. 2015. Convolutional networks on graphs for learning molecular fingerprints. In Advances in Neural Information Processing Systems (NIPS), 2224–2232.
  6. Dyckhoff, R. 1992. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic 57(3):795– 807. find
  7. Evans, R.; Saxton, D.; Amos, D.; Kohli, P.; and Grefenstette, E. 2018. Can neural networks understand logical entailment? In International Conference on Learning Representations (ICLR).
  8. Ferrari, M.; Fiorentini, C.; and Fiorino, G. 2010. fCube: An efficient prover for intuitionistic propositional logic. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, 294–301. Springer. find
  9. Hochreiter, S., and Schmidhuber, J. 1997. Long short-term memory. Neural Computation 9(8):1735–1780. find
  10. Huang, D.; Dhariwal, P.; Song, D.; and Sutskever, I. 2018. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608. Irving, G.; Szegedy, C.; Alemi, A. A.; Eén, N.; Chollet, F.; and Urban, J. 2016. DeepMath - deep sequence models for premise selection. In Advances in Neu…
  11. Kaliszyk, C.; Chollet, F.; and Szegedy, C. 2017. Holstep: A machine learning dataset for higher-order logic theorem proving. In International Conference on Learning Representations (ICLR).
  12. Lagoudakis, M. G., and Parr, R. 2003. Least-squares policy iteration. Journal of Machine Learning Research (JMLR) 4:1107–1149. find
  13. Lederman, G.; Rabe, M. N.; and Seshia, S. A. 2018. Learning heuristics for automated reasoning through deep reinforcement learning. arXiv preprint arXiv:1807.08058.
  14. Li, Y.; Tarlow, D.; Brockschmidt, M.; and Zemel, R. S. 2016. Gated graph sequence neural networks. In International Conference on Learning Representations (ICLR). find
  15. Loos, S. M.; Irving, G.; Szegedy, C.; and Kaliszyk, C. 2017. Deep network guided proof search. In 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, 85–105.
  16. Raths, T.; Otten, J.; and Kreitz, C. 2007. The ILTP problem library for intuitionistic logic. Journal of Automated Reasoning 38(1-3):261–271. find
  17. Sekiyama, T., and Suenaga, K. 2018. Automated proof synthesis for propositional logic with deep neural networks. arXiv preprint arXiv:1805.11799. — [arXiv:1805.11799](https://arxiv.org/abs/1805.11799) find
  18. Selsam, D.; Lamm, M.; Bunz, B.; Liang, P.; de Moura, L.; and Dill, D. L. 2018. Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685.
  19. Silver, D.; Huang, A.; Maddison, C. J.; Guez, A.; Sifre, L.; van den Driessche, G.; Schrittwieser, J.; Antonoglou, I.; Panneershelvam, V.; Lanctot, M.; Dieleman, S.; Grewe, D.; Nham, J.; Kalchbrenner, N.; Sutskever, I.; Lillicrap, T. P.; Leach, M.; Kavukcuoglu, K.; Graepel, T.; and Hassabis, D. 2016… find
  20. Silver, D.; Hubert, T.; Schrittwieser, J.; Antonoglou, I.; Lai, M.; Guez, A.; Lanctot, M.; Sifre, L.; Kumaran, D.; Graepel, T.; Lillicrap, T. P.; Simonyan, K.; and Hassabis, D. 2017a. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. arXiv preprint arXiv:1712.01…
  21. Silver, D.; Schrittwieser, J.; Simonyan, K.; Antonoglou, I.; Huang, A.; Guez, A.; Hubert, T.; Baker, L.; Lai, M.; Bolton, A.; Chen, Y.; Lillicrap, T.; Hui, F.; Sifre, L.; van den Driessche, G.; Graepel, T.; and Hassabis, D. 2017b. Mastering the game of Go without human knowledge. Nature 550(7676):35… find
  22. Sutton, R. S., and Barto, A. G. 1998. Reinforcement learning: An introduction, volume 1. MIT Press Cambridge. find
  23. Tokui, S.; Oono, K.; Hido, S.; and Clayton, J. 2015. Chainer: A next-generation open source framework for deep learning. In Proceedings of Workshop on Machine Learning Systems (LearningSys) in Neural Information Processing Systems (NIPS). find
  24. Wang, M.; Tang, Y.; Wang, J.; and Deng, J. 2017. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems (NIPS), 2786–2796.
  25. Whalen, D. 2016. Holophrasm: A neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kusumoto-2018-automated-theorem-proving-intuitionistic-propositional/