Elamur Research⌕
☰
home / papers / 2022 / Passport: Improving Automated Formal Verification Using Identifiers

Passport: Improving Automated Formal Verification Using Identifiers

Paper · 2022 · Alex Sanchez-Stern, Emily First, Timothy Zhou et al.

Summary

Machine-learning proof-synthesis tools for the Coq proof assistant learn from existing proof corpora to suggest proof scripts. Most prior work has focused on model architecture and has made little use of identifiers, the names of theorems, datatypes, functions, constructors and local variables, even though such names carry much meaning in Coq, which has no primitive datatypes. The authors present Passport, which extends the tactic-prediction model inherited from ASTactic and TacTok with three identifier encodings. Category vocabulary indexing tags each identifier with its kind and assigns indices to frequent names. Subword sequence modeling splits names into word-pieces to connect related identifiers. Path elaboration adds the fully qualified directory, file and module location of global definitions and constructors. On the CoqGym benchmark, each encoding improves the number of theorems proved automatically, and so does encoding each identifier category on its own. The work suggests that richer data representation, not only new architectures, can substantially advance automated formal verification.

Key points

  • Evaluation uses CoqGym, a benchmark of 124 open-source Coq projects, with a test set of 10,782 theorems. Baselines are ASTactic, Tac and Tok.
  • Head-to-head, a Passport-enhanced tool proves 29% more theorems than the strongest base tool. The three enhanced tools combined prove 38% more than the three base tools combined.
  • Pooling base and Passport tools proves 1,820 theorems (about 17.2%), compared with 1,259 for the base tools alone. This is a 45% gain.
  • Path elaboration alone yields 12.6% more proven theorems. Global definitions, local variables and type constructors each help when encoded separately.
  • Passport is open source (github.com/LASER-UMASS/Passport). The study also measures how non-deterministic training variance affects results.

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 Illinois Urbana-ChampaignUrbana · United States228 works · 74,591 citations🎓University of Massachusetts AmherstAmherst Center · United States122 works · 69,574 citations

 Fields, topics and concepts

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

Cite

Cite as Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun and Talia Ringer. 2022. Passport: Improving Automated Formal Verification Using Identifiers. arXiv:2204.10370 (ACM Transactions on Programming Languages and Systems (TOPLAS), 45(2):12:1-12:30, June 2023).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3593374 · arXiv 2204.10370

@misc{sanchezstern2022passport,
  title = {{Passport: Improving Automated Formal Verification Using Identifiers}},
  author = {Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun and Talia Ringer},
  year = {2022},
  doi = {10.1145/3593374},
  eprint = {2204.10370},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3593374}
}

