Elamur Research⌕
☰
home / papers / 2020 / Teaching Temporal Logics to Neural Networks

Teaching Temporal Logics to Neural Networks

Paper · 2020 · Christopher Hahn, Frederik Schmitt, Jens U. Kreber et al.

Summary

The paper tests two things. First, can a neural network solve a hard logical task end to end? Second, does it learn what the logic means, or does it only copy the tool that produced its training data? The task is finding a satisfying trace for a formula in linear-time temporal logic (LTL), a core problem in verification.

The authors build datasets of formula–trace pairs. Formulas are either conjunctions of the 55 specification patterns from Dwyer et al. or random formulas. Traces are finite "lasso" encodings of infinite sequences, generated with Büchi-automaton constructions from the spot framework. A propositional variant uses SAT solvers instead.

A Transformer is trained as a sequence-to-sequence model that outputs a trace directly. Each training formula has only one of many valid answers. Even so, the model produces correct traces for 96.8% of held-out pattern formulas and for 83% of formulas on which spot timed out. Many of its outputs differ from the solver's trace but still satisfy the formula, which suggests the network has learned the semantics. Learned models could therefore complement classical reasoning tools.

Key points

  • Datasets: LTLPattern126 (pattern conjunctions), LTLRandom35 / LTLRandom50 (random LTL formulas), LTLUnsolved254 (formulas where spot timed out) and PropRandom35 (propositional formulas labelled by SAT solvers).
  • Evaluation: The authors separate syntactic accuracy (the output matches the generator's trace) from semantic accuracy (the output is any correct trace). On LTLRandom35, the best model reaches 83.8% syntactic and 98.5% semantic accuracy.
  • Out-of-distribution behavior: On out-of-distribution inputs, almost no predicted trace equals the solver's solution, even though most predictions are correct.
  • Longer formulas: Tree-positional encodings (Shiv & Quirk, 2019) let the model handle formulas longer than those seen in training. The standard positional encoding does not.
  • Hyperparameters: Encoder/decoder depth matters most, with 8 layers working best. Raising both the number of heads and the feed-forward size gives a small gain. Changing either one alone, or the embedding size, helps little.

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

🏢GoogleMountain View · United States533 works · 443,885 citations🎓Saarland UniversitySaarbrücken · Germany153 works · 18,501 citations🔬Helmholtz Center for Information SecuritySaarbrücken · Germany22 works · 1,197 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe and Bernd Finkbeiner. 2020. Teaching Temporal Logics to Neural Networks. arXiv:2003.04218.

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

@misc{hahn2020teaching,
  title = {{Teaching Temporal Logics to Neural Networks}},
  author = {Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe and Bernd Finkbeiner},
  year = {2020},
  doi = {10.48550/arxiv.2003.04218},
  eprint = {2003.04218},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2003.04218}
}

