---
title: "Automated Theorem Proving in Intuitionistic Propositional Logic"
description: "The authors frame proving theorems in intuitionistic propositional logic (IPL) as a search problem: the… 25 references, cited by 6 papers here."
authors: ["Mitsuru Kusumoto", "Keisuke Yahata", "Masahiro Sakai"]
year: 2018
venue: "arXiv:1811.00796"
source: "https://arxiv.org/abs/1811.00796"
doi: "10.48550/arxiv.1811.00796"
arxiv: "1811.00796"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/kusumoto-2018-automated-theorem-proving-intuitionistic-propositional/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kusumoto-2018-automated-theorem-proving-intuitionistic-propositional/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2018](https://md.research.elamur.ai/free/en/papers/2018/page/7/) / Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

# Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

**Authors:** Mitsuru Kusumoto, Keisuke Yahata and Masahiro Sakai · **Year:** 2018 · **Venue:** arXiv:1811.00796 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1811.00796) · [PDF](https://arxiv.org/pdf/1811.00796v1) · [DOI 10.48550/arxiv.1811.00796](https://doi.org/10.48550/arxiv.1811.00796) · [arXiv 1811.00796](https://arxiv.org/abs/1811.00796) · [OpenAlex](https://openalex.org/W2899482370)

**Citations:** 9 citations (OpenAlex, 2026-10-14) · [6](https://md.research.elamur.ai/free/en/papers/kusumoto-2018-automated-theorem-proving-intuitionistic-propositional/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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:**

  | Prover | 1 s | 3 s | 10 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.*

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/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.

```bibtex
@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}
}
```

- [← previous When data permutations are pathological: the case of neural natural language inference](https://md.research.elamur.ai/free/en/papers/schluter-2018-when-data-permutations-are-pathological/)
- [next → Derivational Relations in Arabic WordNet](https://md.research.elamur.ai/free/en/papers/batita-2018-derivational-relations-arabic-wordnet/)
- [↑ back to papers of 2018](https://md.research.elamur.ai/free/en/papers/2018/page/7/)

## 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](https://md.research.elamur.ai/free/en/papers/allamanis-2017-learning-represent-programs-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](https://scholar.google.com/scholar?q=An+EATCS+Series%2E+Springer%2E+Bowman%2C+S%2E+R%2E%3B+Gauthier%2C+J%2E%3B+Rastogi%2C+A%2E%3B+Gupta%2C+R%2E%3B+Manning%2C+C%2E+D%2E%3B+and+Potts%2C+C%2E+2016%2E+A+fast+unified+model+for+parsing+and+sentence+understanding%2E+In+Proceedings+of+the+A)
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](https://scholar.google.com/scholar?q=Buss%2C+S%2E+R%2E+1998%2E+An+introduction+to+proof+theory%2E+In+Buss%2C+S%2E+R%2E%2C+ed%2E%2C+Handbook+of+proof+theory%2C+volume+137%2E+Elsevier%2C+Amsterdam%2E+1%E2%80%9378%2E)
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](https://scholar.google.com/scholar?q=Chung%2C+J%2E%3B+Gulcehre%2C+C%2E%3B+Cho%2C+K%2E%3B+and+Bengio%2C+Y%2E+2014%2E+Empirical+evaluation+of+gated+recurrent+neural+networks+on+sequence+modeling%2E+arXiv+preprint+arXiv%3A1412%2E3555%2E)
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](https://md.research.elamur.ai/free/en/papers/duvenaud-2015-convolutional-networks-graphs-learning-molecular/). 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](https://scholar.google.com/scholar?q=Dyckhoff%2C+R%2E+1992%2E+Contraction%2Dfree+sequent+calculi+for+intuitionistic+logic%2E+The+Journal+of+Symbolic+Logic+57%283%29%3A795%E2%80%93+807%2E)
7. Evans, R.; Saxton, D.; Amos, D.; Kohli, P.; and Grefenstette, E. 2018. [Can neural networks understand logical entailment?](https://md.research.elamur.ai/free/en/papers/evans-2018-can-neural-networks-understand-logical/) 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](https://scholar.google.com/scholar?q=Ferrari%2C+M%2E%3B+Fiorentini%2C+C%2E%3B+and+Fiorino%2C+G%2E+2010%2E+fCube%3A+An+efficient+prover+for+intuitionistic+propositional+logic%2E+In+International+Conference+on+Logic+for+Programming+Artificial+Intelligence+and+R)
9. Hochreiter, S., and Schmidhuber, J. 1997. Long short-term memory. Neural Computation 9(8):1735–1780. [find](https://scholar.google.com/scholar?q=Hochreiter%2C+S%2E%2C+and+Schmidhuber%2C+J%2E+1997%2E+Long+short%2Dterm+memory%2E+Neural+Computation+9%288%29%3A1735%E2%80%931780%2E)
10. Huang, D.; Dhariwal, P.; Song, D.; and Sutskever, I. 2018. [Gamepad: A learning environment for theorem proving](https://md.research.elamur.ai/free/en/papers/huang-2018-gamepad-learning-environment-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](https://md.research.elamur.ai/free/en/papers/kaliszyk-2017-holstep-machine-learning-dataset-higher/). 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](https://scholar.google.com/scholar?q=Lagoudakis%2C+M%2E+G%2E%2C+and+Parr%2C+R%2E+2003%2E+Least%2Dsquares+policy+iteration%2E+Journal+of+Machine+Learning+Research+%28JMLR%29+4%3A1107%E2%80%931149%2E)
13. Lederman, G.; Rabe, M. N.; and Seshia, S. A. 2018. [Learning heuristics for automated reasoning through deep reinforcement learning](https://md.research.elamur.ai/free/en/papers/lederman-2018-learning-heuristics-quantified-boolean-formulas/). 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](https://scholar.google.com/scholar?q=Li%2C+Y%2E%3B+Tarlow%2C+D%2E%3B+Brockschmidt%2C+M%2E%3B+and+Zemel%2C+R%2E+S%2E+2016%2E+Gated+graph+sequence+neural+networks%2E+In+International+Conference+on+Learning+Representations+%28ICLR%29%2E)
15. Loos, S. M.; Irving, G.; Szegedy, C.; and Kaliszyk, C. 2017. [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-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](https://scholar.google.com/scholar?q=Raths%2C+T%2E%3B+Otten%2C+J%2E%3B+and+Kreitz%2C+C%2E+2007%2E+The+ILTP+problem+library+for+intuitionistic+logic%2E+Journal+of+Automated+Reasoning+38%281%2D3%29%3A261%E2%80%93271%2E)
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](https://scholar.google.com/scholar?q=Sekiyama%2C+T%2E%2C+and+Suenaga%2C+K%2E+2018%2E+Automated+proof+synthesis+for+propositional+logic+with+deep+neural+networks%2E+arXiv+preprint+arXiv%3A1805%2E11799%2E+%E2%80%94+%5BarXiv%3A1805%2E11799%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1805%2E11799%29)
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](https://md.research.elamur.ai/free/en/papers/selsam-2018-learning-sat-solver-single-bit/). 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](https://scholar.google.com/scholar?q=Silver%2C+D%2E%3B+Huang%2C+A%2E%3B+Maddison%2C+C%2E+J%2E%3B+Guez%2C+A%2E%3B+Sifre%2C+L%2E%3B+van+den+Driessche%2C+G%2E%3B+Schrittwieser%2C+J%2E%3B+Antonoglou%2C+I%2E%3B+Panneershelvam%2C+V%2E%3B+Lanctot%2C+M%2E%3B+Dieleman%2C+S%2E%3B+Grewe%2C+D%2E%3B+Nham%2C+J%2E%3B+Kalchbrenner%2C)
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](https://md.research.elamur.ai/free/en/papers/al-2017-mastering-chess-shogi-self-play/). 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](https://scholar.google.com/scholar?q=Silver%2C+D%2E%3B+Schrittwieser%2C+J%2E%3B+Simonyan%2C+K%2E%3B+Antonoglou%2C+I%2E%3B+Huang%2C+A%2E%3B+Guez%2C+A%2E%3B+Hubert%2C+T%2E%3B+Baker%2C+L%2E%3B+Lai%2C+M%2E%3B+Bolton%2C+A%2E%3B+Chen%2C+Y%2E%3B+Lillicrap%2C+T%2E%3B+Hui%2C+F%2E%3B+Sifre%2C+L%2E%3B+van+den+Driessche%2C+G%2E%3B+Graepe)
22. Sutton, R. S., and Barto, A. G. 1998. Reinforcement learning: An introduction, volume 1. MIT Press Cambridge. [find](https://scholar.google.com/scholar?q=Sutton%2C+R%2E+S%2E%2C+and+Barto%2C+A%2E+G%2E+1998%2E+Reinforcement+learning%3A+An+introduction%2C+volume+1%2E+MIT+Press+Cambridge%2E)
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](https://scholar.google.com/scholar?q=Tokui%2C+S%2E%3B+Oono%2C+K%2E%3B+Hido%2C+S%2E%3B+and+Clayton%2C+J%2E+2015%2E+Chainer%3A+A+next%2Dgeneration+open+source+framework+for+deep+learning%2E+In+Proceedings+of+Workshop+on+Machine+Learning+Systems+%28LearningSys%29+in+Neural+)
24. Wang, M.; Tang, Y.; Wang, J.; and Deng, J. 2017. [Premise selection for theorem proving by deep graph embedding](https://md.research.elamur.ai/free/en/papers/wang-2017-premise-selection-theorem-proving-deep/). In Advances in Neural Information Processing Systems (NIPS), 2786–2796.
25. Whalen, D. 2016. [Holophrasm: A neural automated theorem prover for higher-order logic](https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/). arXiv preprint arXiv:1608.02644.

*Updated 3 November 2026*