Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs
By Wenda Li, Lei Yu, Yuhuai Wu, Lawrence Charles Paulson. 2020
10 citations recorded by the source corpus.
Mathematical proofs can be mechanised using proof assistants to eliminate gaps and errors. However, mechanisation still requires intensive labour. To promote automation, it is essential to capture high-level human mathematical reasoning, which we address as the problem of generating suitable propositions. We build a non-synthetic dataset from the largest repository of mechanised proofs and propose a task on causal reasoning, where a model is required to fill in a missing intermediate proposition given a causal context. Our experiments (using various neural sequence-to-sequence models) reveal that while the task is challenging, neural models can indeed capture non-trivial mathematical reasoning. We further propose a hierarchical transformer model that outperforms the transformer baseline.
Subfields: Natural Language Processing
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Natural Language Processing
- Yuhuai Wu
- Markus Norman Rabe
- Wenda Li
- Dawn Song
- Kshitij Bansal
- Steven Basart
- Roger Baker Grosse
- Jimmy Ba
Citations in the corpus
- Measuring Mathematical Problem Solving With the MATH Dataset (2021, background): “These benchmarks can be approached with seq2seq (Sutskever et al., 2014) Transformers which have traction on the problem (Polu and Sutskever, 2020; Rabe et al., 2020; Li et al., 2020). et al. (2020).”
- LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, methodology): “Compared to other ITPs, MetaMath is a low-level proving system: each proof step makes only a small step towards the goal.”
- Mathematical Reasoning via Self-supervised Skip-tree Training (2020, background): “Also, very recently, Li et al. [2020] applied language modeling to proofs of formal mathematics.”
- Teaching Temporal Logics to Neural Networks (2020, background): “, 2018), interactive theorem provers (Kaliszyk et al., 2017; Bansal et al., 2019; Huang et al., 2018; Yang & Deng, 2019; Polu & Sutskever, 2020; Wu et al., 2020; Li et al., 2020; Lee et al., 2020; Urban & Jakubv, 2020; Rabe et al., 2020), symbolic mathematics (Lample & Charton, 2020), and mathematic”