References

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

  1. Miltiadis Allamanis, Marc Brockschmidt, and Mahmoud Khademi. Learning to represent programs with graphs. arXiv preprint arXiv:1711.00740, 2017.
  2. Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools, 27 (1):1840001:1–1840001:25, 2018. doi: 10.1142/S0218213018400018. URL https://doi.org/10.1142/S0218213018400018. — [doi:10.1142/s0218213018400018](https://doi.org/10.1142/s0218213018400018) ↗
  3. Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning to solve smt formulas. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (eds.), Advances in Neural Information Processing Systems 31, pp. 10317– 10328. Curran Associates, Inc., 2018. URL http://papers.nip… ↗
  4. Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving. In arXiv preprint arXiv:1904.03241, 2019.
  5. S. Bhatia, P. Kohli, and R. Singh. Neuro-symbolic program corrector for introductory programming assignments. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), pp. 60–70, May 2018. doi: 10.1145/3180155.3180219. — [doi:10.1145/3180155.3180219](https://doi.org/10.1145/3180155.3180219) find
  6. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101–148, 2016.
  7. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  8. Paul Cairns. Informalising formal mathematics: Searching the mizar library with latent semantics. In International Conference on Mathematical Knowledge Management, pp. 58–72. Springer, 2004. find
  9. Tommaso Dreossi, Alexandre Donzé, and Sanjit A Seshia. Compositional falsification of cyber-physical systems with machine learning components. Journal of Automated Reasoning, 63(4): 1031–1053, 2019. find
  10. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0—a framework for ltl and ω-automata manipulation. In International Symposium on Automated Technology for Verification and Analysis, pp. 122–129. Springer, 2016. find
  11. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark A. Ardis and Joanne M. Atlee (eds.), Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4-5, 1998, Clearwater Beach, Florida, USA, pp. 7–15. find
  12. ACM, 1998. doi: 10.1145/298595.298598. URL https://doi.org/10.1145/298595.298598. — [doi:10.1145/298595.298598](https://doi.org/10.1145/298595.298598) ↗
  13. Kousha Etessami and Gerard J. Holzmann. Optimizing büchi automata. In Catuscia Palamidessi (ed.), CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science, pp. 153–167. find
  14. Springer, 2000. doi: 10.1007/3-540-44618-4\\ 13. URL https://doi.org/10.1007/3-540-44618-4_13. — [doi:10.1007/3-540-44618-4\](https://doi.org/10.1007/3-540-44618-4\) ↗
  15. Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv:1802.08535, 2018.
  16. Patrick Fernandes, Miltiadis Allamanis, and Marc Brockschmidt. Structured neural summarization. arXiv preprint arXiv:1811.01824, 2018. find
  17. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to reason with hol4 tactics. arXiv preprint arXiv:1804.00595, 2018. find
  18. Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3–18. find
  19. Justin Gilmer, Samuel S Schoenholz, Patrick F Riley, Oriol Vinyals, and George E Dahl. Neural message passing for quantum chemistry. In Proceedings of the 34th International Conference on Machine Learning-Volume 70, pp. 1263–1272. JMLR. org, 2017.
  20. Rahul Gupta, Soham Pal, Aditya Kanade, and Shirish Shevade. Deepfix: Fixing common C language errors by deep learning. In Thirty-First AAAI Conference on Artificial Intelligence, 2017. find
  21. Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Delving deep into rectifiers: Surpassing human-level performance on imagenet classification. In 2015 IEEE International Conference on Computer Vision, ICCV 2015, Santiago, Chile, December 7-13, 2015, pp. 1026–1034, 2015. doi: 10.1109/ICCV.2015.1… find
  22. Vincent J. Hellendoorn, Charles Sutton, Rishabh Singh, and Petros Maniatis. Global relational models of source code. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum?id=B1lnbRNtwr. ↗
  23. Jan Holeček, Tomáš Kratochvı́la, Vojtěch Řehák, David Šafránek, Pavel Šimeček, et al. Verification results in liberouter project, 2004. find
  24. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608, 2018.
  25. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification, pp. 3–29. Springer, 2017. find
  26. IEEE-Commission et al. Ieee standard for property specification language (psl). IEEE Std 1850-2005, 2005. find
  27. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning, 53(2):173–213, 2014.
  28. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In Proceedings of International Conference on Learning Representations (ICLR), 2017.
  29. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In ICLR, 2020.
  30. Gil Lederman, Markus N. Rabe, Edward A. Lee, and Sanjit A. Seshia. Learning heuristics for quantified boolean formulas through deep reinforcement learning. 2020. URL http://arxiv.org/abs/1807.08058. ↗
  31. Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathematical reasoning in latent space. 2020.
  32. Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. LTL satisfiability checking revisited. In César Sánchez, Kristen Brent Venable, and Esteban Zimányi (eds.), 2013 20th International Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013, pp… find
  33. IEEE Computer Society, 2013. doi: 10.1109/TIME.2013.19. URL https://doi.org/10.1109/TIME.2013.19. — [doi:10.1109/time.2013.19](https://doi.org/10.1109/time.2013.19) ↗
  34. Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, and Jifeng He. Aalta: an ltl satisfiability checker over infinite/finite traces. In Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pp. 731–734, 2014. find
  35. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. arXiv preprint arXiv:2006.09265, 2020.
  36. Yaguang Li, Rose Yu, Cyrus Shahabi, and Yan Liu. Diffusion convolutional recurrent neural network: Data-driven traffic forecasting. arXiv preprint arXiv:1707.01926, 2017. — [arXiv:1707.01926](https://arxiv.org/abs/1707.01926) find
  37. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In LPAR, 2017.
  38. Jia Meng and Lawrence C Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1):41–57, 2009. find
  39. Matej Moravcı́k, Martin Schmid, Neil Burch, Viliam Lisý, Dustin Morrill, Nolan Bard, Trevor Davis, Kevin Waugh, Michael Johanson, and Michael H. Bowling. Deepstack: Expert-level artificial intelligence in no-limit poker. CoRR, abs/1701.01724, 2017. URL http://arxiv.org/abs/1701.01724. — [arXiv:1701.01724](https://arxiv.org/abs/1701.01724) ↗
  40. Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In AAAI, 2020.
  41. Radek Pelánek. BEEM: benchmarks for explicit model checkers. In Dragan Bosnacki and Stefan Edelkamp (eds.), Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings, volume 4595 of Lecture Notes in Computer Science, pp. 263–267. find
  42. Springer, 2007. doi: 10.1007/978-3-540-73370-6\\ 17. URL https://doi.org/10.1007/978-3-540-73370-6_17. — [doi:10.1007/978-3-540-73370-6\](https://doi.org/10.1007/978-3-540-73370-6\) ↗
  43. Chris Piech, Jonathan Huang, Andy Nguyen, Mike Phulsuksombati, Mehran Sahami, and Leonidas Guibas. Learning program embeddings to propagate feedback on student code. In International Conference on Machine Learning, pp. 1093–1102, 2015. find
  44. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46–57, 1977. doi: 10.1109/SFCS.1977.32. URL https://doi.org/10.1109/SFCS.1977.32. ↗
  45. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
  46. Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. 2020.
  47. Kristin Y Rozier and Moshe Y Vardi. Ltl satisfiability checking. In International SPIN Workshop on Model Checking of Software, pp. 149–167. Springer, 2007. find
  48. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. CoRR, abs/1904.01557, 2019. URL http://arxiv.org/abs/1904.01557. ↗
  49. Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions on Neural Networks, 20(1):61–80, 2008. find
  50. Imanol Schlag, Paul Smolensky, Roland Fernandez, Nebojsa Jojic, Jürgen Schmidhuber, and Jianfeng Gao. Enhancing the transformer with explicit relational encoding for math problem solving. arXiv preprint arXiv:1910.06611, 2019. — [arXiv:1910.06611](https://arxiv.org/abs/1910.06611) find
  51. Stephan Schulz. System description: E 1.8. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 735–743. Springer, 2013. find
  52. Viktor Schuppan and Luthfi Darmawan. Evaluating ltl satisfiability solvers. In International Symposium on Automated Technology for Verification and Analysis, pp. 397–413. Springer, 2011. find
  53. Stefan Schwendimann. A new one-pass tableau calculus for pltl. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 277–291. Springer, 1998. find
  54. Daniel Selsam and Nikolaj Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, pp. 336– 353, 2019. doi: 10.1007/978-3-030-2…
  55. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019. URL https://openreview.net/forum?id=HJ… ↗
  56. Sanjit A. Seshia and Dorsa Sadigh. Towards verified artificial intelligence. CoRR, abs/1606.08514, 2016. URL http://arxiv.org/abs/1606.08514. — [arXiv:1606.08514](https://arxiv.org/abs/1606.08514) ↗
  57. Sanjit A Seshia, Ankush Desai, Tommaso Dreossi, Daniel J Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. Formal specification for deep neural networks. In International Symposium on Automated Technology for Verification and Analysis, pp. 20–34. Spr… find
  58. Vighnesh Leonardo Shiv and Chris Quirk. Novel positional encodings to enable tree-based transformers. In NeurIPS 2019, 2019. URL https://www.microsoft.com/en-us/research/publication/novel-positional-encodings-to-enable-tree-based-transformers/. ↗
  59. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. Nature, 550(7676):354–359, 2017. find
  60. Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1–30, 2019. find
  61. Yaniv Taigman, Ming Yang, Marc’Aurelio Ranzato, and Lior Wolf. Deepface: Closing the gap to human-level performance in face verification. In 2014 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2014, Columbus, OH, USA, June 23-28, 2014, pp. 1701–1708, 2014. doi: 10.1109/CVPR.2014.22… — [doi:10.1109/cvpr.2014.220](https://doi.org/10.1109/cvpr.2014.220) find
  62. Josef Urban. MPTP–motivation, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. find
  63. Josef Urban. Malarea: a metasystem for automated reasoning in large theories. ESARLT, 257, 2007.
  64. Josef Urban and Jan Jakubův. First neural conjecturing datasets and experiments. In Conference on Intelligent Computer Mathematics, 2020.
  65. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. Malarea sg1-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, pp. 441–456. Springer, 2008. find
  66. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4-9 December 2017, Long B…
  67. Marcell Vazquez-Chanlatte. mvcisback/py-aiger, August 2018. URL https://doi.org/10.5281/zenodo.1326224. — [doi:10.5281/zenodo.1326224](https://doi.org/10.5281/zenodo.1326224) ↗
  68. Ke Wang, Rishabh Singh, and Zhendong Su. Dynamic neural program embedding for program repair. In ICLR, 2018. find
  69. Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, N… find
  70. Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. arXiv preprint arXiv:2007.02924, 2020.
  71. Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S Yu. A comprehensive survey on graph neural networks. arXiv preprint arXiv:1901.00596, 2019.
  72. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. arXiv preprint arXiv:1905.09381, 2019.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/hahn-2020-teaching-temporal-logics-neural-networks/