{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:15:18Z","timestamp":1773479718948,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373827","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"85-98","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Exploration of neural machine translation in autoformalization of mathematics in Mizar"],"prefix":"10.1145","author":[{"given":"Qingxiang","family":"Wang","sequence":"first","affiliation":[{"name":"University of Innsbruck, Austria"}]},{"given":"Chad","family":"Brown","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Czechia"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Austria \/ University of Warsaw, Poland"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Czechia"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 12th International Conference on Automated Deduction (CADE-12)","author":"Anonymous","year":"1994","unstructured":"Anonymous . 1994 . The QED Manifesto . In Proceedings of the 12th International Conference on Automated Deduction (CADE-12) . SpringerVerlag, London, UK, UK, 238\u2013251. http:\/\/dl.acm.org\/citation.cfm?id= 648231.752823 Anonymous. 1994. The QED Manifesto. In Proceedings of the 12th International Conference on Automated Deduction (CADE-12). SpringerVerlag, London, UK, UK, 238\u2013251. http:\/\/dl.acm.org\/citation.cfm?id= 648231.752823"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D18-1399"},{"key":"e_1_3_2_1_3_1","volume-title":"3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, Yoshua Bengio and Yann LeCun (Eds.). http:\/\/arxiv.org\/abs\/1409","author":"Bahdanau Dzmitry","year":"2015","unstructured":"Dzmitry Bahdanau , Kyunghyun Cho , and Yoshua Bengio . 2015 . Neural Machine Translation by Jointly Learning to Align and Translate . In 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, Yoshua Bengio and Yann LeCun (Eds.). http:\/\/arxiv.org\/abs\/1409 .0473 Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. 2015. Neural Machine Translation by Jointly Learning to Align and Translate. In 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, Yoshua Bengio and Yann LeCun (Eds.). http:\/\/arxiv.org\/abs\/1409.0473"},{"key":"e_1_3_2_1_4_1","first-page":"19","article-title":"Automatic Translation in Formalized Mathematics","volume":"5","author":"Bancerek Grzegorz","year":"2006","unstructured":"Grzegorz Bancerek . 2006 . Automatic Translation in Formalized Mathematics . Mechanized Mathematics and Its Applications 5 , 2 (2006), 19 \u2013 31 . Grzegorz Bancerek. 2006. Automatic Translation in Formalized Mathematics. Mechanized Mathematics and Its Applications 5, 2 (2006), 19\u201331.","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9440-6"},{"key":"e_1_3_2_1_6_1","volume-title":"Mizar and the Machine Translation of Mathematics Documents. Available online at http:\/\/ www.mizar.org\/ project\/ banc_carl93.ps","author":"Bancerek Grzegorz","year":"1994","unstructured":"Grzegorz Bancerek and Patricia Carlson . 1994. Mizar and the Machine Translation of Mathematics Documents. Available online at http:\/\/ www.mizar.org\/ project\/ banc_carl93.ps ( 1994 ). Grzegorz Bancerek and Patricia Carlson. 1994. Mizar and the Machine Translation of Mathematics Documents. Available online at http:\/\/ www.mizar.org\/ project\/ banc_carl93.ps (1994)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96812-4_1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"e_1_3_2_1_9_1","volume-title":"Enriching Word Vectors with Subword Information. arXiv preprint arXiv:1607.04606","author":"Bojanowski Piotr","year":"2016","unstructured":"Piotr Bojanowski , Edouard Grave , Armand Joulin , and Tomas Mikolov . 2016. Enriching Word Vectors with Subword Information. arXiv preprint arXiv:1607.04606 ( 2016 ). Piotr Bojanowski, Edouard Grave, Armand Joulin, and Tomas Mikolov. 2016. Enriching Word Vectors with Subword Information. arXiv preprint arXiv:1607.04606 (2016)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42547-4_8"},{"key":"e_1_3_2_1_12_1","volume-title":"Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling. CoRR abs\/1412.3555","author":"Chung Junyoung","year":"2014","unstructured":"Junyoung Chung , \u00c7aglar G\u00fcl\u00e7ehre , KyungHyun Cho , and Yoshua Bengio . 2014. Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling. CoRR abs\/1412.3555 ( 2014 ). Junyoung Chung, \u00c7aglar G\u00fcl\u00e7ehre, KyungHyun Cho, and Yoshua Bengio. 2014. Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling. CoRR abs\/1412.3555 (2014)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_2_1_14_1","volume-title":"The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts","author":"Cramer Marcos","unstructured":"Marcos Cramer , Bernhard Fisseni , Peter Koepke , Daniel K\u00fchlwein , Bernhard Schr\u00f6der , and Jip Veldman . 2010. The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts . In Controlled Natural Language, Norbert E. Fuchs (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 170\u2013186. Marcos Cramer, Bernhard Fisseni, Peter Koepke, Daniel K\u00fchlwein, Bernhard Schr\u00f6der, and Jip Veldman. 2010. The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts. In Controlled Natural Language, Norbert E. Fuchs (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 170\u2013186."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02551274"},{"key":"e_1_3_2_1_16_1","volume-title":"BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding. CoRR abs\/1810.04805","author":"Devlin Jacob","year":"2018","unstructured":"Jacob Devlin , Ming-Wei Chang , Kenton Lee , and Kristina Toutanova . 2018 . BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding. CoRR abs\/1810.04805 (2018). arXiv: 1810.04805 http:\/\/arxiv.org\/abs\/1810.04805 Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2018. BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding. CoRR abs\/1810.04805 (2018). arXiv: 1810.04805 http:\/\/arxiv.org\/abs\/1810.04805"},{"key":"e_1_3_2_1_17_1","volume-title":"Gradient Descent Finds Global Minima of Deep Neural Networks. CoRR abs\/1811.03804","author":"Du Simon S.","year":"2018","unstructured":"Simon S. Du , Jason D. Lee , Haochuan Li , Liwei Wang , and Xiyu Zhai . 2018. Gradient Descent Finds Global Minima of Deep Neural Networks. CoRR abs\/1811.03804 ( 2018 ). Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai. 2018. Gradient Descent Finds Global Minima of Deep Neural Networks. CoRR abs\/1811.03804 (2018)."},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. of ICML.","author":"Gehring Jonas","year":"2017","unstructured":"Jonas Gehring , Michael Auli , David Grangier , Denis Yarats , and Yann N Dauphin . 2017 . Convolutional Sequence to Sequence Learning . In Proc. of ICML. Jonas Gehring, Michael Auli, David Grangier, Denis Yarats, and Yann N Dauphin. 2017. Convolutional Sequence to Sequence Learning. In Proc. of ICML."},{"key":"e_1_3_2_1_19_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham (Eds.). 1993 . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press , New York, NY, USA . M. J. C. Gordon and T. F. Melham (Eds.). 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1162\/neco.1997.9.8.1735"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-6080(91)90009-T"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-6080(89)90020-8"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_15"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_2"},{"key":"e_1_3_2_1_26_1","volume-title":"Advances in Neural Information Processing Systems 25","author":"Krizhevsky Alex","unstructured":"Alex Krizhevsky , Ilya Sutskever , and Geoffrey E Hinton . 2012. ImageNet Classification with Deep Convolutional Neural Networks . In Advances in Neural Information Processing Systems 25 , F. Pereira, C. J. C. Burges, L. Bottou, and K. Q. Weinberger (Eds.). Curran Associates, Inc. , 1097\u20131105. http:\/\/papers.nips.cc\/paper\/4824-imagenet-classificationwith-deep-convolutional-neural-networks.pdf Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. 2012. ImageNet Classification with Deep Convolutional Neural Networks. In Advances in Neural Information Processing Systems 25, F. Pereira, C. J. C. Burges, L. Bottou, and K. Q. Weinberger (Eds.). Curran Associates, Inc., 1097\u20131105. http:\/\/papers.nips.cc\/paper\/4824-imagenet-classificationwith-deep-convolutional-neural-networks.pdf"},{"key":"e_1_3_2_1_27_1","volume-title":"Cross-lingual Language Model Pretraining. arXiv preprint arXiv:1901.07291","author":"Lample Guillaume","year":"2019","unstructured":"Guillaume Lample and Alexis Conneau . 2019. Cross-lingual Language Model Pretraining. arXiv preprint arXiv:1901.07291 ( 2019 ). Guillaume Lample and Alexis Conneau. 2019. Cross-lingual Language Model Pretraining. arXiv preprint arXiv:1901.07291 (2019)."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D18-1549"},{"key":"e_1_3_2_1_29_1","volume-title":"Neural Machine Translation (seq2seq) Tutorial. https:\/\/github.com\/tensorflow\/nmt","author":"Luong Minh-Thang","year":"2017","unstructured":"Minh-Thang Luong , Eugene Brevdo , and Rui Zhao . 2017. Neural Machine Translation (seq2seq) Tutorial. https:\/\/github.com\/tensorflow\/nmt ( 2017 ). Minh-Thang Luong, Eugene Brevdo, and Rui Zhao. 2017. Neural Machine Translation (seq2seq) Tutorial. https:\/\/github.com\/tensorflow\/nmt (2017)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D15-1166"},{"key":"e_1_3_2_1_31_1","volume-title":"Advances in Neural Information Processing Systems 26","author":"Mikolov Tomas","unstructured":"Tomas Mikolov , Ilya Sutskever , Kai Chen , Greg S Corrado , and Jeff Dean . 2013. Distributed Representations of Words and Phrases and their Compositionality . In Advances in Neural Information Processing Systems 26 , C. J. C. Burges, L. Bottou, M. Welling, Z. Ghahramani, and K. Q. Weinberger (Eds.). Curran Associates, Inc. , 3111\u20133119. Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S Corrado, and Jeff Dean. 2013. Distributed Representations of Words and Phrases and their Compositionality. In Advances in Neural Information Processing Systems 26, C. J. C. Burges, L. Bottou, M. Welling, Z. Ghahramani, and K. Q. Weinberger (Eds.). Curran Associates, Inc., 3111\u20133119."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.3115\/1073083.1073135"},{"key":"e_1_3_2_1_33_1","volume-title":"Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop.","author":"Paszke Adam","year":"2017","unstructured":"Adam Paszke , Sam Gross , Soumith Chintala , Gregory Chanan , Edward Yang , Zachary DeVito , Zeming Lin , Alban Desmaison , Luca Antiga , and Adam Lerer . 2017 . Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop. Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. 2017. Automatic Differentiation in PyTorch. In NIPS Autodiff Workshop."},{"key":"e_1_3_2_1_34_1","volume-title":"Guiding Theorem Proving by Recurrent Neural Networks. CoRR abs\/1905.07961","author":"Piotrowski Bartosz","year":"2019","unstructured":"Bartosz Piotrowski and Josef Urban . 2019. Guiding Theorem Proving by Recurrent Neural Networks. CoRR abs\/1905.07961 ( 2019 ). arXiv: 1905.07961 http:\/\/arxiv.org\/abs\/1905.07961 Bartosz Piotrowski and Josef Urban. 2019. Guiding Theorem Proving by Recurrent Neural Networks. CoRR abs\/1905.07961 (2019). arXiv: 1905.07961 http:\/\/arxiv.org\/abs\/1905.07961"},{"key":"e_1_3_2_1_35_1","volume-title":"Depth Separation in ReLU Networks for Approximating Smooth Non-Linear Functions. ArXiv abs\/1610.09887","author":"Safran Itay","year":"2016","unstructured":"Itay Safran and Ohad Shamir . 2016. Depth Separation in ReLU Networks for Approximating Smooth Non-Linear Functions. ArXiv abs\/1610.09887 ( 2016 ). Itay Safran and Ohad Shamir. 2016. Depth Separation in ReLU Networks for Approximating Smooth Non-Linear Functions. ArXiv abs\/1610.09887 (2016)."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58156-1_18"},{"key":"e_1_3_2_1_37_1","volume-title":"Le","author":"Sutskever Ilya","year":"2014","unstructured":"Ilya Sutskever , Oriol Vinyals , and Quoc V . Le . 2014 . Sequence to Sequence Learning with Neural Networks. CoRR abs\/1409.3215 (2014). Ilya Sutskever, Oriol Vinyals, and Quoc V. Le. 2014. Sequence to Sequence Learning with Neural Networks. CoRR abs\/1409.3215 (2014)."},{"key":"e_1_3_2_1_38_1","volume-title":"Representation Benefits of Deep Feedforward Networks. CoRR abs\/1509.08101","author":"Telgarsky Matus","year":"2015","unstructured":"Matus Telgarsky . 2015. Representation Benefits of Deep Feedforward Networks. CoRR abs\/1509.08101 ( 2015 ). Matus Telgarsky. 2015. Representation Benefits of Deep Feedforward Networks. CoRR abs\/1509.08101 (2015)."},{"key":"e_1_3_2_1_39_1","volume-title":"Axiomatics 1","author":"Trybulec Andrzej","year":"1989","unstructured":"Andrzej Trybulec . 1989. Tarski Grothendieck Set Theory. Journal of Formalized Mathematics , Axiomatics 1 ( 1989 ). Andrzej Trybulec. 1989. Tarski Grothendieck Set Theory. Journal of Formalized Mathematics, Axiomatics 1 (1989)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6245-1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11618027_23"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213006002588"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9032-3"},{"key":"e_1_3_2_1_44_1","first-page":"I","article-title":"Attention is All you Need","volume":"30","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani , Noam Shazeer , Niki Parmar , Jakob Uszkoreit , Llion Jones , Aidan N Gomez , \u0141ukasz Kaiser , and Illia Polosukhin . 2017 . Attention is All you Need . In Advances in Neural Information Processing Systems 30 , I . Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (Eds.). Curran Associates, Inc., 5998\u2013 6008. http:\/\/papers.nips.cc\/paper\/7181-attention-is-all-you-need.pdf Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141ukasz Kaiser, and Illia Polosukhin. 2017. Attention is All you Need. In Advances in Neural Information Processing Systems 30, I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (Eds.). Curran Associates, Inc., 5998\u2013 6008. http:\/\/papers.nips.cc\/paper\/7181-attention-is-all-you-need.pdf","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/2267732"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96812-4_22"}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"New Orleans LA USA","acronym":"POPL '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373827","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373827","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373827"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":46,"alternative-id":["10.1145\/3372885.3373827","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373827","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}