---
title: "Premise Selection in Natural Language Mathematical Texts (2020)"
description: "They build PS-ProofWiki, a corpus drawn from ProofWiki. 27 references, cited by 23 papers here."
authors: ["Deborah Ferreira", "André Freitas"]
year: 2020
venue: "Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics"
source: "https://aclanthology.org/2020.acl-main.657/"
doi: "10.18653/v1/2020.acl-main.657"
licence: "CC BY 4.0 (ACL Anthology)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ferreira-2020-premise-selection-natural-language-mathematical/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ferreira-2020-premise-selection-natural-language-mathematical/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/) / Premise Selection in Natural Language Mathematical Texts

# Premise Selection in Natural Language Mathematical Texts

**Authors:** [Deborah Ferreira](https://md.research.elamur.ai/free/en/authors/deborah-ferreira/) and [André Freitas](https://md.research.elamur.ai/free/en/authors/andre-freitas/) · **Year:** 2020 · **Venue:** [Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics](https://md.research.elamur.ai/free/en/venues/acl/) ([ACL 2020](https://md.research.elamur.ai/free/en/venues/acl/2020/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://aclanthology.org/2020.acl-main.657/) · [PDF](https://aclanthology.org/2020.acl-main.657.pdf) · [DOI 10.18653/v1/2020.acl-main.657](https://doi.org/10.18653/v1/2020.acl-main.657) · [OpenAlex](https://openalex.org/W3034902472)

**Citations:** 21 citations (OpenAlex, 2026-10-14) · [23](https://md.research.elamur.ai/free/en/papers/ferreira-2020-premise-selection-natural-language-mathematical/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
In automated theorem proving, premise selection usually works on formal logic, which covers little of mathematics and is hard for people to read. Ferreira and Freitas move the task to ordinary mathematical prose mixed with LaTeX formulae. Given a new conjecture, the system should pick out the theorems, definitions and axioms that would likely help prove it.

They build PS-ProofWiki, a corpus drawn from ProofWiki. Statements become nodes in a directed graph, and each "is used to prove" link becomes an edge. Premise selection is then treated as link prediction with a Deep Graph Convolutional Neural Network (DGCNN). The model classifies small enclosing subgraphs around candidate statement pairs. Each node combines a structural label from Double-Radius Node Labelling (DRNL), adapted here to directed graphs, with an embedding of the node's text.

Against a fine-tuned BERT baseline, the graph model improves F1 by about 41% (relative). It also degrades far less as negative examples increase and handles multi-hop premises better. The authors conclude that the dependency structure between proofs carries signal that text similarity alone misses.

## Key points
- **Corpus:** PS-ProofWiki has over 18,000 entries averaging about 289 characters and symbols. Around 10k statements can serve as premises, and 6,866 statements have only one to three dependants, so positive pairs are rare and the data is highly imbalanced. A smaller trigonometry subset, PS-ProofWiki TRIG, provides a more constrained setting.
- **Main result (30 negatives per positive):**
  - On full PS-ProofWiki, F1 rose from 34.1 (BERT) to 48.1 for the DGCNN model.
  - On PS-ProofWiki TRIG, F1 rose from 29.1 to 40.5 (about +39% relative).
- **Imbalance robustness:** As random negatives were added, the BERT classifier's F1 fell sharply toward near zero. The proposed model's F1 dropped by only about 25%.
- **Transitive (n-hop) premises:** These were tested on PS-ProofWiki TRIG with 10 negatives per positive.
  - At 2 hops, F1 was 61.0 for the DGCNN model versus 59.3 for BERT.
  - At 3 hops, F1 was 61.2 versus 49.2, a 24% relative gain.
- **Error analysis:** The model handles formula-heavy statements poorly. The authors call for embeddings that capture operator semantics, which neither PV-DM (Doc2Vec) nor BERT provides, and suggest pretraining BERT on mathematical text as future work.

*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 Manchester](https://md.research.elamur.ai/free/en/universities/university-of-manchester/) — University, Manchester, United Kingdom · 93 works · 45,138 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,450 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,296 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Deborah Ferreira and André Freitas. 2020. Premise Selection in Natural Language Mathematical Texts. Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{ferreira2020premise,
  title = {{Premise Selection in Natural Language Mathematical Texts}},
  author = {Deborah Ferreira and André Freitas},
  booktitle = {Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics},
  year = {2020},
  doi = {10.18653/v1/2020.acl-main.657},
  url = {https://doi.org/10.18653/v1/2020.acl-main.657}
}
```

- [← previous Joint Diacritization, Lemmatization, Normalization, and Fine-Grained Morphological Tagging](https://md.research.elamur.ai/free/en/papers/zalmout-2020-joint-diacritization-lemmatization-normalization-fine/)
- [next → Edition 1.2 of the PARSEME Shared Task on Semi-supervised Identification of Verbal Multiword Expressions](https://md.research.elamur.ai/free/en/papers/ramisch-2020-edition-1-2-parseme-shared/)
- [↑ back to papers of 2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/)

## References

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

1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. 2014. Premise selection for mathematics by corpus analysis and kernel methods. Journal of Automated Reasoning, 52(2):191–213. [find](https://scholar.google.com/scholar?q=Jesse+Alama%2C+Tom+Heskes%2C+Daniel+Ku%CC%88hlwein%2C+Evgeni+Tsivtsivadze%2C+and+Josef+Urban%2E+2014%2E+Premise+selection+for+mathematics+by+corpus+analysis+and+kernel+methods%2E+Journal+of+Automated+Reasoning%2C+52%282%29%3A19)
2. Marcos Cramer, Bernhard Fisseni, Peter Koepke, Daniel Kühlwein, Bernhard Schröder, and Jip Veldman. 2009. The naproche project controlled natural language proof checking of mathematical texts. In International Workshop on Controlled Natural Language, pages 170–186. Springer. [find](https://scholar.google.com/scholar?q=Marcos+Cramer%2C+Bernhard+Fisseni%2C+Peter+Koepke%2C+Daniel+Ku%CC%88hlwein%2C+Bernhard+Schro%CC%88der%2C+and+Jip+Veldman%2E+2009%2E+The+naproche+project+controlled+natural+language+proof+checking+of+mathematical+texts%2E+In+In)
3. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2018. [Bert: Pre-training of deep bidirectional transformers for language understanding](https://md.research.elamur.ai/free/en/papers/devlin-2019-bert-pre-training-deep-bidirectional/). arXiv preprint arXiv:1810.04805.
4. Thibault Gauthier and Cezary Kaliszyk. 2015. Premise selection and external provers for hol4. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pages 49–57, New York, NY, USA. ACM. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier+and+Cezary+Kaliszyk%2E+2015%2E+Premise+selection+and+external+provers+for+hol4%2E+In+Proceedings+of+the+2015+Conference+on+Certified+Programs+and+Proofs%2C+CPP+%E2%80%9915%2C+pages+49%E2%80%9357%2C+New+York%2C+NY)
5. Andr Greiner-Petter, Terry Ruas, Moritz Schubotz, Akiko Aizawa, William Grosky, and Bela Gipp. 2019. Why Machines Cannot Learn Mathematics, Yet. (July). [find](https://scholar.google.com/scholar?q=Andr+Greiner%2DPetter%2C+Terry+Ruas%2C+Moritz+Schubotz%2C+Akiko+Aizawa%2C+William+Grosky%2C+and+Bela+Gipp%2E+2019%2E+Why+Machines+Cannot+Learn+Mathematics%2C+Yet%2E+%28July%29%2E)
6. Danqing Huang, Shuming Shi, Chin-Yew Lin, Jian Yin, and Wei-Ying Ma. 2016. How well do computers solve math word problems? large-scale dataset construction and evaluation. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), volume 1, pa… [find](https://scholar.google.com/scholar?q=Danqing+Huang%2C+Shuming+Shi%2C+Chin%2DYew+Lin%2C+Jian+Yin%2C+and+Wei%2DYing+Ma%2E+2016%2E+How+well+do+computers+solve+math+word+problems%3F+large%2Dscale+dataset+construction+and+evaluation%2E+In+Proceedings+of+the+54th+A)
7. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. 2016. [Deepmath-deep sequence models for premise selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/). In Advances in Neural Information Processing Systems, pages 2235–2243.
8. Kriste Krstovski and David M Blei. 2018. Equation embeddings. arXiv preprint arXiv:1803.09123. [find](https://scholar.google.com/scholar?q=Kriste+Krstovski+and+David+M+Blei%2E+2018%2E+Equation+embeddings%2E+arXiv+preprint+arXiv%3A1803%2E09123%2E)
9. Quoc Le and Tomas Mikolov. 2014. [Distributed representations of sentences and documents](https://md.research.elamur.ai/free/en/papers/le-2014-distributed-representations-sentences-documents/). In International Conference on Machine Learning, pages 1188–1196.
10. Behrooz Mansouri, Shaurya Rohatgi, Douglas W Oard, Jian Wu, C Lee Giles, and Richard Zanibbi. 2019. Tangent-cft: An embedding model for mathematical formulas. [find](https://scholar.google.com/scholar?q=Behrooz+Mansouri%2C+Shaurya+Rohatgi%2C+Douglas+W+Oard%2C+Jian+Wu%2C+C+Lee+Giles%2C+and+Richard+Zanibbi%2E+2019%2E+Tangent%2Dcft%3A+An+embedding+model+for+mathematical+formulas%2E)
11. Michael Färber and Cezary Kaliszyk. 2015. Random forests for premise selection. In Frontiers of Combining Systems, pages 325–340, Cham. Springer International Publishing. [find](https://scholar.google.com/scholar?q=Michael+Fa%CC%88rber+and+Cezary+Kaliszyk%2E+2015%2E+Random+forests+for+premise+selection%2E+In+Frontiers+of+Combining+Systems%2C+pages+325%E2%80%93340%2C+Cham%2E+Springer+International+Publishing%2E)
12. Mathias Niepert, Mohamed Ahmed, and Konstantin Kutzkov. 2016. Learning convolutional neural networks for graphs. In Proceedings of the 33rd International Conference on International Conference on Machine Learning - Volume 48, ICML’16, pages 2014–2023. JMLR.org. [find](https://scholar.google.com/scholar?q=Mathias+Niepert%2C+Mohamed+Ahmed%2C+and+Konstantin+Kutzkov%2E+2016%2E+Learning+convolutional+neural+networks+for+graphs%2E+In+Proceedings+of+the+33rd+International+Conference+on+International+Conference+on+Mach)
13. Deborah Ferreira and Andre Freitas. 2020. Natural language premise selection: Finding supporting statements for mathematical texts. 12th Language Resources and Evaluation Conference (LREC), Marseille, France. [find](https://scholar.google.com/scholar?q=Deborah+Ferreira+and+Andre+Freitas%2E+2020%2E+Natural+language+premise+selection%3A+Finding+supporting+statements+for+mathematical+texts%2E+12th+Language+Resources+and+Evaluation+Conference+%28LREC%29%2C+Marseille%2C)
14. Vivian Dos Santos Silva, Siegfried Handschuh, and André Freitas. 2018. Recognizing and justifying text entailment through distributional navigation on definition graphs. In AAAI. [find](https://scholar.google.com/scholar?q=Vivian+Dos+Santos+Silva%2C+Siegfried+Handschuh%2C+and+Andre%CC%81+Freitas%2E+2018%2E+Recognizing+and+justifying+text+entailment+through+distributional+navigation+on+definition+graphs%2E+In+AAAI%2E)
15. André Freitas, Joao Carlos Pereira da Silva, Edward Curry, and Paul Buitelaar. 2014. A distributional semantics approach for selective reasoning on commonsense graph knowledge bases. In International Conference on Applications of Natural Language to Data Bases/Information Systems, pages 21–32. Spri… [find](https://scholar.google.com/scholar?q=Andre%CC%81+Freitas%2C+Joao+Carlos+Pereira+da+Silva%2C+Edward+Curry%2C+and+Paul+Buitelaar%2E+2014%2E+A+distributional+semantics+approach+for+selective+reasoning+on+commonsense+graph+knowledge+bases%2E+In+International)
16. M Ganesalingam and William Timothy Gowers. 2017. A fully automatic theorem prover with human-style output. Journal of Automated Reasoning, 58(2):253–291. [find](https://scholar.google.com/scholar?q=M+Ganesalingam+and+William+Timothy+Gowers%2E+2017%2E+A+fully+automatic+theorem+prover+with+human%2Dstyle+output%2E+Journal+of+Automated+Reasoning%2C+58%282%29%3A253%E2%80%93291%2E)
17. Mohan Ganesalingam. 2013. The language of mathematics. In The Language of Mathematics, pages 17–38. Springer. [find](https://scholar.google.com/scholar?q=Mohan+Ganesalingam%2E+2013%2E+The+language+of+mathematics%2E+In+The+Language+of+Mathematics%2C+pages+17%E2%80%9338%2E+Springer%2E)
18. Vivian S Silva, André Freitas, and Siegfried Handschuh. 2019. Exploring knowledge graphs in an interpretable composite approach for text entailment. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pages 7023–7030. [find](https://scholar.google.com/scholar?q=Vivian+S+Silva%2C+Andre%CC%81+Freitas%2C+and+Siegfried+Handschuh%2E+2019%2E+Exploring+knowledge+graphs+in+an+interpretable+composite+approach+for+text+entailment%2E+In+Proceedings+of+the+AAAI+Conference+on+Artificia)
19. Daniel Solow. 2002. How to read and do proofs an introduction to mathematical thought processes. [find](https://scholar.google.com/scholar?q=Daniel+Solow%2E+2002%2E+How+to+read+and+do+proofs+an+introduction+to+mathematical+thought+processes%2E)
20. Marco Valentino, Mokanarangan Thayaparan, and Andr Freitas. 2020. Unification-based reconstruction of explanations for science questions. [find](https://scholar.google.com/scholar?q=Marco+Valentino%2C+Mokanarangan+Thayaparan%2C+and+Andr+Freitas%2E+2020%2E+Unification%2Dbased+reconstruction+of+explanations+for+science+questions%2E)
21. Eric Wallace, Yizhong Wang, Sujian Li, Sameer Singh, and Matt Gardner. 2019. [Do nlp models know numbers? probing numeracy in embeddings](https://md.research.elamur.ai/free/en/papers/wallace-2019-do-nlp-models-know-numbers/). arXiv preprint arXiv:1909.07940.
22. Lei Wang, Yan Wang, Deng Cai, Dongxiang Zhang, and Xiaojiang Liu. 2018. Translating a math word problem to an expression tree. arXiv preprint arXiv:1811.05632. [find](https://scholar.google.com/scholar?q=Lei+Wang%2C+Yan+Wang%2C+Deng+Cai%2C+Dongxiang+Zhang%2C+and+Xiaojiang+Liu%2E+2018%2E+Translating+a+math+word+problem+to+an+expression+tree%2E+arXiv+preprint+arXiv%3A1811%2E05632%2E)
23. Zhipeng Xie and Shichao Sun. 2019. A goal-driven tree-structured neural model for math word problems. In Proceedings of the 28th International Joint Conference on Artificial Intelligence, pages 5299– 5305. AAAI Press. [find](https://scholar.google.com/scholar?q=Zhipeng+Xie+and+Shichao+Sun%2E+2019%2E+A+goal%2Ddriven+tree%2Dstructured+neural+model+for+math+word+problems%2E+In+Proceedings+of+the+28th+International+Joint+Conference+on+Artificial+Intelligence%2C+pages+5299%E2%80%93+)
24. Muhan Zhang and Yixin Chen. 2018. Link prediction based on graph neural networks. In Advances in Neural Information Processing Systems, pages 5165–5175. [find](https://scholar.google.com/scholar?q=Muhan+Zhang+and+Yixin+Chen%2E+2018%2E+Link+prediction+based+on+graph+neural+networks%2E+In+Advances+in+Neural+Information+Processing+Systems%2C+pages+5165%E2%80%935175%2E)
25. Muhan Zhang, Zhicheng Cui, Marion Neumann, and Yixin Chen. 2018. An end-to-end deep learning architecture for graph classification. In Thirty-Second AAAI Conference on Artificial Intelligence. [find](https://scholar.google.com/scholar?q=Muhan+Zhang%2C+Zhicheng+Cui%2C+Marion+Neumann%2C+and+Yixin+Chen%2E+2018%2E+An+end%2Dto%2Dend+deep+learning+architecture+for+graph+classification%2E+In+Thirty%2DSecond+AAAI+Conference+on+Artificial+Intelligence%2E)
26. Claus Zinn. 2003. A computational framework for understanding mathematical discourse. Logic Journal of IGPL, 11(4):457–484. [find](https://scholar.google.com/scholar?q=Claus+Zinn%2E+2003%2E+A+computational+framework+for+understanding+mathematical+discourse%2E+Logic+Journal+of+IGPL%2C+11%284%29%3A457%E2%80%93484%2E)
27. Yanyan Zou and Wei Lu. 2019. Text2math: End-to-end parsing text into math expressions. arXiv preprint arXiv:1910.06571. [find](https://scholar.google.com/scholar?q=Yanyan+Zou+and+Wei+Lu%2E+2019%2E+Text2math%3A+End%2Dto%2Dend+parsing+text+into+math+expressions%2E+arXiv+preprint+arXiv%3A1910%2E06571%2E)

*Updated 2 November 2026*