{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T06:24:44Z","timestamp":1783405484628,"version":"3.54.6"},"reference-count":142,"publisher":"MIT Press","license":[{"start":{"date-parts":[[2023,9,20]],"date-time":"2023-09-20T00:00:00Z","timestamp":1695168000000},"content-version":"vor","delay-in-days":262,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["direct.mit.edu"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,9,19]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Automating discovery in mathematics and science will require sophisticated methods of information extraction and abstract reasoning, including models that can convincingly process relationships between mathematical elements and natural language, to produce problem solutions of real-world value. We analyze mathematical language processing methods across five strategic sub-areas (identifier-definition extraction, formula retrieval, natural language premise selection, math word problem solving, and informal theorem proving) from recent years, highlighting prevailing methodologies, existing limitations, overarching trends, and promising avenues for future research.<\/jats:p>","DOI":"10.1162\/tacl_a_00594","type":"journal-article","created":{"date-parts":[[2023,9,20]],"date-time":"2023-09-20T15:03:11Z","timestamp":1695222191000},"page":"1162-1184","update-policy":"https:\/\/doi.org\/10.1162\/mitpressjournals.corrections.policy","source":"Crossref","is-referenced-by-count":3,"title":["Introduction to Mathematical Language Processing: Informal Proofs, Word Problems, and Supporting Tasks"],"prefix":"10.1162","volume":"11","author":[{"given":"Jordan","family":"Meadows","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Manchester, UK. jordan.meadows@postgrad.manchester.ac.uk"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e9","family":"Freitas","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, UK"},{"name":"Idiap Research Institute, Switzerland. andre.freitas@idiap.ch"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"281","published-online":{"date-parts":[[2023,9,19]]},"reference":[{"key":"2023092014493531000_bib1","first-page":"88","article-title":"Ntcir-11 math-2 task overview","volume-title":"NTCIR","author":"Aizawa","year":"2014"},{"key":"2023092014493531000_bib2","first-page":"3466","article-title":"Multilingual aliasing for auto-generating proposition banks","volume-title":"Proceedings of COLING 2016, the 26th International Conference on Computational Linguistics: Technical Papers","author":"Akbik","year":"2016"},{"issue":"2","key":"2023092014493531000_bib3","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","article-title":"Premise selection for mathematics by corpus analysis and kernel methods","volume":"52","author":"Alama","year":"2014","journal-title":"Journal of Automated Reasoning"},{"key":"2023092014493531000_bib4","first-page":"2204","article-title":"Mathalign: Linking formula identifiers to their contextual natural language descriptions","volume-title":"Proceedings of The 12th Language Resources and Evaluation Conference","author":"Alexeeva","year":"2020"},{"issue":"18","key":"2023092014493531000_bib5","doi-asserted-by":"publisher","first-page":"4909","DOI":"10.1073\/pnas.1603205113","article-title":"Origins of the brain networks for advanced mathematics in expert mathematicians","volume":"113","author":"Amalric","year":"2016","journal-title":"Proceedings of the National Academy of Sciences"},{"key":"2023092014493531000_bib6","article-title":"Mathqa: Towards interpretable math word problem solving with operation-based formalisms","author":"Amini","year":"2019","journal-title":"arXiv preprint arXiv:1905.13319"},{"key":"2023092014493531000_bib7","unstructured":"Takuto\n              Asakura\n            , YusukeMiyao, AkikoAizawa, and MichaelKohlhase. 2021. Miogatto: A math identifier-oriented grounding annotation tool. Technical report, EasyChair."},{"key":"2023092014493531000_bib8","article-title":"Proofnet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems","author":"Azerbayev","year":"2022"},{"key":"2023092014493531000_bib9","article-title":"Holist: An environment for machine learning of higher-order theorem proving (extended version)","author":"Bansal","year":"2019","journal-title":"arXiv preprint arXiv:1904.03241"},{"key":"2023092014493531000_bib10","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D19-1371","article-title":"Scibert: A pretrained language model for scientific text","author":"Iz","year":"2019","journal-title":"arXiv preprint arXiv:1903.10676"},{"key":"2023092014493531000_bib11","article-title":"Natural language input for a computer problem solving system","author":"Bobrow","year":"1964"},{"key":"2023092014493531000_bib12","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1162\/tacl_a_00051","article-title":"Enriching word vectors with subword information","volume":"5","author":"Bojanowski","year":"2017","journal-title":"Transactions of the Association for Computational Linguistics"},{"key":"2023092014493531000_bib13","first-page":"1877","article-title":"Language models are few-shot learners","volume":"33","author":"Brown","year":"2020","journal-title":"Advances in Neural Information Processing Systems"},{"key":"2023092014493531000_bib14","article-title":"Mathematics and the brain","author":"Butterworth","year":"2002","journal-title":"Opening address to the Mathematical Association, Reading"},{"key":"2023092014493531000_bib15","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1609\/aaai.v35i1.16075","article-title":"A bottom-up dag structure extraction model for math word problems","volume-title":"Thirty-Fifth AAAI Conference on Artificial 2021","author":"Cao","year":"2021"},{"key":"2023092014493531000_bib16","first-page":"303","article-title":"Computer solution of calculus word problems","volume-title":"Proceedings of the 1st International Joint Conference on Artificial Intelligence","author":"Charniak","year":"1969"},{"key":"2023092014493531000_bib17","article-title":"Evaluating large language models trained on code","author":"Chen","year":"2021","journal-title":"arXiv preprint arXiv:2107.03374"},{"key":"2023092014493531000_bib18","article-title":"Palm: Scaling language modeling with pathways","author":"Chowdhery","year":"2022","journal-title":"arXiv preprint arXiv:2204.02311"},{"key":"2023092014493531000_bib19","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/537","article-title":"Transformers as soft reasoners over language","author":"Clark","year":"2020","journal-title":"arXiv preprint arXiv: 2002.05867"},{"key":"2023092014493531000_bib20","article-title":"Learning to match mathematical statements with proofs","author":"Coavoux","year":"2021","journal-title":"arXiv preprint arXiv:2102.02110"},{"key":"2023092014493531000_bib21","article-title":"Training verifiers to solve math word problems","author":"Cobbe","year":"2021","journal-title":"arXiv preprint arXiv:2110.14168"},{"key":"2023092014493531000_bib22","first-page":"124","article-title":"Keyword-based natural language premise selection for an automatic mathematical statement proving","volume-title":"Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing","author":"Dastgheib","year":"2022"},{"key":"2023092014493531000_bib23","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1145\/3077136.3080748","article-title":"Layout and semantics: Combining representations for mathematical formula search","volume-title":"Proceedings of the 40th International ACM SIGIR Conference on Research and Development in Information Retrieval","author":"Davila","year":"2017"},{"key":"2023092014493531000_bib24","article-title":"BERT: Pre-training of deep bidirectional transformers for language understanding","author":"Devlin","year":"2018","journal-title":"arXiv preprint arXiv: 1810.04805"},{"key":"2023092014493531000_bib25","doi-asserted-by":"publisher","first-page":"820","DOI":"10.1109\/NLPKE.2003.1276017","article-title":"Hownet-a hybrid language and knowledge resource","volume-title":"International Conference on Natural Language Processing and Knowledge Engineering, 2003. Proceedings. 2003","author":"Dong","year":"2003"},{"issue":"4","key":"2023092014493531000_bib26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1045\/april2002-weibel","article-title":"Metadata principles and practicalities","volume":"8","author":"Duval","year":"2002","journal-title":"D-lib Magazine"},{"key":"2023092014493531000_bib27","volume-title":"Computers and Thought","author":"Feigenbaum","year":"1963"},{"key":"2023092014493531000_bib28","doi-asserted-by":"publisher","first-page":"3395","DOI":"10.18653\/v1\/2021.emnlp-main.273","article-title":"Graphmr: Graph neural network for mathematical reasoning","volume-title":"Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing","author":"Feng","year":"2021"},{"key":"2023092014493531000_bib29","article-title":"Natural language premise selection: Finding supporting statements for mathematical text","author":"Ferreira","year":"2020","journal-title":"arXiv preprint arXiv:2004.14959"},{"key":"2023092014493531000_bib30","doi-asserted-by":"publisher","first-page":"7365","DOI":"10.18653\/v1\/2020.acl-main.657","article-title":"Premise selection in natural language mathematical texts","volume-title":"Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics","author":"Ferreira","year":"2020"},{"key":"2023092014493531000_bib31","doi-asserted-by":"publisher","first-page":"3234","DOI":"10.18653\/v1\/2021.eacl-main.282","article-title":"Star: Cross-modal [sta] tement [r] epresentation for selecting relevant mathematical premises","volume-title":"Proceedings of the 16th Conference of the European Chapter of the Association for Computational Linguistics: Main Volume","author":"Ferreira","year":"2021"},{"key":"2023092014493531000_bib32","doi-asserted-by":"publisher","first-page":"938","DOI":"10.18653\/v1\/2022.findings-acl.76","article-title":"To be or not to be an integer? Encoding variables for mathematical text","volume-title":"Findings of the Association for Computational Linguistics: ACL 2022","author":"Ferreira","year":"2022"},{"key":"2023092014493531000_bib33","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.semeval-1.233","article-title":"Machamp at semeval-2022 tasks 2, 3, 4, 6, 10, 11, and 12: Multi-task multi-lingual learning for a pre-selected set of semantic datasets","volume-title":"Proceedings of the 16th International Workshop on Semantic Evaluation (SemEval-2022). Association for Computational Linguistics","author":"van der Goot","year":"2022"},{"key":"2023092014493531000_bib34","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1145\/3477314.3507177","article-title":"Question answering over logic puzzles using theorem proving","volume-title":"Proceedings of the 37th ACM\/ SIGAPP Symposium on Applied Computing","author":"Groza","year":"2022"},{"issue":"4","key":"2023092014493531000_bib35","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11786-016-0274-0","article-title":"A survey on retrieval of mathematical knowledge","volume":"10","author":"Guidi","year":"2016","journal-title":"Mathematics in Computer Science"},{"key":"2023092014493531000_bib36","article-title":"Introduction to the flyspeck project","volume-title":"Dagstuhl Seminar Proceedings","author":"Hales","year":"2006"},{"key":"2023092014493531000_bib37","article-title":"Contrastive finetuning of generative language models for informal premise selection","author":"Han","year":"2021"},{"key":"2023092014493531000_bib38","article-title":"Measuring massive multitask language understanding","author":"Hendrycks","year":"2020","journal-title":"arXiv preprint arXiv:2009.03300"},{"key":"2023092014493531000_bib39","article-title":"Measuring mathematical problem solving with the math dataset","author":"Hendrycks","year":"2021","journal-title":"arXiv preprint arXiv:2103.03874"},{"key":"2023092014493531000_bib40","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-79409-7_19","article-title":"Word similarity in wordnet","volume-title":"Modeling, Simulation and Optimization of Complex Processes","author":"Hong-Minh","year":"2008"},{"key":"2023092014493531000_bib41","doi-asserted-by":"publisher","first-page":"893","DOI":"10.18653\/v1\/S19-2153","article-title":"Semeval-2019 task 10: Math question answering","volume-title":"Proceedings of the 13th International Workshop on Semantic Evaluation","author":"Hopkins","year":"2019"},{"key":"2023092014493531000_bib42","doi-asserted-by":"publisher","first-page":"887","DOI":"10.18653\/v1\/P16-1084","article-title":"How well do computers solve math word problems? Large-scale dataset construction and evaluation","volume-title":"Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)","author":"Huang","year":"2016"},{"key":"2023092014493531000_bib43","first-page":"2235","article-title":"Deepmath-deep sequence models for premise selection","volume-title":"Advances in Neural Information Processing Systems","author":"Irving","year":"2016"},{"key":"2023092014493531000_bib44","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.eacl-main.74","article-title":"Leveraging passage retrieval with generative models for open domain question answering","author":"Izacard","year":"2020","journal-title":"arXiv preprint arXiv:2007.01282"},{"key":"2023092014493531000_bib45","article-title":"Learning to reason deductively: Math word problem solving as complex relation extraction","author":"Jie","year":"2022","journal-title":"arXiv preprint arXiv:2203.10316"},{"key":"2023092014493531000_bib46","doi-asserted-by":"crossref","first-page":"3102","DOI":"10.18653\/v1\/2021.findings-emnlp.266","article-title":"Modeling mathematical notation semantics in academic papers","volume-title":"Findings of the Association for Computational Linguistics: EMNLP 2021","author":"Jo","year":"2021"},{"key":"2023092014493531000_bib47","first-page":"119","article-title":"Snlp at textgraphs 2022 shared task: Unsupervised natural language premise selection in mathematical texts using sentence-mpnet","volume-title":"Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing","author":"Kadusabe","year":"2022"},{"key":"2023092014493531000_bib48","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-20615-8_19","article-title":"Formalizing physics: Automation, presentation and foundation issues","volume-title":"International Conference on Intelligent Computer Mathematics","author":"Kaliszyk","year":"2015"},{"key":"2023092014493531000_bib49","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-22102-1_15","article-title":"Learning to parse on aligned corpora (rough diamond)","volume-title":"International Conference on Interactive Theorem Proving","author":"Kaliszyk","year":"2015"},{"key":"2023092014493531000_bib50","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.emnlp-main.550","article-title":"Dense passage retrieval for open-domain question answering","author":"Karpukhin","year":"2020","journal-title":"arXiv preprint arXiv:2004.04906"},{"key":"2023092014493531000_bib51","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/3397271.3401075","article-title":"Colbert: Efficient and effective passage search via contextualized late interaction over bert","volume-title":"Proceedings of the 43rd International ACM SIGIR Conference on Research and Development in Information Retrieval","author":"Khattab","year":"2020"},{"key":"2023092014493531000_bib52","doi-asserted-by":"publisher","first-page":"3768","DOI":"10.18653\/v1\/2020.emnlp-main.308","article-title":"Point to the expression: Solving algebraic word problems using the expression-pointer transformer model","volume-title":"Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)","author":"Kim","year":"2020"},{"key":"2023092014493531000_bib53","doi-asserted-by":"publisher","first-page":"1152","DOI":"10.18653\/v1\/N16-1136","article-title":"Mawps: A math word problem repository","volume-title":"Proceedings of the 2016 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies","author":"Koncel-Kedziorski","year":"2016"},{"key":"2023092014493531000_bib54","first-page":"127","article-title":"Textgraphs-16 natural language premise selection task: Zero-shot premise selection with prompting generative language models","volume-title":"Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing","author":"Kovriguina","year":"2022"},{"issue":"11","key":"2023092014493531000_bib55","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1045\/november14-kristianto","article-title":"Extracting textual descriptions of mathematical expressions in scientific papers","volume":"20","author":"Kristianto","year":"2014","journal-title":"D-Lib Magazine"},{"key":"2023092014493531000_bib56","first-page":"1","article-title":"Extracting definitions of mathematical expressions in scientific papers","volume-title":"Proceedings of the 26th Annual Conference of JSAI","author":"Kristianto","year":"2012"},{"key":"2023092014493531000_bib57","article-title":"Mcat math retrieval system for ntcir-12 mathir task.","volume-title":"NTCIR","author":"Kristianto","year":"2016"},{"key":"2023092014493531000_bib58","article-title":"The mcat math retrieval system for ntcir-11 math track.","volume-title":"NTCIR","author":"Kristianto","year":"2014"},{"issue":"38","key":"2023092014493531000_bib59","doi-asserted-by":"publisher","first-page":"8023","DOI":"10.1523\/JNEUROSCI.0269-21.2021","article-title":"Cortical processing of arithmetic and simple sentences in an auditory attention task","volume":"41","author":"Kulasingham","year":"2021","journal-title":"Journal of Neuroscience"},{"key":"2023092014493531000_bib60","doi-asserted-by":"publisher","first-page":"271","DOI":"10.3115\/v1\/P14-1026","article-title":"Learning to automatically solve algebra word problems","volume-title":"Proceedings of the 52nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)","author":"Kushman","year":"2014"},{"key":"2023092014493531000_bib61","doi-asserted-by":"publisher","first-page":"1671","DOI":"10.18653\/v1\/2022.semeval-1.230","article-title":"Semeval 2022 task 12: Symlink-linking mathematical symbols to their descriptions","volume-title":"Proceedings of the 16th International Workshop on Semantic Evaluation (SemEval-2022)","author":"Lai","year":"2022"},{"key":"2023092014493531000_bib62","article-title":"Cross-lingual language model pretraining","author":"Lample","year":"2019","journal-title":"arXiv preprint arXiv:1901.07291"},{"key":"2023092014493531000_bib63","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D18-1549","article-title":"Phrase-based & neural unsupervised machine translation","author":"Lample","year":"2018","journal-title":"arXiv preprint arXiv:1804 .07755"},{"key":"2023092014493531000_bib64","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/2724660.2724664","article-title":"Mathematical language processing: Automatic grading and feedback for open response mathematical questions","volume-title":"Proceedings of the Second (2015) ACM Conference on Learning@ Scale","author":"Lan","year":"2015"},{"key":"2023092014493531000_bib65","article-title":"Albert: A lite bert for self-supervised learning of language representations","author":"Lan","year":"2019","journal-title":"arXiv preprint arXiv:1909.11942"},{"key":"2023092014493531000_bib66","article-title":"Jbnu-cclab at semeval-2022 task 12: Fusing maximum entity information for linking mathematical symbols to their descriptions","author":"Lee","year":"2022"},{"key":"2023092014493531000_bib67","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.acl-main.703","article-title":"Bart: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension","author":"Lewis","year":"2019","journal-title":"arXiv preprint arXiv:1910.13461"},{"key":"2023092014493531000_bib68","article-title":"Solving quantitative reasoning problems with language models","author":"Lewkowycz","year":"2022","journal-title":"arXiv preprint arXiv: 2206.14858"},{"key":"2023092014493531000_bib69","article-title":"Graph-to-tree neural networks for learning structured input-output translation with applications to semantic parsing and math word problem","author":"Li","year":"2020","journal-title":"arXiv preprint arXiv:2004.13781"},{"key":"2023092014493531000_bib70","article-title":"A unified mrc framework for named entity recognition","author":"Li","year":"2019","journal-title":"arXiv preprint arXiv:1910.11476"},{"key":"2023092014493531000_bib71","article-title":"On the advance of making language models better reasoners","author":"Li","year":"2022","journal-title":"arXiv preprint arXiv:2206.02336"},{"key":"2023092014493531000_bib72","article-title":"Mwp-bert: A strong baseline for math word problems","author":"Liang","year":"2021","journal-title":"arXiv preprint arXiv:2107.13435"},{"key":"2023092014493531000_bib73","doi-asserted-by":"publisher","first-page":"4232","DOI":"10.1609\/aaai.v35i5.16547","article-title":"Hms: A hierarchical solver with dependency-enhanced understanding for math word problem","volume-title":"Thirty-Fifth AAAI Conference on Artificial 2021","author":"Lin","year":"2021"},{"key":"2023092014493531000_bib74","doi-asserted-by":"crossref","first-page":"2370","DOI":"10.18653\/v1\/D19-1241","article-title":"Tree-structured decoding for solving math word problems","volume-title":"Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP)","author":"Liu","year":"2019"},{"key":"2023092014493531000_bib75","article-title":"Roberta: A robustly optimized bert pretraining approach","author":"Liu","year":"2019","journal-title":"arXiv preprint arXiv:1907.11692"},{"key":"2023092014493531000_bib76","article-title":"Neural machine translation (seq2seq) tutorial","author":"Luong","year":"2017"},{"key":"2023092014493531000_bib77","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-030-99739-7_51","article-title":"Advancing math-aware search: The arqmath-3 lab at clef 2022","volume-title":"Advances in Information Retrieval: 44th European Conference on IR Research, ECIR 2022, Stavanger, Norway, April 10\u201314, 2022, Proceedings, Part II","author":"Mansouri","year":"2022"},{"key":"2023092014493531000_bib78","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13643-6_20","article-title":"Overview of arqmath-3 (2022): Third clef lab on answer retrieval for questions on math (working notes version)","author":"Mansouri","year":"2022","journal-title":"Working Notes of CLEF"},{"key":"2023092014493531000_bib79","first-page":"5","article-title":"Dprl systems in the clef 2022 arqmath lab: Introducing mathamr for math-aware search","author":"Mansouri","year":"2021","journal-title":"Proceedings of the Working Notes of CLEF 2022"},{"key":"2023092014493531000_bib80","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/3341981.3344235","article-title":"Tangent-cft: An embedding model for mathematical formulas","volume-title":"Proceedings of the 2019 ACM SIGIR International Conference on Theory of Information Retrieval","author":"Mansouri","year":"2019"},{"key":"2023092014493531000_bib81","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-030-85251-1_17","article-title":"Overview of arqmath-2 (2021): second clef lab on answer retrieval for questions on math","volume-title":"International Conference of the Cross-Language Evaluation Forum for European Languages","author":"Mansouri","year":"2021"},{"issue":"4","key":"2023092014493531000_bib82","doi-asserted-by":"publisher","first-page":"L042010","DOI":"10.1103\/PhysRevResearch.3.L042010","article-title":"Similarity-based equational inference in physics","volume":"3","author":"Meadows","year":"2021","journal-title":"Physical Review Research"},{"key":"2023092014493531000_bib83","article-title":"Efficient estimation of word representations in vector space","author":"Mikolov","year":"2013","journal-title":"arXiv preprint arXiv:1301.3781"},{"key":"2023092014493531000_bib84","article-title":"Lila: A unified benchmark for mathematical reasoning","author":"Mishra","year":"2022","journal-title":"arXiv preprint arXiv:2210.17517"},{"key":"2023092014493531000_bib85","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","article-title":"The lean theorem prover (system description)","volume-title":"International Conference on Automated Deduction","author":"de Moura","year":"2015"},{"key":"2023092014493531000_bib86","article-title":"Mathematical language processing project","author":"Pagael","year":"2014","journal-title":"arXiv preprint arXiv:1407.0167"},{"key":"2023092014493531000_bib87","article-title":"Combining tf-idf text retrieval with an inverted index over symbol pairs in math expressions: The tangent math search engine at ntcir 2014.","volume-title":"NTCIR","author":"Pattaniyil","year":"2014"},{"key":"2023092014493531000_bib88","article-title":"Mathbert: A pre-trained model for mathematical formula understanding","author":"Peng","year":"2021","journal-title":"arXiv preprint arXiv:2105.00377"},{"key":"2023092014493531000_bib89","article-title":"Team an (l) p at semeval-2022 task 12: Building a lightweight symbol recognition system","author":"Ping","year":"2022"},{"key":"2023092014493531000_bib90","article-title":"Generative language modeling for automated theorem proving","author":"Polu","year":"2020","journal-title":"arXiv preprint arXiv:2009.03393"},{"key":"2023092014493531000_bib91","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.semeval-1.232","article-title":"Aifb-webscience at semeval-2022 task 12: Relation extraction first\u2013using relation extraction to identify entities","author":"Popovic","year":"2022","journal-title":"arXiv preprint arXiv:2203.05325"},{"key":"2023092014493531000_bib92","article-title":"Neural-symbolic solver for math word problems with auxiliary tasks","author":"Qin","year":"2021","journal-title":"arXiv preprint arXiv:2107 .01431"},{"key":"2023092014493531000_bib93","article-title":"Semantically-aligned universal tree-structured solver for math word problems","author":"Qin","year":"2020","journal-title":"arXiv preprint arXiv:2010 .06823"},{"key":"2023092014493531000_bib94","article-title":"Mathematical reasoning via self-supervised skip-tree training","author":"Rabe","year":"2020","journal-title":"arXiv preprint arXiv:2006.04757"},{"key":"2023092014493531000_bib95","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D19-1410","article-title":"Sentence-bert: Sentence embeddings using siamese bert-networks","author":"Reimers","year":"2019","journal-title":"arXiv preprint arXiv:1908 .10084"},{"key":"2023092014493531000_bib96","article-title":"Solving general arithmetic word problems","author":"Roy","year":"2016","journal-title":"arXiv preprint arXiv:1608.01413"},{"key":"2023092014493531000_bib97","first-page":"311","article-title":"An overview of the mizar project","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"Rudnicki","year":"1992"},{"key":"2023092014493531000_bib98","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1145\/2911451.2911503","article-title":"Semantification of identifiers in mathematics for better math information retrieval","volume-title":"Proceedings of the 39th International ACM SIGIR conference on Research and Development in Information Retrieval","author":"Schubotz","year":"2016"},{"key":"2023092014493531000_bib99","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-65813-1_7","article-title":"Evaluating and improving the extraction of mathematical identifier definitions","volume-title":"International Conference of the Cross-Language Evaluation Forum for European Languages","author":"Schubotz","year":"2017"},{"key":"2023092014493531000_bib100","first-page":"146","article-title":"Getting the units right.","volume-title":"FM4M\/MathUI\/ThEdu\/DP\/WIP@ CIKM","author":"Schubotz","year":"2016"},{"key":"2023092014493531000_bib101","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1145\/2766462.2767787","article-title":"Challenges of mathematical information retrievalin the ntcir-11 math wikipedia task","volume-title":"Proceedings of the 38th international ACM SIGIR conference on research and development in information retrieval","author":"Schubotz","year":"2015"},{"key":"2023092014493531000_bib102","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/N19-4008","article-title":"Eidos, indra, & delphi: From free text to executable causal models","volume-title":"Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics (Demonstrations)","author":"Sharp","year":"2019"},{"key":"2023092014493531000_bib103","doi-asserted-by":"publisher","first-page":"2924","DOI":"10.18653\/v1\/2020.coling-main.262","article-title":"Solving math word problems with multi-encoders and multi-decoders","volume-title":"Proceedings of the 28th International Conference on Computational Linguistics","author":"Shen","year":"2020"},{"key":"2023092014493531000_bib104","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1117\/12.2074084","article-title":"Math expression retrieval using an inverted index over symbol pairs","volume-title":"Document Recognition and Retrieval XXII","author":"Stalnaker","year":"2015"},{"key":"2023092014493531000_bib105","doi-asserted-by":"publisher","first-page":"303","DOI":"10.18653\/v1\/N18-1028","article-title":"Variable typing: Assigning meaning to variables in mathematical text","volume-title":"Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers)","author":"Stathopoulos","year":"2018"},{"key":"2023092014493531000_bib106","doi-asserted-by":"publisher","first-page":"334","DOI":"10.3115\/v1\/P15-2055","article-title":"Retrieval of research-level mathematical information needs: A test collection and technical terminology experiment","volume-title":"Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 2: Short Papers)","author":"Stathopoulos","year":"2015"},{"key":"2023092014493531000_bib107","first-page":"2344","article-title":"Mathematical information retrieval based on type embeddings and query expansion","volume-title":"Proceedings of COLING 2016, the 26th International Conference on Computational Linguistics: Technical Papers","author":"Stathopoulos","year":"2016"},{"issue":"2","key":"2023092014493531000_bib108","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","article-title":"The tptp problem library","volume":"21","author":"Sutcliffe","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"2023092014493531000_bib109","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53518-6_1","article-title":"A promising path towards autoformalization and general artificial intelligence","volume-title":"International Conference on Intelligent Computer Mathematics","author":"Szegedy","year":"2020"},{"key":"2023092014493531000_bib110","first-page":"114","article-title":"Ijs at textgraphs-16 natural language premise selection task: Will contextual information improve natural language premise selection?","volume-title":"Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing","author":"Tran","year":"2022"},{"key":"2023092014493531000_bib111","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15582-6_30","article-title":"Evaluation of automated theorem proving on the mizar mathematical library","volume-title":"International Congress on Mathematical Software","author":"Urban","year":"2010"},{"key":"2023092014493531000_bib112","first-page":"105","article-title":"TextGraphs 2022 shared task on natural language premise selection","volume-title":"Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing","author":"Valentino","year":"2022"},{"key":"2023092014493531000_bib113","first-page":"322","article-title":"Odin\u2019s runes: A rule language for information extraction","volume-title":"Proceedings of the Tenth International Conference on Language Resources and Evaluation (LREC\u201916)","author":"Valenzuela-Esc\u00e1rcega","year":"2016"},{"key":"2023092014493531000_bib114","article-title":"Attention is all you need","author":"Vaswani","year":"2017","journal-title":"arXiv preprint arXiv: 1706.03762"},{"key":"2023092014493531000_bib115","article-title":"Learning to prove theorems by learning to generate theorems","author":"Wang","year":"2020","journal-title":"arXiv preprint arXiv:2002.07019"},{"key":"2023092014493531000_bib116","article-title":"Premise selection for theorem proving by deep graph embedding","author":"Wang","year":"2017","journal-title":"arXiv preprint arXiv:1709.09994"},{"key":"2023092014493531000_bib117","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/3372885.3373827","article-title":"Exploration of neural machine translation in autoformalization of mathematics in mizar","volume-title":"Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"Wang","year":"2020"},{"key":"2023092014493531000_bib118","doi-asserted-by":"publisher","first-page":"845","DOI":"10.18653\/v1\/D17-1088","article-title":"Deep neural solver for math word problems","volume-title":"Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing","author":"Wang","year":"2017"},{"key":"2023092014493531000_bib119","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1109\/BigData52589.2021.9671942","article-title":"Mathematical formula representation via tree embeddings.","volume-title":"iTextbooks@ AIED","author":"Wang","year":"2021"},{"key":"2023092014493531000_bib120","article-title":"Naturalproofs: Mathematical theorem proving in natural language","author":"Welleck","year":"2021","journal-title":"arXiv preprint arXiv:2104.01112"},{"key":"2023092014493531000_bib121","article-title":"Towards grounded natural language proof generation","volume-title":"MathAI4Ed Workshop at NeurIPS","author":"Welleck","year":"2021"},{"key":"2023092014493531000_bib122","article-title":"Symbol declarations in mathematical writing","author":"Wolska","year":"2010"},{"key":"2023092014493531000_bib123","doi-asserted-by":"publisher","first-page":"25","DOI":"10.3115\/1218955.1218959","article-title":"Analysis of mixed natural and symbolic input in mathematical dialogs","volume-title":"Proceedings of the 42nd Annual Meeting of the Association for Computational Linguistics (ACL-04)","author":"Wolska","year":"2004"},{"key":"2023092014493531000_bib124","article-title":"Autoformalization with large language models","author":"Yuhuai","year":"2022"},{"key":"2023092014493531000_bib125","first-page":"11251","article-title":"Lime: Learning inductive bias for primitives of mathematical reasoning","volume-title":"International Conference on Machine Learning","author":"Yuhuai","year":"2021"},{"key":"2023092014493531000_bib126","doi-asserted-by":"publisher","first-page":"5299","DOI":"10.24963\/ijcai.2019\/736","article-title":"A goal-driven tree-structured neural model for math word problems.","volume-title":"IJCAI","author":"Xie","year":"2019"},{"key":"2023092014493531000_bib127","doi-asserted-by":"publisher","first-page":"9490","DOI":"10.1609\/aaai.v34i05.6493","article-title":"Automatic generation of headlines for online math questions.","volume-title":"AAAI","author":"Ke","year":"2020"},{"key":"2023092014493531000_bib128","article-title":"Ntcir-12 mathir task overview","volume-title":"NTCIR","author":"Zanibbi","year":"2016"},{"issue":"4","key":"2023092014493531000_bib129","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10032-011-0174-4","article-title":"Recognition and retrieval of mathematical expressions","volume":"15","author":"Zanibbi","year":"2011","journal-title":"International Journal on Document Analysis and Recognition (IJDAR)"},{"key":"2023092014493531000_bib130","doi-asserted-by":"publisher","DOI":"10.1145\/2911451.2911512","article-title":"The tangent search engine: Improved similarity metrics and scalability for math formula search","author":"Zanibbi","year":"2015","journal-title":"arXiv preprint arXiv:1507.06235"},{"key":"2023092014493531000_bib131","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/2911451.2911512","article-title":"Multi-stage math formula search: Using appearance-based similarity metrics at scale","volume-title":"Proceedings of the 39th International ACM SIGIR conference on Research and Development in Information Retrieval","author":"Zanibbi","year":"2016"},{"issue":"9","key":"2023092014493531000_bib132","doi-asserted-by":"publisher","first-page":"2287","DOI":"10.1109\/TPAMI.2019.2914054","article-title":"The gap of semantic parsing: A survey on automatic math word problem solvers","volume":"42","author":"Zhang","year":"2019","journal-title":"IEEE Transactions on Pattern Analysis and Machine Intelligence"},{"key":"2023092014493531000_bib133","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.acl-main.362","article-title":"Graph-to-tree learning for solving math word problems","author":"Zhang","year":"2020"},{"key":"2023092014493531000_bib134","article-title":"Link prediction based on graph neural networks","author":"Zhang","year":"2018","journal-title":"arXiv preprint arXiv:1802.09691"},{"key":"2023092014493531000_bib135","article-title":"Multi-view reasoning: Consistent contrastive learning for math word problem","author":"Zhang","year":"2022","journal-title":"arXiv preprint arXiv:2210.11694"},{"key":"2023092014493531000_bib136","doi-asserted-by":"publisher","DOI":"10.1109\/TASLP.2022.3145314","article-title":"Hgen: Learning hierarchical heterogeneous graph encoding for math word problem solving","author":"Yi","year":"2022","journal-title":"IEEE\/ACM Transactions on Audio, Speech, and Language Processing"},{"key":"2023092014493531000_bib137","article-title":"Minif2f: A cross-system benchmark for formal olympiad-level mathematics","author":"Zheng","year":"2021","journal-title":"arXiv preprint arXiv:2109.00110"},{"key":"2023092014493531000_bib138","doi-asserted-by":"publisher","first-page":"714","DOI":"10.1007\/978-3-030-45439-5_47","article-title":"Accelerating substructure similarity search for formula retrieval","volume-title":"European Conference on Information Retrieval","author":"Zhong","year":"2020"},{"key":"2023092014493531000_bib139","article-title":"Evaluating token-level and passage-level dense retrieval models for math information retrieval","author":"Zhong","year":"2022","journal-title":"arXiv preprint arXiv:2203.11163"},{"key":"2023092014493531000_bib140","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-030-31624-2","article-title":"Structural similarity search for formulas using leaf-root paths in operator subtrees","volume-title":"European Conference on Information Retrieval","author":"Zhong","year":"2019"},{"key":"2023092014493531000_bib141","article-title":"Understanding mathematical discourse","volume-title":"Proceedings of the Workshop on the Semantics and Pragmatics of Dialogue, Amsterdam University","author":"Zinn","year":"1999"},{"issue":"4","key":"2023092014493531000_bib142","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1093\/jigpal\/11.4.457","article-title":"A computational framework for understanding mathematical discoursexy","volume":"11","author":"Zinn","year":"2003","journal-title":"Logic Journal of IGPL"}],"container-title":["Transactions of the Association for Computational Linguistics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/direct.mit.edu\/tacl\/article-pdf\/doi\/10.1162\/tacl_a_00594\/2159104\/tacl_a_00594.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/direct.mit.edu\/tacl\/article-pdf\/doi\/10.1162\/tacl_a_00594\/2159104\/tacl_a_00594.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,20]],"date-time":"2023-09-20T15:03:44Z","timestamp":1695222224000},"score":1,"resource":{"primary":{"URL":"https:\/\/direct.mit.edu\/tacl\/article\/doi\/10.1162\/tacl_a_00594\/117587\/Introduction-to-Mathematical-Language-Processing"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":142,"URL":"https:\/\/doi.org\/10.1162\/tacl_a_00594","relation":{},"ISSN":["2307-387X"],"issn-type":[{"value":"2307-387X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023]]},"published":{"date-parts":[[2023]]}}}