1 of 21

Premise Selection in Natural Language:

Finding supporting facts for mathematical statements

(Work in Progress)

Deborah Ferreira

deborah.ferreira@manchester.ac.uk

University of Manchester

2 of 21

Motivational Example

?

Proposition...

Premise

?

Proposition...

E=mc²

3 of 21

Why not use ATPs?

Non trivial!

4 of 21

Starting question...

Can we adapt Natural Language Processing techniques in order to understand corpora containing mathematical text?

​

Focus: Natural Language Premise Selection

5 of 21

Natural Language Premise Selection

Definition (Natural Language Premise Selection): Given a set of premises (or supporting facts) P in a mathematical corpus (containing both natural language and mathematical elements) and a new conjecture c proposed by a user, predict those premises from P that will most likely be useful for generating a proof for c.

6 of 21

Natural Language Premise Selection

​

Mathematical KB

Conjecture

Premise 1

Premise 2

Premise n

...

Model

7 of 21

Natural Language premise selection: Example

Premises

8 of 21

Natural Language premise selection

9 of 21

Data Source: ProofWiki

10 of 21

Reframing as binary classification problem

From a set of possible premises of size n + 1, select the one that is useful for proving a conjecture c.

​

Conjecture

Premise

Not Premise

n=1

Premise

Not Premise

n=2

Premise

Not Premise

n=5

Premise

Not Premise

n=10

Not Premise

Not Premise

Not Premise

Not Premise

Not Premise

Not Premise

Not Premise

Not Premise

….

11 of 21

Reframing as binary classification problem

Conjecture - Premise Pairs.

Goal: Classify as True or False.

Selection of Distracting Premises:

  1. Random
  2. Lexical similarity to real premises.

Number of distractors

12 of 21

Handling Mathematical Text

​

  • How to deal with the dual modality contained in the mathematical text?

​

  • Solution: Represent mathematical language and natural language as two different languages.

13 of 21

Statement Representation

(STAR)

14 of 21

Combining Representations

Is B a premise to A?

15 of 21

Our Baseline:

16 of 21

Selecting Random Distracting Premises

Our Approach

Baseline

17 of 21

Selecting Similar Distracting Premises

Our Approach

Baseline

18 of 21

Transferring Knowledge between different areas

AA: Abstract Algebra

ST: Set Theory

TP: Topology

Our Approach

Baseline

19 of 21

Qualitative Analysis

20 of 21

Comparison with other baselines

21 of 21

Conclusion

  • We can adapt NLP techniques for mathematical text.
  • Representing mathematical language separately from natural language achieves better performance with STAR.
  • STAR also is able to transfer better the knowledge between different areas of mathematics.
  • Dealing with a large number of distractors is still a challenge (n>10).

Thanks for your attention!

Questions?