References

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

  1. Agda Development Team. 2007-2021. The Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php ↗
  2. Andrew W. Appel. 2011. Verified Software Toolchain. In Programming Languages and Systems, Gilles Barthe (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–17. find
  3. Emilio Jesús Gallego Arias. 2016. SerAPI: Machine-Friendly, Data-Centric Serialization for COQ. find
  4. Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021. Program Synthesis with Large Language Models. CoRR abs/2108.07732 (2021). arXiv:2108.07732 https://arxiv.org/abs/2108.07732 ↗
  5. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR abs/1904.03241 (2019). arXiv:1904.03241 http://arxiv.org/abs/1904.03241 ↗
  6. Alejandro Barredo Arrieta, Natalia Díaz-Rodríguez, Javier Del Ser, Adrien Bennetot, Siham Tabik, Alberto Barbado, Salvador Garcia, Sergio Gil-Lopez, Daniel Molina, Richard Benjamins, Raja Chatila, and Francisco Herrera. 2020. Explainable Artificial Intelligence (XAI): Concepts, taxonomies, opportuni… find
  7. Pavol Bielik, Veselin Raychev, and Martin Vechev. 2016. PHOG: Probabilistic Model for Code. In Proceedings of The 33rd International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 48), Maria Florina Balcan and Kilian Q. Weinberger (Eds.). PMLR, New York, New York, USA… find
  8. Lukas Biewald. 2020. Experiment Tracking with Weights and Biases. https://www.wandb.com/ Software available from wandb.com. ↗
  9. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. 2020. Tactic Learning and Proving for the Coq Proof Assistant. In LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (EPiC Series in Computing, Vol. 73), Elvira Albert and Laura Kovacs (Ed… — [doi:10.29007/wg1q](https://doi.org/10.29007/wg1q) find
  10. Ahmet Celik, Karl Palmskog, and Milos Gligoric. 2017. ICoq: Regression proof selection for large-scale verification projects. In IEEE/ACM International Conference on Automated Software Engineering (ASE). Urbana-Champaign, IL, USA, 171–182. https://doi.org/10.1109/ASE.2017.8115630 — [doi:10.1109/ase.2017.8115630](https://doi.org/10.1109/ase.2017.8115630) ↗
  11. Ahmet Celik, Karl Palmskog, and Milos Gligoric. 2018. A Regression Proof Selection Tool for Coq. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Gothenburg, Sweden, 117–120. https://doi.org/10.1145/3183440.3183493 — [doi:10.1145/3183440.3183493](https://doi.org/10.1145/3183440.3183493) ↗
  12. Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric. 2019. Mutation Analysis for Coq. In IEEE/ACM International Conference on Automated Software Engineering (ASE). San Diego, California, 539–551. https://doi.org/10.1109/ASE.2019.00057 — [doi:10.1109/ase.2019.00057](https://doi.org/10.1109/ase.2019.00057) ↗
  13. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhai… — Evaluating Large Language Models Trained on Code
  14. Qibin Chen, Jeremy Lacomis, Edward J. Schwartz, Graham Neubig, Bogdan Vasilescu, and Claire Le Goues. 2022. VarCLR: Variable Semantic Representation Pre-Training via Contrastive Learning. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22… find
  15. Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. find
  16. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emi… — PaLM: Scaling Language Modeling with Pathways
  17. Coq Development Team. 1989-2021. The Coq Proof Assistant. http://coq.inria.fr ↗
  18. Thierry Coquand and Gérard Huet. 1986. The calculus of constructions. Technical Report RR-0530. INRIA. https://hal.inria.fr/inria-00076024 ↗
  19. Thierry Coquand and Christine Paulin. 1990. Inductively defined types. In COLOG-88, Per Martin-Löf and Grigori Mints (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 50–66. find
  20. Łukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning 61, 1 (01 Jun 2018), 423–453. https://doi.org/10.1007/s10817-018-9458-4 ↗
  21. Hoa Khanh Dam, Truyen Tran, and Trang Pham. 2016. A deep language model for software code. CoRR abs/1608.02715 (2016). arXiv:1608.02715 http://arxiv.org/abs/1608.02715 — [arXiv:1608.02715](https://arxiv.org/abs/1608.02715) ↗
  22. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic — With Proofs, Without Compromises. In IEEE Symposium on Security and Privacy (S&P). 1202–1219. https://doi.org/10.1109/SP.2019.00005 — [doi:10.1109/sp.2019.00005](https://doi.org/10.1109/sp.2019.00005) ↗
  23. Emily First and Yuriy Brun. 2022. Diversity-Driven Automated Formal Verification. In Proceedings of the 44th International Conference on Software Engineering (ICSE) (22–27). Pittsburgh, PA, USA. https://doi.org/10.1145/3510003.3510138 — [doi:10.1145/3510003.3510138](https://doi.org/10.1145/3510003.3510138) ↗
  24. Emily First, Yuriy Brun, and Arjun Guha. 2020. TacTok: Semantics-Aware Proof Synthesis. Proceedings of the ACM on Programming Languages (PACMPL) Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) issue 4 (November 2020), 231:1–231:31. https://doi.org/10.1145/3428299 DOI: 10.1… — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) ↗
  25. Jonathan Frankle, Peter-Michael Osera, David Walker, and S Zdancewic. 2016. Example-directed synthesis: a type-theoretic interpretation. ACM SIGPLAN Notices 51 (01 2016), 802–815. https://doi.org/10.1145/2914770.2837629 — [doi:10.1145/2914770.2837629](https://doi.org/10.1145/2914770.2837629) ↗
  26. Philip Gage. 1994. A New Algorithm for Data Compression. C Users J. 12, 2 (feb 1994), 23–38. find
  27. Xiang Gao. 2022. cub device scan is not deterministic as described in the documentation \#454. https://github.com/NVIDIA/cub/issues/454. ↗
  28. Leilani H. Gilpin, David Bau, Ben Z. Yuan, Ayesha Bajwa, Michael A. Specter, and Lalana Kagal. 2018. Explaining Explanations: An Approach to Evaluating Interpretability of Machine Learning. CoRR abs/1806.00069 (2018). arXiv:1806.00069 http://arxiv.org/abs/1806.00069 — [arXiv:1806.00069](https://arxiv.org/abs/1806.00069) ↗
  29. Riccardo Guidotti, Anna Monreale, Salvatore Ruggieri, Franco Turini, Fosca Giannotti, and Dino Pedreschi. 2018. A Survey of Methods for Explaining Black Box Models. ACM Comput. Surv. 51, 5, Article 93 (aug 2018), 42 pages. https://doi.org/10.1145/3236009 — [doi:10.1145/3236009](https://doi.org/10.1145/3236009) ↗
  30. Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete Completion using Types and Weights. find
  31. PLDI 2013 (2013), 12. 27–38. http://infoscience.epfl.ch/record/188990 ↗
  32. Lennart Heim. 2022. Estimating PaLM’s training cost. https://blog.heim.xyz/author/lennart/. ↗
  33. Vincent J. Hellendoorn, Premkumar T. Devanbu, and Mohammad Amin Alipour. 2018. On the naturalness of proofs. In ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) New Ideas and Emerging Results track. Orlando, FL, USA, 72… find
  34. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In International Conference on Learning Representations. https://openreview.net/forum?id=r1xwKoR9Y7 ↗
  35. Isabelle Development Team. 1994-2021. Isabelle. http://isabelle.in.tum.de ↗
  36. Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric. 2020. MCoq: Mutation Analysis for Coq Verification Projects. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Seoul, South Korea, 89–92. https://doi.org/10.1145/3377812.3382156 — [doi:10.1145/3377812.3382156](https://doi.org/10.1145/3377812.3382156) ↗
  37. Rafael Michael Karampatsis, Hlib Babii, Romain Robbes, Charles Sutton, and Andrea Janes. 2020. Big Code != Big Vocabulary: Open-Vocabulary Models for Source code. In Proceedings of the 42nd International Conference on Software Engineering (Seoul, South Korea) (ICSE ’20). ACM. https://doi.org/10.1145… find
  38. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22Nd Symposi… find
  39. Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov. 2012. Machine Learning in Proof General: Interfacing Interfaces. In Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012 (EPTCS, Vol. 118), Cezary Kaliszyk and Christoph… — [doi:10.4204/eptcs.118.2](https://doi.org/10.4204/eptcs.118.2) find
  40. Lean Development Team. 2014-2021. Theorem Proving in Lean. http://leanprover.github.io/tutorial/ ↗
  41. Thabang Lebese, Ndivhuwo Makondo, Cristina Cornelio, and Naweed Khan. 2021. Proof Extraction for Logical Neural Networks. In Advances in Programming Languages and Neurosymbolic Systems Workshop. https://openreview.net/forum?id=Xw3kb6UyA31 ↗
  42. Dmitry Lepikhin, HyoukJoong Lee, Yuanzhong Xu, Dehao Chen, Orhan Firat, Yanping Huang, Maxim Krikun, Noam Shazeer, and Zhifeng Chen. 2020. GShard: Scaling Giant Models with Conditional Computation and Automatic Sharding. In International Conference on Learning Representations. find
  43. Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814 ↗
  44. Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, James M… — Competition-Level Code Generation with AlphaCode
  45. Yangguang Li, Feng Liang, Lichen Zhao, Yufeng Cui, Wanli Ouyang, Jing Shao, Fengwei Yu, and Junjie Yan. 2022b. Supervision Exists Everywhere: A Data Efficient Contrastive Language-Image Pre-training Paradigm. In International Conference on Learning Representations. https://openreview.net/forum?id=zq… ↗
  46. Liyuan Liu, Xiaodong Liu, Jianfeng Gao, Weizhu Chen, and Jiawei Han. 2020. Understanding the Difficulty of Training Transformers. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP). Association for Computational Linguistics, Online, 5747–5763. https://d…
  47. Lili Mou, Ge Li, Zhi Jin, Lu Zhang, and Tao Wang. 2014. TBCNN: A Tree-Based Convolutional Neural Network for Programming Language Processing. CoRR abs/1409.5718 (2014). arXiv:1409.5718 http://arxiv.org/abs/1409.5718 ↗
  48. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2020a. Deep Generation of Coq Lemma Names Using Elaborated Terms. In International Joint Conference on Automated Reasoning (IJCAR). Paris, France, 97–118. find
  49. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2020b. Learning to Format Coq Code Using Language Models. In The Coq Workshop. Aubervilliers, France. find
  50. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2021. Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Madrid, Spain, 21–24. https://doi.org/10.1109/ICSE-Companio… — [doi:10.1109/icse-companion52605.2021.00026](https://doi.org/10.1109/icse-companion52605.2021.00026) ↗
  51. Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis. SIGPLAN Not. 50, 6 (June 2015), 619–630. https://doi.org/10.1145/2813885.2738007 ↗
  52. Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. 2020. Graph representations for higher-order logic and theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 34. 2967–2974.
  53. Karl Palmskog, Ahmet Celik, and Milos Gligoric. 2018. PiCoq: Parallel Regression Proving for Large-Scale Verification Projects. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). Amsterdam, Netherlands, 344–355. https://doi.org/10.1145/3213846.3213877 — [doi:10.1145/3213846.3213877](https://doi.org/10.1145/3213846.3213877) ↗
  54. Matthew E. Peters, Mark Neumann, Mohit Iyyer, Matt Gardner, Christopher Clark, Kenton Lee, and Luke Zettlemoyer. 2018. Deep Contextualized Word Representations. In Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (NAACL-HLT), Vol.…
  55. Hung Viet Pham, Shangshu Qian, Jiannan Wang, Thibaud Lutellier, Jonathan Rosenthal, Lin Tan, Yaoliang Yu, and Nachiappan Nagappan. 2020a. Problems and Opportunities in Training Deep Learning Software Systems: An Analysis of Variance. In Proceedings of the 35th IEEE/ACM International Conference on Au… — [doi:10.1145/3324884.3416545](https://doi.org/10.1145/3324884.3416545) find
  56. Hung Viet Pham, Shangshu Qian, Jiannan Wang, Thibaud Lutellier, Jonathan Rosenthal, Lin Tan, Yaoliang Yu, and Nachiappan Nagappan. 2020b. Problems and Opportunities in Training Deep Learning Software Systems: An Analysis of Variance. In Proceedings of the 35th IEEE/ACM International Conference on Au… — [doi:10.1145/3324884.3416545](https://doi.org/10.1145/3324884.3416545) find
  57. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. 2021. Software Foundations. Vol. 1: Logical Foundations. https://softwarefoundations.cis.upenn.edu/lf-current/index.html Stanislas Polu, Jesse Michae… ↗
  58. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. CoRR abs/2009.03393 (2020). arXiv:2009.03393 https://arxiv.org/abs/2009.03393 ↗
  59. Martin Popel and Ondřej Bojar. 2018. Training Tips for the Transformer Model. The Prague Bulletin of Mathematical Linguistics 110, 1 (2018), 43–70.
  60. Shangshu Qian, Viet Hung Pham, Thibaud Lutellier, Zeou Hu, Jungwon Kim, Lin Tan, Yaoliang Yu, Jiahao Chen, and Sameena Shah. 2021. Are My Deep Learning Systems Fair? An Empirical Study of Fixed-Seed Training. In Advances in Neural Information Processing Systems, M. Ranzato, A. Beygelzimer, Y. Dauphi… find
  61. Samyam Rajbhandari, Jeff Rasley, Olatunji Ruwase, and Yuxiong He. 2020. ZeRO: Memory Optimizations toward Training Trillion Parameter Models. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (Atlanta, Georgia) (SC ’20). IEEE Press, Artic… find
  62. Tom P Reichel. 2022. Large cumulative sums appear to be nondeterministic. \#75240. https://github.com/pytorch/pytorch/issues/75240. ↗
  63. Talia Ringer and Joe Cutler. 2021. Talia and Joe chat about proof engineering with copilot. https://youtu.be/jFL-ftywPiM ↗
  64. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends®in Programming Languages 5, 2-3 (2019), 102–281. https://doi.org/10.1561/2500000045 — [doi:10.1561/2500000045](https://doi.org/10.1561/2500000045) ↗
  65. Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. 2021. Proof repair across type equivalences. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM. https://doi.org/10.1145/3453483.3454033 — [doi:10.1145/3453483.3454033](https://doi.org/10.1145/3453483.3454033) ↗
  66. Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. 2020. REPLica: REPL Instrumentation for Coq Analysis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY… — [doi:10.1145/3372885.3373823](https://doi.org/10.1145/3372885.3373823) find
  67. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. 2020. Generating Correctness Proofs with Neural Networks. In Machine Learning in Programming Languages. ACM SIGPLAN.
  68. D. Sculley, Gary Holt, Daniel Golovin, Eugene Davydov, Todd Phillips, Dietmar Ebner, Vinay Chaudhary, and Michael Young. 2014. Machine Learning: The High Interest Credit Card of Technical Debt. In SE4ML: Software Engineering for Machine Learning (NIPS 2014 Workshop). find
  69. Rico Sennrich, Barry Haddow, and Alexandra Birch. 2016. Neural Machine Translation of Rare Words with Subword Units. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). Association for Computational Linguistics, Berlin, Germany, 1715–17…
  70. Gil Shamir and Dong Lin. 2022. Reproducibility in Deep Learning and Smooth Activations. https://ai.googleblog.com/2022/04/reproducibility-in-deep-learning-and.html?m=1. ↗
  71. Jean Souyris. 2014. Industrial Use of CompCert on a Safety-Critical Software Product. http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf. ↗
  72. Alexey Svyatkovskiy, Sebastian Lee, Anna Hadjitofi, Maik Riechert, Juliana Franco, and Miltiadis Allamanis. 2020. Fast and Memory-Efficient Neural Code Completion. CoRR abs/2004.13651 (2020). arXiv:2004.13651 https://arxiv.org/abs/2004.13651 — [arXiv:2004.13651](https://arxiv.org/abs/2004.13651) ↗
  73. Kai Sheng Tai, Richard Socher, and Christopher D. Manning. 2015. Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks. In Annual Meeting of the Association for Computational Linguistics (ACL), Vol. 1. Beijing, China, 1556–1566. https://doi.org/10.3115/v1/P15-1150 ↗
  74. Zhaopeng Tu, Zhendong Su, and Premkumar Devanbu. 2014. On the Localness of Software. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (Hong Kong, China) (FSE 2014). Association for Computing Machinery, New York, NY, USA, 269–280. https://doi.org/1… find
  75. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Por… — [doi:10.1145/2737924.2737958](https://doi.org/10.1145/2737924.2737958) find
  76. Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. 2022. Memorizing Transformers. In International Conference on Learning Representations. https://openreview.net/forum?id=TrjbxzRcnf- ↗
  77. Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML). Long Beach, CA, USA. http://proceedings.mlr.press/v97/yang19a/yang19a.pdf ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/stern-2022-passport-improving-automated-formal-verification/