NaturalProver: Grounded Mathematical Proof Generation with Language Models
Authors: Sean Welleck
Jiacheng Liu
Ximing Lu
Hannaneh Hajishirzi
Yejin Choi
Venue: NeurIPS 2022 Accept (2022)
Keywords: language modeling
reasoning
neural theorem proving

Abstract: Theorem proving in natural mathematical language – the mixture of symbolic and natural language used by humans – plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet it has remained underexplored with modern generative models. We study large-scale language models on two new generation tasks: suggesting the next step in a mathematical proof, and full proof generation. We develop NaturalProver, a language model that generates proofs by conditioning on background references (e.g. theorems and definitions that are either retrieved or human-provided), and optionally enforces their presence with constrained decoding. On theorems from the NaturalProofs benchmark, NaturalProver improves the quality of next-step suggestions and generated proofs over fine-tuned GPT-3, according to human evaluations from university-level mathematics students. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time, which is to our knowledge the first demonstration of these capabilities using neural language models.

NATURAL,RRVER: Grounded Mathematical Proof Generation with Language Models
Sean Welleck 1.2" JJacheng Liu Ximing Lu², Hannaneh Hajishirzi Yejin Choi
Paul G. Allen School of Computer Science & Engineering, University of Washington 2 Allen Institute for Artificial Intelligence, "Equal contribution wellecks@uw.c edu
Abstract
Theorem proving in natural mathematical language the mixture of symbolic and natural language used humans - plays central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet it has remained underexplored with modern generative models. We study large- scale language models on two new generation tasks: suggesting the next step in a mathematical proof, and full proof generation. We develop NATURAL PROVERR language model that generates proofs by conditioning on background references (e.g. theorems and definitions that are either retrieved or proaaddrrovddd), and optionally enforces their presence with constrained decoding. On theorems from the NATURALPROOM benchmark, NATURALPROVER improves the quality of next-step suggestions and generated proofs over fine-tuned GPT-3, according to human evaluations from university-level mathematics students. NATURALPROVER is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time, which is to our knowledge the first demonstration of these capabilities using neural language models
Generate with in-context reference titles and constrained decoding
Learn generate proofs and reconstruct references
Theoram
Theorem
Language Model
Constrained Decoding
The sum any finite number of even integers even.
By induction: N, Pin)...
integar. Then + oddi
Reference Titles
Referance Content
Even Integer
Generated Proof
Reference Even Integer
integer iff it is the form
Odd Integer
Proof by Consadiction: Aiming fora contediction,
Integer
4
Proof by Contradiction
exists an integer that This contradicte the premize that even
Henos, Proof
Figure I: NATURALPROVER proves Even Integer Plus 5 is Odd At training time, NATURAL obtains background knowledge about references (e.g. theorems or definitions) via reference recon- struction: learning to map reference's 's title to its content. At test time, NATURALPROVE its generations through in-context reference constraints that are retrieved or human human-provided. and optionally enforced with stepwise constrained decoding. This theorem's 's human -rrtt-nnrtte proof in ProofWiki contains an error and differs substantially from NATURALPROVER 's correct proof.
grounds
1 Coode and data available at
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Introduction
Constructing a rational argument that justifies a claim is a key aspect of explaining. verifying, and communicating ideas in situations ranging from everyday interactions, to legal and political discourse, to science and mathematics [10 1 24! Within the latter context, a mathematical proof sequence of logical arguments expressed in a mixture of symbolic and natural language assumes this role by providing justification and insight into why claim is true [12. Proofs operate on a relatively explicit and objective set of ground knowledge, isolating a subset of reasoning that is desirable for models that form the foundation of machine learning systems [3]. Moreover, we envision assistive systems that provide suggested proofs or next-steps, analogous to language- mooegge-mooll-bbaae based code suggestions (e.g. GitHub CoPilot (6) or formal proof assistants (e.g. GPT- fl (0) ). which could make learning using mathematics more productive and accessible.
To this end, we study the capabilities of large-scale language models (e.g. GPT-3 (5)) on two new theorem proving tasks in natural mathematical language: next-step suggestion, in which a model suggests the next step of proof, full full-proo) generation, in which a model fully proves claim. As proof's are grounded in knowledge from past results (e.g. theorems, definitions), analogous to facts deployed in a conversation [3, prior rulings used in legal opinion [16], or articles used to justify an answer BO), we develop a methodology for obtaining and using background knowledge to prove theorems with generic language model.
We develop NATURAI.ROVER, a language model that generates proofs by conditioning on back- ground references (e.g. theorems and definitions that are either retrieved or numan-providedd and optionally enforces their presence with a constrained decoding algorithm that leverages the multi-step structure of proofs. On collection of theorems from the NATURAL PROOrS benchmark A5 NAT- URALPROVER improves the quality of next-step suggestions and generated proof's over fine-tuned GPT-3, according to human evaluations from university-level mathematics students. NATURAL- PROVER is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated correct and useful more than 40% of the time, which is to knowledge the first demonstration of these capabilities using neural language models.
Along with these successes, we study deficiencies in our current models. We find that models can struggle with logical coherence on longer proofs, with providing valid justifications, and with performing multi-step symbolic derivations. Taken together, our tasks, methodology, and evaluation show the feasibility of language models as interactive aids in mathematics, along with open challenges.
2 NATURALPROOFS-GE Dataset and Tasks
We create a AATORAI.PROOF-- dataset adapted from NATURAL dataset for two tasks: suggesting the next step of proof, and fully proving theorem.
45 and use the
EXTURALPROOFS-GGER NATURALPROOFS- GEN adapts data from NATURALPROOFS, which contains theorem statements, proof', definitions, and additional pages (e.g. axioms, corollaries) sourced from Wrkof an online compendium of community-contribunt
mathematical proofs. In NATURALPROOFS GEN, each example (x. y) E D pairs theorem x with gold proof y, both of which are a mixture of text and LSTEX. 4S] split the examples and reference sets into training, dev, and test splits to ensure that no theorem in the dev or test splits mentioned in the training split. We adopt these splits of roughly 12.5k training, 1 validation, and 1 test examples, and sampled core evaluation sets with 100 dev and 100 test theorems that are used for human evaluation. The proofs contain additional structure, discussed next.
Multi-step proof structure. Each proof has a multi-step structure, meaning that proof y (Vi,..., ) is a variable-length token sequence that is segmented into proof steps, where each step Yi is itself a variable-length sequence of tokens (either text Latex). The segmentation is largely determined by ProofWiki's formatting and community standards for structuring proofs, and we additionally merge steps to ensure that each step contains non-trivial semantic content. For example, Figure I shows a stsp (generated) proof with each step highlighted in green.
References. Each proof mentions a variable-number of references (ri,...,,',, from a set R of roughly 33k theorems and definitions, analogous to how Wikipedia articles reference other pages. For example, Figure [ shows proof with reference mentions in blue. Each mention identifies

---

reference by its title and provides natural language surface form. For instance, in Figure I, the first proof step mentions the definition of even integer as even, which is formatted the proof as [[Def initiiiiinni Even Integer leven]] ] and tokenized along with the rest of the proof.
Tasks, We consider two tasks that are motivated by an assistive system that provides suggested proofs next-steps user. The full proof generation task is generate proof given theorem x. The next-step suggestion task is to generate a set of next steps {ur" k== given theorem x and proof history Veet from a gold proof. In each case, consider additional provided reference setting where the model is also given the set of references {ri..... FR,, } from gold proof of the theorem. The next-step task simulates human correctly proving the theorem up to point, then querying system for suggested next-steps when stuck, while the provided reference setting simulates a human specifying a plan for system that writes proof.
3 NATURALPROVER: Grounded Proof Generation via Language Modeling
We describe NATURAL PROVER,,ROVER, a language model which generates grounded proofs by conditioning on references and optionally enforcing their presence with constrained decoding.
Setup. Our objective is to generate correct proofs, ý = arg maxy correct(x, y). Unfortunately. evaluating proof correctness is costly, and is only done once test time. A naive approach is to approximate the objective, ý z arg maxy log (y(y)x), by fine-tuning language model examples and using decoding algorithm (e.g. greedy decoding). We instead investigate conditioning on background knowledge in the form of reference documents, Pa Py(y)x, R), which is beneficial
yx
in related generation settings (e.g. (88), and offers control over the generated proof. To do so, NATURALPROVER uses in-context references and reference reconstruction objective.
In-context references. Language models have limited context window that prevents conditioning on full documents. Instead, NATURALPROVER conditions on set of reference titles, pe ( Ratt). Concretely, we fine-tune on (theorem, reference titles, proof) sequences of the form,
<theoren> <title> (theoren-titie) </title> <oontent> (theoren-content) </content> </theoren>
<raf> (raf-title-1) </ref> <ref> (raf-title-R) </rot>
<proot> (proof) </proot>
with new-lines and { tokens omitted, relevant strings inserted, and loss only tokens after <proof>.
Reference reconstruction. Reference titles do not capture all of the information contained in the reference documents. We learn a mapping between each reference title and its underlying document with a reference reconstruction objective, po (r(tue)) for references r in the training reference set. Concretely, we fine-tune on additional (title, content) pairs of the form,
<(typo>>
<title> (title) </title> <content>
(comtent) </content> </<typo)>,
where the {type} is theorem/definitionnoltee and the loss is only on tokens after <content>, Intuitively, this lets the model associate each reference title with the reference's 's underlying content.
The joint objective.
For training, we minimize the joint loss,
(())
Σ
- log pe (ylx, Rutee) +
Σ rER
- log pe (r (T]Tins))
(3)
Dirain + Rirain
(
Evaluation-time references. We consider two settings for evaluation-time references: (i) retrieved references, from retrieval model fxx - (ri...., r.k., and (ii) human-prn proniddd references from the ground-truth proof. The retrieval setting simulates fully automated proof assistant, while the second simulates human specifying a plan for an assistant that writes proof, and acts as an upper bound for retrieval system optimized to predict references in a ground-truth proof.
3.1 Stepwise constrained decoding
In the provided-referrnce setting, the conditioned references are known to be relevant to correct. proof. We hypothesize that explicitly encouraging generated proofs to contain the references will improve correctness, by placing lexical constraints on the reference-titles at decoding time,
ý R3 arg max log pe (y) x, Raite) subject to 1 [[rate E y] = [Rade]s
Σ Frita Rate
(4)
y
3

---

where [[:] is an indicator function. To approximate this objective, we generate step-by-step by sampling multiple proof-ttep candidates, retaining those with high value (reference coverage and log-probability) in beam, and continuing to the next step, which we call stepwise beam search.
Value function. The search supports any function of the proof-so-far, v(yec) R. We use a value function that is a weighted combination of constraint satisfaction and log- log-probability.
(5) where Counstrain (Ug+) is the number of unique in-context reference-titles in yst. and ULM is log po (VVse). We normalize each term by dividing by the maximum absolute value among candidates.
Ca (yge) = O' (Uge) + (1 - a (VSM)))))
Stepwise beam search. The procedure generates a proof y = (y yT) by iteratively sampling and pruning next-proof-step candidates y/. Each iteration expands size-K beam of proofs-so-far, S = (1 by generating N next-step candidates.
(6) where q is a decoding algorithm (e.g. temperature sampling) and is concatenation. The next iteration's beam is formed by selecting the top scoring candidates, S, = arg top-Kyg.est vo (ysr). When proof in the beam terminates, it is not expanded further. The search ends when the beam consists of K terminated proofs. The highest value proof is returned as the final output.
- -y=. (y< ( o vy")
se ~ q(-lve,, x, R n=11
Stepwise++. We add two mechanisms for promoting exploration at each step. First, we expand each prefix in the beam (Eqn. 6 by sampling with multiple temperatures, {y ~ 9r (-1 x, Rate) T E (r)m=.) ). where 9- is sampling with temperature т. This relaxes the commitment temperature for all proof steps, balancing exploration (higher T) with exploitation (lower 7).
single
Second, rather than selecting the top-K candidates, we select clusters based on different value weights: S, = Va topx (S where S is the set candidates scored with Ua. and K' = k/e. This interpolates between selecting steps based on likelihood (low a:) and constraint satisfaction (high a).
Full proof sampling and greedy decoding. An alternative is to sample full proofs and select the best one according to the value function. This can be viewed as expansion (Eqn. 5 done at the full proof, rather than the step level. Moreover, greedy decoding corresponds to expanding only 1 candidate with temperature -> O. We formalize this in $D segment-level search that contains stepwise+*, full proof sampling, and greedy decoding as special cases.
4 Proof Evaluation
proof's correctness is contingent on a variety of factors, including reasoning with past results, performing symbolic derivations, and altogether providing sufficient evidence that the claim is true. We design a human-evaluation schema that isolates these aspects at the proof-step level, along with a full- summary. Table | the schema, which we overview below.
References. First, proofs involve deploying statements from references, such as applying a definition or adapting it to fit the context. Deployments should be consistent with the reference, e.g. deploying the definition of even integer as "..by definition, 3k E I 2k...', rather than '..3k E Z
2k 1', and are a common source of errors in student proofs 15
Second, proofs use references justification for steps of reasoning; for instance, Real Addition is Commutative provides justification for the statement x + y = + x where x, y E IR, but not for xy= = yv. This aspect is analogous to using article to justify claim (e.g. 30). Finally, proofs should not hallucinate references, or 'beg the question' by self-referencing the current theorem.
Proofs contain variety of multi-step derivations, ranging from simple arithmetic to more sophisticated derivations (c.g. see Table 17p. A derivation should start with a valid equation given the surrounding context (e.g. + x 2x in Table versus + x 3x). Each subsequent step should be a valid derivation from the previous step, e.g. stating = (2k + 6) - after y = 2k + 5.
Equations.
Other reasoning, language, & symbolic errors. A proof should provide sufficient evidence that a claim is true to a human reader; should not skip steps. Proof steps should make progress towards proving the goal; in particular, they should not repeat known conditions in the theorem or conclusions made a prior step. Finally, our schema leaves room for any other reasoning errors, as well as symbol errors (e.g. undefined symbols) and language errors (c.g. incomplete statements).

---

Error Type
Example
Reasoning: Reference
Invalid Deployment Invalid Justification
Since is an even integer. 31 E & x== 2k 1.
TB = Ei= P'Pr(X k) Power Series for Exponential Function
Hallucinated Ref.
From Power of Number are Irrational (Proving Pythagoras's Theorem:)
2/ is irrational.
Self Loop
From Pythagoras's 's Theorem, c² a² -a"+00 +b².
Reasoning: Equation
Invalid Equation
Ve E 2 + i = 3z.
Invalid Derivation
(Since is an even integer, +1 2r +1) = 2(r 11
Reasoning: Other
Skips Steps
(Ir E Z not multiple 3.) Therefore, x² = 1 or 8(mod 9)
Repetition Invalid (Other)
(Let AABC he right triangle.)
Then AACC is a right triangle.
(ar is an even integer.)
So, x + 1 is an even integer.
Language
Let va=ladd 6 be the
( (incomplete statement; ; unknown symbol aadd Let = zo (undefined operator o for real numbers )
Symbolic
(l.et.v E R.)
Table 1: Overview of human evaluation error schema. See Table 24 for full schema. Reference.
Hallucinated reference.
The necessary context (e.g. known conditions, prior steps).
Usefulness and correctness. To judge the potential utility of language models as assistive systems in natural mathematics, we measure whether generated next-steps and full proofs are potentially useful hints for proving the theorem one's own. Additionally, correctness. Note that an incorrect statement can still be helpful; for instance, it could give hint for the type of reference to use, derivation to perform, argument to make, etc.
measure a summary judgment of
Human evaluation protocol. We measure these aspects through human annotation at a step-wise and an overall level. For step-wise annotation, an annotator is presented with the theorem, proof-so-fit and a generated next-step. The annotator labels the (0, 1} correctness, usefulness, and presence of fine-grained errors outlined above. After labeling each step of proof, the annotator rates the full proof"s overall correctness and usefulness on 0-5 scale. A rating of 4 or 5 is needed to considered as correct, and rating of 3 or above is needed to be considered useful.
Automatic metries: lexical content. As automatic proxies for quality, we compare each generated proof against its ground ground-truth counterpart using the sentence-level n-gram matching metric GLEU [29], and following work in knowledge-grounde
dialogue t we use F1 overlap between generated
and ground- truth tokens. Prior to computing the metrics, we normalize the generated and ground- truth proofs by only keeping the surface form of references, removing formatting characters with MediaWiki parser, and collapsing any consecutive whitespace into single space.
Automatic metrics: knowledge grounding. We define knowledge grounding meaning that generated proof contains the same references as those found in the ground-truth proof. To measure this, we use precision, recall, and Fl-score between the reference sets contained in the generated and ground-truth proofs; i.e. m({fi,... g {ri...., ri. H), where m(-) is precision, recall, or FI. We also use Knowledge Token-Fl (kF1) (158). ), the overlap of the generated proof's tokens with tokens contained in the references mentioned in the ground- -tuth proof.
5 Experiments
We use the training and dev splits of NATURALPROOFS GEN during fine-tuning, and the core evaluation sets consisting of 100 theorems from the validation set and 100 from the test set for evaluation (see $ These theorems were selected by the authors such that by looking the theorem title each author could recall its content and sketch a proof. While this may shift the evaluation towards an easier slice of the dataset, it was necessary make human evaluation at meaningful scale feasible. We also use the core sets for explorations and ablations.
We finetune three GPT-3 5 (Curie) models, using the OpenAl API (see Appendix E for details):
5

---

Reasoning Ems (L)
Lexical Err (4)
Per-Step (t)
Full Proof (t)
Ref.
Equ.
Other
Lang.
Sym.
Useful
Correct
Useful
Correct
GPT-3
30.92
32.54
40.15
5.61
5.24
25.69
28.18
20%
13%
PATURAL.RRVERR:III
23.52
37.55
23.66
4.54
6.19
41.54
33.56
32%
24%
NATURALPROVER
25.84
35.93
25.23
8.41
5.35
39.60
26.30
35%
24%
NATURALPROVER 23.61
28.54
18.45
5.58
3.65
46,57
35,41
45% %
32%
Next-step (NATURALPROVeR)
19.70
26.32
19.10
8.57
5.86
51.43
42.86
Table 2:
Human evaluation results the core test set for full proof generation and next-step suggestion (bottom row). All models are fine-tuned on NATURAL PROOFS-GEN.. Knowledge - either retrieved or human provided and constrained decoding improve proof generation, with 46% of proof steps rated as useful and 35% correct according to university-level mathematics students.
Baseline GPT-3. We finetune a baseline GPT-3 model, po x), on theorem-proof examples y() from the training split. At test time, we condition the model test theorem.
2. PRUUTRALPROVEREEEEE
We finetune GPT-3 with retrieved references, ( F1,..... fo,..,, f-20)-
We use a pretrained joint retrieval model f(x + (ri,.... F(R)) from A51, which was trained to retrieve an input theorem's ground truth references. At test time, the model receives a theorem and the top-20 reference titles that are retrieved given the theorem.
3. NATURALPROVER We finetune GPT-3 with human-provided references, po rī, FR where (ri ..... FR,1 is the set of reference-title in the ground trothd-truth proof. We use reference-titee title conditioned examples (Eqn. and
(Eqn. on the training split/reference set. At test time, the model receives a theorem and reference titles from its ground-truth proof.
For next-step suggestion we use the human-provided knowledge model NATURALPROVERR
Decoding, For full proof generation, we use stepwise++ decoding with the provided knowledge model. which refer to
and otherwise greedy decoding. We do not use stepwise constrained decoding with retrieved references since these references introduce noisy constraints, nor for next-step prediction since the algorithm is designed for multi-step proofs. See $ for additional experimental details.
Human evaluation setup. To evaluate the proofs generated by NATURALPROVER we recruited 15 students from the Department of Mathematics and Applied Mathematics at the University of Washington, including undergraduate, masters, and Ph.D. students. The annotators were trained on how to evaluate proof correctness and compensated according to IRB requirements; see F22 For each task, we first reveal the theorem and its gold proof to the annotator. If they cannot understand a theorem or its gold proof, they may skip evaluating it. Otherwise, they may proceed to see the model-generann proof, one step time, and annotate each step under the step-wise evaluation schema (outlined in $ After all the steps are shown and evaluated, for the full-proof generation task, the annotator is asked to annotate the entire proof under the overall evaluation schema.
5.1 Main Results
Our best method is capable of generating correct and useful proofs. According to human evaluation results Table 2). our best method is NATURAL and stepwise++ inference. 32% of the proofs generated by this method are rated as correct and 45% rated as useful correct and 47% useful. Taking more granular view, best method makes significantly less reference), equation, and other reasoning errors than other baselines. It makes very few language and symbolic errors, meaning it produces mostly complete, well-formatted mathematical statements, and defines and uses symbols accordingly. It mostly avoids hallucinating references or creating circular proofs. On the other hand, despite improving over the other methods, the model often struggles with correctly deploying and using references (23.6% reference error rate), as well as symbolic computations (28.5% equation
with human-provided references
aid for human proof writers. On the per-step level, 35% of the proof steps
rate), especially multi-step derivations (21.9% invalid).
What do the model's correct proofs look like? We inspected the proofs labeled as correct and found three main categories: (1) reference-ussembbly proofs whose correctness is heavily determined by reference statements (e.g. Table 18 Table 20); (2) template-alaptatien
proofs in which the model adapts the structure and content of training theorem's 's proof to prove the unseen evaluation theorem

---

Theorem
Singleton Set is not Dense-in-itellf (5, T) topological space.
Singletion Point is Isolated
Let T (S, 7) be lopological space.
Let S.
Let E
Then the singleton set {x) is not dense in itself.
Then is isolated point of
GPT-3
Let
the singleton set {z).
From Clopon Points in Topological Space we have that
x
but not necessarly an isolated point of
{a} is open in T.
Dense in in-itelf
From Point is Open ifT it not Dense in-itself, it follows
Let S, be topological space.
that (a) is dense-in-ieee
H C
Then If is iinse-in-itself iff it contains
NATURALPROVERR_. From Singleton Point is Isolated, {x) an isolated point.
no isolated points.
Hence the result definition dense-in-itself.
Table 3: GPT-3 hallucinates references, while the -grouuddgggrouddddd NATURAL with
constrained decoding correctly uses references, resulting a correct and useful proof.
(3) complex proofs that not fully determined by reference statements and differ significantly from training proof's (c.g. Figure I Table 3). In terms of techniques, our method demonstrates some ability to produce direct proofs Table 19), proofs by cases Table 22). proof's by
(e.g- Table 21
Table 22);
induction Table 23), utilize references (Table 20) and do symbolic computations TTble 2
Vanilla fine-tuned GPT-3 struggles with proof generation. The vanilla fine-tuned GPT-3 model yielded fewer useful and correct proofs, with more reference- based and other reasoning errors than all three knowledge-groundd groundedd settings. The model showed severe reference hallucination (18%) and repetition (23%). It also makes significantly more reasoning errors related to reference usage. Language and symbolic error rates roughly stay the same. Overall, naively fine-tuning GPT-3 theorem-proof examples alone is suboptimal for proof generation.
fluman-provided knowledge improves proof generation. Grounding the generations with human- provided references significantly raises correctness and usefulness of the proofs in both full- proof and per-step evaluation. most substantially reduces reference errors especially invalid deployments and hallucinated references. For example, Table 3 shows the model grounding a proof with information from the theorem Singleton Point is Isolated and the definition of Dense-in-itsed in contrast to the vanilla GPT-3 model which hallucinates references.
Retrieved knowledge also improves proof generation. Retrieved knowledge also turns out to be very helpful, and even comparable to numan-provied knowledge in some metrics. Although the retrieval model far from perfect, the proof generation model is capable of narrowing down the retrieved reference titles provided in its context, assembling proofs that are useful and correct more often than the no-knowledge model. Qualitatively, we found examples where grounding in retrieved references eliminates repetition, enables multi-step derivations justified by references (Table 21). and assembles references into a correct proof Taale 20p. This paves a promising path towards fully automated mathematical proof generation in natural mathematical language.
Constrained decoding further improves proof gen- eration. Table 4 confirms that stepwisc++ decoding approximates the constrained objective (Eqn. bet- ter than greedy search, yielding proofs with lower perplexity and higher constraint satisfaction (Ref-F1). This translates to generations that are correct and useful more often according to the annotators. Intu- itively, the constraints encourage the model to include references that help prove the claim (e.g. Table 18).
In-context Stepwise++ PPL (L) Ref-FI (1)
X
x
1.0639
26.33
x
/
1.0549
30.07
X
1.0644
89.43
/
1.0549
94.25
Table 4: Stepwise++ decoding approximates the constrained objective better than greedy decoding, resulting in both lower perplexity and better reference coverage, regardless of whether knowledge is provided in-context.
Next-step suggestion. The next-step suggestion task characterizes a model's performance on mak- ing single proof step given a correct proof-so-far In Table 2 we use the provided- provided-knowledge knowledge model with greedy decoding for next-step sugges- tion, and find that reasoning errors decrease and per-step usefulness and correctness improve compared to the full proof setting, with 51% of the proof steps rated as useful and 43% cor- rect. Although we used a single suggestion in our human evaluation study, in Table 5 we simulate a user choosing from among multiple suggestions by sampling 10 next-steps from model and computing automatic metries the sample with the best sum of metrics. Us-
7

---

Lexical
Grounding
GLEU
Token F1
kF1
Ref-P
Ref-R
Ref-F1
Halluc (4)
GPT-3
24.40
49.96
49.30
29.93
24.73
23.69
17.92
NATURAL PROVERRRRVEEEEEEE RETRIEVE
26.58
53.02
55.88
38.17
28.48
27.10
2.25
NATURALPROVER
35.27
66.00
90.07
93.05
86.05
87.08
1.60
NATURALPROVER
34.49
65.61
96.39
94.66
95.00
93.92
1.71
Correctness [full]
0.93
0.91
0.86
0.83
0.85
0:85
0:94
Usefulness [ful]]
0.90
0.87
0.82
0.78
0.80
0.80
0:97
human metric
Correctnezs [steo]
0.81
0.80
0.69
0.73
0.72
0.97
Usefulness [steo]
0.65
0.61
0.53
0.47
0.52
0.51
0.98
Reasoning Erross: Ref.
0.71
0.
0.52
0.48
0.50
0.50
0.95
Reasoning Erross: Eqn.
0.70
0.74
0.75
0.69
0.74
0.73
0.78
Reasoning Errors: Other
0.65
0.61
0.53
0.47
0.52
0.51
0:98
Lenguage Errors
0.99
1.00
0.99
0.91
0:99
0.99
0.73
Symbolic Errors
-0.72
-0.80
-0.88
0.89
00. 09
-0.
00.88
00.21
Table Automatic metrics on the core test set for full-proof generation, and correlation between human metrics and automatic metrics on the core validation set.
ing 10 samples instead of greedily decoding single sequence substantially improves each metric, suggesting that utility might be increased further by presenting multiple suggestions.
How good are Automatic Metries? We study how well the automatic lexical and grounding metrics introduced in p$4 can reflect the real quality of proofs, guide for using them a proxy evaluation protocol for AXTURALPROOFS-A compute the Pearson correlation coefficient between each pair of human and automatic metrics, with data from the four exper- iment settings for full-proof generation. Results are shown in the lower part of Table 6) with error metrics negated, meaning positive correlation is desired.
Decoding
GLEU
Ref-FI
Greedy
47.87
65.50
We
Temp (t= 6)
60.60
84.44
Temp (I=.8)
61.89
86.74 76.74
Temp (t=1.0)
62.12
86.87
Table 5: Next-step suggestion: Sampling 10 suggestions improves over a single greedy suggestion.
The lexical and grounding metrics positively correlate with full proof correctness and usefulness (2 0.8). At the step-level,
the metrics show (i) high correlation with step-level correctness and language errors; (ūi) varied, but positive, correlations with aggregate reasoning errors; (iii) negative correlation with symbolic errors (though symbolic errors are relatively low all models). The results suggest that optimizing for automatic metrics may be viable strategy, albeit without guarantees on how finer-grained reasoning aspects vary across proofs.
5.2 Ablations and error analysis.
Reference reconstruction. We fine-tune an additional GPT-3 model that is provided with in-context reference titles, but without reference reconstruction. As seen TTbll 7 refer- reconstruction improves content and reference usage.
Recon. Gleu Ref-FI Hallue.
33.03
82.85
3.32
35.93
84.15
2.68
Constrained decoding. First. Table coompares the step-level search in stepwise++ with searching at the full-proof level through sampling multiple proofs and selecting best with the NATURAL.PRVV
Table 7: Effect of reference re- construction in NATURALPROVER (greedy decoding, full validation set).
value function (rerank (n)). Rerank- ing 60 samples matches the cost of stepwisc++ in terms number of decoded tokens. Full-proof reranking yields the best Gleu, though with lower reference-Fl. Second, Table 8 shows that the expansion and selection mechanisms together result the best reference matching, while holding Gleu at similar level. Finally, Table 13 shows that both terms in the NATURAL value function ('Veosstriits + (1 aLLLMM are needed: increasing the constraint weight increases enference-matching with tradeoff in Gleu at high values.
Language model comparison. Table 10 varies language model used to parameterize NATU- R RAL.PROVE... The content and reference usage metrics improve with larger models. Separately, we find that increasing inference-time compute closes the gap reference-matching between GPT-2 and the larger GPT-3 model (Table II): sampling 10 full-proofs from GPT-2 and selecting the best

---

Expand Select
GLEU
Ref-F1
Decoding
Gleu
Ref-FI
X
40.62 (884
91.78 (.49)
Greedy
41.12 (-)
89.30 (-)
x
41.12 (.58)
92.61 (.63)
Rerank (10) 43.88 (.29)
91.72 (.28)
x
/
39.14 (.55)
93.11 (.34)
Rerank (60)
42.23 (.80)
93.16 (.27)
/
V
40.11 (1.55)
94.13 (.45)
Stepwise++ 40.11 (1.55)
94.13 (.45)
Table 8: Ablation of the stepwise++ expansion Table 9: Stepwise versus full-proof search. Mcan and selection mechanisms. Mean (std) over 3 (std) over runs on the core dev set. runs shown the core dev set.
using the NATURALPROVER value function achieves the same reference-Fl GPT-3 with single greedily-decoded proof. However, Gleu remains much higher with the larger GPT-3 model.
Challenge: Reasoning with references. Although reference reasoning errors were decreased through knowledge-groundingg and constrained decoding. on 23.6% of test steps (27% dev), with 15% of steps containing invalid deployments and 10% invalid justifications. For next-step prediction, the reference error rate remains nontrivial (19.7% test, 13% dev). meaning that the model can struggle to correctly deploy references or use them justification even in the absence of compounding errors from previous steps. Table 15 shows example invalid deployments and justifications; the emrrrs are at times subtle, and require reasoning about the theorem statement, reference content, and proof context.
still commits a reference error
Challenge: Equations and derivations. NATURAL commits an equation-related er- ror on 28.5% of test steps (22.8% dev), including invalid equations (9.4%) and derivations (21.9%). Though an improvement over vanilla fine-tuned GPT-3 (32.5%), the errors occur fre- quently and remain high for next-step prediction (26%). Table 17 shows representative errors, which range from simple "commonsense" mistakes (e.g. 24 = 2a) to making invalid steps with false justification within more sophisticated multi-step proofs. Investigating the role of pretraining, in-context techniques 31, and autoformalization
39 is interesting future work.
Challenge: Proof length. Although NATURAL- PROVER demonstrates some ability to write long proofs (e.g. Table 23). the 42% next-step correctness suggests that compounding errors are likely as proof length increases. Indeed, our best model's 's full-proof correctness 48% on 1-4 step proofs (n = 102), decreasing to 15.6% on proofs with 5 more steps (n = 64), with lower per-step usefulness and cor- rectness at later steps (Figure 2}. Our findings are analogous to recent work on language modeling for formal theorem proving [32], where current models are typically limited to chaining or 3 non-trivial steps of mathematical reasoning.
corectt
(teelsteep)
(ncod stesl
Step
Figure 2: Per-step correctness and usefulness as function of step number, for full-proof generation with NATURAI.PROVER and next-step prediction with
5.3
Additional discussion
Finally, provide higher-level comments on future work related to interactive systems, mathematical assistants, and generating proofs in informal versus formal mathematics.
Interactive & improving systems. Currently, our tasks are at two ends of a spectrum: in next-step generation, we always assume previous steps are from human--ritten proof, while in full proof generation they are always from the model. Our results with multiple next-step suggestions suggest that users might find some suggestion among the multiple returned useful at a high rate, pointing to PROVER, in which human picks the next step
middle ground: a semman-n--the-lor from among the returned suggestions, or writes one based on the suggestions. The selected or written next-step could then be used as feedback to improve the system, enabling iteratively improving NATURALPRovE This notion of a continuously improving, teachable system an emerging (e.g. ( and interesting future direction.
Assistants for mathematics. Our tasks were motivated by an assistant that helps a user write a proof, either from scratch or when stuck part of the way through. Our study here focuses capability:

---

investigating whether neural language models are capable of performing the underlying mathematics that would be expected from such an assistant. A further challenge is to also ensure reliability user should have confidence that the model is not deceptive or incorrect, and is robust to changes in domain, on nearby problems, and on alternative ways of expressing a problem. Even further, we would like flexibility human teachers can interact with student flexibly through dialogue, natural language, and diagrams, rather than the strict input-output format defined by a dataset. Our work provides an initial step towards this larger vision.
Informal and formalized mathematics. Our work investigates theorem proving entirely in natural mathematical language (i.e. 'informal' mathematics), as it reflects an interface that a student typically uses when working with mathematics. An alternative is proving theorems a formalized system, in which proof steps are expressed in programming language (e.g. Lean MT].. Operating purely in formalized system allows for verifying correctness unlike our setting which must be verified by human arguably at the cost of flexibility and interpretability, as the mathematics is no longer expressed natural language and must adhere constraints of the formal system. Investigating combinations of the two e.g. expressing theorem in natural language, receiving verified formal proof, then providing an interpretation in natural language presents a wide range of interesting directions for future work.
6 Related Work
Formalized mathematics with neural language models. A large portion of work on machine
learning for mathematics focuses on formalized mathematics. Language models have been used for
interactive theorem proving, including in GPT- B33 321. PACT [20. and in [4 In these settings
proof steps are expressed in a programming language (e.g. Lean II] and there is access to verifier,
which differs from our setting of theorem proving natural mathematical language.
Informal mathematics with neural language models. Previous work on theorem proving in
natural mathematical language focuses on retrieving relevant premises (e.g. theorems, definitions)
17 T8 45 21).
informal-to-formee translation [X], which differ from our setting of generating
next-steps or full proofs. Outside of theorem proving, various works use sequence models for problem
solving, including benchmarking language models on arithmetic 7
competition problems [2)
symbolic mathematics (25] 46]. augmenting LMs with verifiers ? or in-context rationales
44
for math word problems, or using language models for math-related program synthesis
and competitive programming (66] These settings focus on generating executable programs or
numerical answer, which differ from our theorem proving setting, where the goal is generate sound and convincing arguments on a range of topics in natural mathematical language.
Related areas in NLP. Systematic reasoning in natural language (outside math) has been studied with synthetic proofs 33 20 single-step deductions 4 entailment trees [. which differ from proving real-world mathematical theorems. Augmenting LMs with knowledge reduces hallucinations in dialogue (38) which has analogous step-wise structure, while 30) use references within long- form answers; these and related NL.P findings differ from improving the utility of mathematical proofs. Lexically-constrained decoding algorithms include variants of (token-level) beam search 28 27) which assume access to per-token logits, and gradient-based decoding [3]]; our segment-level decoding only assumes sampler that returns text and its bogobbbbbb,lity, making compatible with recent language model API interfaces (e.g. the GPT-3 API).
(e.g. M 23
7
Conclusion
We described NATURAL PROVER, khowledge-groundee language model that generates mathematical proofs by conditioning on background theorems and definitions, and optionally enforces their presence with constrained decoding. Our system improves the quality of next-step suggestions and generated proofs over tne-tuned GPT-3, demonstrating an ability to correctly prove theorems and provide useful suggestions to human proof writers.
10

---

Acknowledgments and Disclosure of Funding
This work was funded in part by the Natural Sciences and Engineering Research Council of Canada (NSERC) (funding reference number 401 401233309), DARPA MCS program through NTWC Pacific N660001-1-2-40333 and the Allen Institute for AL. We also thank Google Cloud Compute, as well as OpenAI.
The authors would like to thank Alisa Liu, Julian Michael, Yuren (Rock) Pang, and Kaiming Cheng for dogfooding and providing valuable feedback our human evaluation system. We would also like to thank James McGivern for developing an interactive demo for NaturalProverr.
References
[1] Peter Anderson, Basura Fernando, Mark Johnson, and Stephen Gould. Guided open vocabulary image captioning with constrained beam search. In Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing, pages 936 945, Copenhagen, Denmark, September 2017. Association for Computational Linguistics.
[2] Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang. Carrie Cai, Michael Terry, Quoe Le, and Charles Sutton. Program synthesis with large language models, 2021.
[3] Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, Russ Altman, Simran Arora, Sydney von Arx, Michael S. Bernstein, Jeannette Bohg, Antoine Bosselut, Emma Brunskill, Erik Brynjolfsson, S. Buch, Dallas Card, Rodrigo Castellon, Niladri S. Chatterji, Annie S. Chen, Kathleen Creel, Jared Davis, Dora Demszky, Chris Donahue, Moussa Doumbouya, Esin Durmus, Stefano Ermon, John Etchemendy, Kawin Ethayarajh, Li Fei-Fei, Chelsea Finn, Trevor Gale, Lauren E. Gillespic, Karan Goel, Noah D. Goodman, Shelby Grossman, Neel Guha, Tatsunori Hashimoto, Peter Henderson, John Hewitt, Daniel E. Ho, Jenny Hong, Kyle Hsu, Jing Huang, Thomas F. Icard, Saahil Jain, Dan Jurafsky, Pratyusha Kalluri, Siddharth Karamcheti, Geoff Keeling, Fereshte Khani, O. Khattab, Pang Wei Koh, Mark S. Krass, Ranjay Krishna, Rohith Kuditipudi, Ananya Kumar, Faisal Ladhak, Mina Lee, Tony Lee, Jure Leskovec, Isabelle Levent, Xiang Lisa Li, Xuechen Li, Tengyu Ma, Ali Malik, Christopher D. Manning, Suvir P. Mirchandani, Eric Mitchell, Zanele Munyikwa, Suraj Nair, Avanika Narayan, Deepak Narayanan, Benjamin Newman, Allen Nie, Juan Carlos Niebles, Hamed Nilforoshan, J. F. Nyarko, Giray Ogut, Laurel Orr, Isabel Papadimitriou, Joon Sung Park, Chris Piech, Eva Portelance, Christopher Potts, Aditi Raghunathan, Robert Reich, Hongyu Ren, Frieda Rong, Yusuf H. Roohani, Camilo Ruiz, Jack Ryan, Christopher R'e, Dorsa Sadigh, Shiori Sagawa, Keshav Santhanam, Andy Shih, Krishna Parasuram Srinivasan, Alex Tamkin, Rohan Taori, Armin W. Thomas, Florian Tramèr, Rose E. Wang, William Wang, Bohan Wu, Jiajun Wu, Yuhuai Wu, Sang Michael Xie, Michihiro Yasunaga, Jiaxuan You. Matei A. Zaharia, Michael Zhang, Tianyi Zhang, Xikun Zhang, Yuhui Zhang, Lucia Zheng, Kaitlyn Zhou, and Percy Liang. On the opportunities and risks of foundation models. ArXiv, 005/2108.07255 2021.
[4] Kaj Bostrom, Xinyu Zhao, Swarat Chaudhuri, and Greg Durrett. Flexible generation of natural language deductions. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 6266-6278, Online and Punta Cana, Dominican Republic, November 2021. Association for Computational Linguistics.
[5] Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Voss,, Gretchen Krueger, T. J. Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeff Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Rad- ford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. ArXiv, 1ttp20005.11665 2020.
[6] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et Evaluating large language models trained on code. arXiv preprint 237702107.03334, 2021.
11

---

[7] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jeny Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv: 10. 10.14680,, 2021.
[8] Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie, Hannah Smith, Leighanna Pi- patanangkura, and Peter Clark, Explaining answers with entailment trees. In Proceedings of the 202/ Conference on Empirical Methods in Natural Language Processing, pages 7358-7370, Online and Punta Cana, Dominican Republic, November 2021. Association for Computational Linguistics.
[9] Bhavana Dalvi, Oyvind Tafjord, and Peter Clark. Towards teachable reasoning systems. ArXiv, abs/2204. 13074, 2022.
[10] Davis and Hersh. The mathematical experience. Birkhauser, 1981.
[11] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy Felty and Aart Middeldorp, editors, CADE, volume 9195 of Lecture Notes in Computer Science, pages 378 -888. Springer, 2015.
[12] Michael de Villiers. The role and function of proof in Mathematics. Pythagoras, 1990.
[13] Emily Dinan, Stephen Roller, Kurt Shuster, Angela Fan, Michael Auli, and Jason Weston. Wizard of wikipedia: Knowledge-powee conversational agents. In International Conference on Learning Representations, 2019.
[14] Iddo Drori, Sarah Zhang, Reece Shuttleworth, Leonard Tang, Albert Lu, Elizabeth Ke, Kevin Liu, Linda Chen, Sunny Tran, Newman Cheng, Roman Wang, Nikhil Singh, Taylor L. Patti, Jayson Lynch, Avi Shporer, Nakul Verma, Eugene Wu, and Gilbert Strang. A neural network solves, explains, and generates university math problems by program synthesis and few-shot learning at human level, 2021.
[15] Barbara S. Edwards and Michael Ward. Surprises from mathematics education research: Student (mis)use of mathematical definitions. American Mathematical Monthly, 2004.
[16] Erik G. Jensen. Thinking Like a Lawyer. In Thinking Like a Lawyer, chapter 2, "Forms. Stanford Law School, 2014.
[17] Deborah Ferreira and André Freitas. Natural language premise selection: Finding support- ing statements for mathematical text. In Proceedings of the 12th Language Resources and Evaluation Conference, pages 2175-2182, Marseille, France, May 2020. European Language Resources Association.
[18] Deborah Ferreira and André Freitas. Premise selection in natural language mathematical texts. In Proceedings of the 58th Amnual Meeting of the Association for Computational Linguistics, pages 7365-7374, Online, July 2020. Association for Computational Linguistics.
[19] Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The Pile: An 800gb dataset of diverse text for language modeling. arXiv preprint arXiv:2101.0000 2020.
[20] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for thcorem proving with language models, 2021.
[21] Jesse Michael Han, Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford. Contrastive finetuning of generative language models for informal premise selection. AITP, 2021.
[22] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset, 2021.
12

---

[23] Chris Hokamp and Qun Liu. Lexically constrained decoding for sequence generation using grid beam search. In Proceedings of the 55th Annual Meeting of the Association for Computa- lional Linguisties Vooluee 1: Long Papers), pages 1535-1546, Vancouver, Canada, July 2017. Association for Computational Linguistics.
[24] David H Kaye. Penn State Law eLibrary Journal Articles Faculty Works 1992, Proof in Law and Science. Jurimetrics J, 32, 1992.
[25] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In Interna- tional Conference on Learning Representations, 2020.
[26] Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, et al. Competition-level code generation with alphacode. arXiv preprint arXiv:2203.0781 2022.
[27] Ximing Lu, Sean Welleck, Peter West, Liwei Jiang, Jungo Kasai, Daniel Khashabi, Ronan Le Bras, Lianhui Qin, Youngjae Yu, Rowan Zellers, Noah A. Smith, and Yejin Choi. Neu- rologic a eseque decoding: Constrained text generation with lookahead heuristies. ArXiv, abs/21 12.0871, 2021.
[28] Ximing Lu, Peter West, Rowan Zellers, Ronan Le Bras, Chandra Bhagavatula, and Yejin Choi. Neurologie decoding: (un)supervised neural text generation with predicate logic constraints. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 4288 4299, Online, June 2021. Association for Computational Linguistics.
[29] Andrew Mutton, Mark Dras, Stephen Wan, and Robert Dale. Gleu: Automatic evaluation of sentence-level fluency. In Proceedings of the 45th Annual Meeting of the Association of Computational Linguistics, pages 344-351, 2007.
[30] Reiichiro Nakano, Jacob Hilton, S. Arun Balaji, Jeff Wu, Long Ouyang. Christina Kim, Christo- pher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, Xu Jiang, Karl Cobbe, Tyna Eloundou, Gretchen Krueger, Kevin Button, Matthew Knight, Benjamin Chess, and John Schulman. Webgpt: Browser-assisted question-answering with human feedback. ArXiv, abs/2112.00 12.0911,, 2021.
[31] Maxwell Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, Charles Sutton, and Augustus Odena. Show your work: Scratchpads for intermediate computation with language models. ArXiv, abs/2112.001 14, 2021.
[32] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
[33] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
[34] Lianhui Qin, Sean Welleck, Daniel Khashabi, and Yejin Choi. Cold decoding: Energy-based constrained text generation with langevin dynamics. ArXiv, abs/2202.11705. 2022.
[35] Alec Radford, Jeff Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. 2019.
[36] Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, and Mohit Bansal. PRover: Proof generation for interpretable reasoning over rules. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 122-136, Online, November 2020. Association for Computational Linguistics.
[37] David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In International Conference on Learning Representations, 2019.
13

---

[38] Kurt Shuster. Spencer Poff, Moya Chen, Douwe Kiela, and Jason Weston. Retrieval augmenta- tion reduces hallucination conversation. In Findings of the Association for Computational Linguistics: EMNLP 2021, pages 3784-3803, Punta Cana, Dominican Republic, November 2021. Association for Computational Linguistics.
[39] Christian Szegedy, editor. A Promising Path Towards Autoformalization and General Artificial Intelligence, 2020.
[40] Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computa- tional Lingwistics: ACL-IJCNLP 2021, pages 3621-3634, Online, August 2021. Association for Computational Linguistics.
[41] Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Interna- tional Conference on Intelligent Computer Mathematics, pages 315-32 323.. Springer, 2020.
[42] James F. Voss and Mary L.. Means. Learning reason via instruction in argumentation. Learning and Instruction, 1991.
[43] Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation autoformalization mathematics Mizar. CPP 2020 Proceedings of the 9th ACM SIGPLAN International Conference Certified Programs and Proofs, located with POPL 2020, 2020.
[44] Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed Chi, Quoe Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models, 2022.
[45] Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fitth Confer- ence on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1),
2021.
[46] Sean Welleck, Peter West, Jize Cao, and Yejin Choi. Symbolic brittleness in sequence models: on systematic generalization in symbolic mathematics. AAAI, http/2109.199900 2022.
14

---

Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's
contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] See $5.2
(c) Did you discuss any potential negative societal impacts of your work? [Yes] See
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them?
[Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [N/A]
(b) Did you include complete proofs of all theoretical results? [N/A]
3. If you ran experiments...
(a) Did you include the code, data, and instructions needed to reproduce the main experimental results (either in the supplemental material as URL)? [Yes] We will release our code in the supplemental material.
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes] See and $
(c) Did you report error bars (e.g., with respect to the random seed after running experiments multiple times)? [Yes]
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, or cloud provider)? [Yes] See
4. you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes]
(b) Did you mention the license of the assets? [Yes] See C
(c) Did you include any new assets either in the supplemental material or as a URL? [Yes] See
and supplementary materials.
(d) Did you discuss whether and how consent was obtained from people whose data you're
using/curating? [Yes] See FF2
(e) Did you discuss whether the data you using/curating contains personally identifiable information or offensive content? [Yes] See F22
you used crowdsourcing or conducted research with human subjects...
(a) Did you include the full text of instructions given participants and screenshots, if applica-
ble? [Yes] See F.2 and supplementary materials.
(b) Did you describe any potential participant risks, with links to Institutional Review Board
(IRB) approvals, if applicable? [Yes] See
FF2
(C) Did you include the estimated hourly wage paid to participants and the total amount spent
participant compensation? [Yes] See
F2
15


Reviews:
[{"review_id": "P2TgEOoJAta", "reviewer": "Reviewer_PnA9", "summary": "This paper presents, NaturalProver, a machine learning-based proof solver that leverages the augments large language models (e.g., GPT-3) with symbolic information so they can be utilized for more than just natural language processing. The authors demonstrate NaturalProver’s advances in two fundamental dimensions: (1) full mathematical proof generation and (2) next-step proof generation. While the full proof generation component is limited to only a small number of steps for proof generation (e.g., 5-6 steps) the next-step proof assistance, in theory, could potentially be applied to any proof, irrespective of the total proof step count. The authors claim the next-step assistant is correct (and useful) up to 40% of the time.\n\nThe authors compare NaturalProver against a GPT-3 baseline.\n", "questions": "Can the authors please try to explain the ways they prevented the weaknesses I have listed above (pasted below) in the evaluation method for the paper?\n\nBecause humans were used to evaluate the correctness of the system, it seems as though there may have been some bias in the results for numerous reasons. First, if the students were aware which proofs were generated by the research team’s system, they may have intentionally (or unintentionally) scored such proofs higher. Second, because the graders are human – and of varying degrees of mathematical competence – there is some chance the grading for some proofs were incorrect. Third, according to the authors, the students were first shown a “golden proof” which is used as a key for the synthesized proofs. However, there can exist many different correct proofs for mathematical problems. Because of this, it could be the case that some of the generated proofs are correct but were flagged is incorrect because they deviated from the “golden proof” steps or solution.\n", "limitations": "I'm not aware of any potential negative societal impact this research could incur.\n", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengthens:\n\nThis paper is well-written and well-motivated.\n\nThe research topic is both timely (e.g., leveraging large language models for more than just natural language processing) and valuable (e.g., assisting formal solvers in ways that may improve some of the intractable computational bounds that have historically limited their capabilities to only relatively small proofs to do exponential state space explosion).\n\nThe two-pronged approach of both full proof and, perhaps more interestingly, next-step proof assistance, is compelling and has a reasonable amount of immediate value both in academia and industry (in my opinion).\n\nAugmenting large language models to handle mathematical proof texts for the authors two-pronged approach is, to my knowledge, novel and clever. Additionally, the fact that the authors added LaTex support for mathematical proofs seems to imply it may have immediate value to other mathematicians in the research community, many of which write their mathematical proofs entirely in LaTex (myself included).\n\nWeaknesses:\n\nWhile GPT-3 is obviously one of the most well-known and effective LLMs to date, it would have been nice to see a comparison to other language models.\n\nBecause humans were used to evaluate the correctness of the system, it seems as though there may have been some bias in the results for numerous reasons. First, if the students were aware which proofs were generated by the research team’s system, they may have intentionally (or unintentionally) scored such proofs higher. Second, because the graders are human – and of varying degrees of mathematical competence – there is some chance the grading for some proofs were incorrect. Third, according to the authors, the students were first shown a “golden proof” which is used as a key for the synthesized proofs. However, there can exist many different correct proofs for mathematical problems. Because of this, it could be the case that some of the generated proofs are correct but were flagged is incorrect because they deviated from the “golden proof” steps or solution.\n\nMinor nits:\n\nSome of the written language in the paper seems a bit misplaced and perhaps in appropriate for a tier-1 research venue. This should hopefully be easy to correct, but I felt it worthwhile to mention. In the abstract there is mention that the LLMs generate “proofs riddled with hallucinations” – I have no idea what this means, but it seems like an inappropriate and unprofessional classification of results in a scientific research paper. In Section 5 under “human evaluation setup” the authors claim that “The human annotators were trained and compensated accordingly.” I have no idea what “compensated accordingly” means nor how to evaluate the accuracy of such a claim. Best to simply eliminate it entirely. I suspect it is fine to say that “students were trained on how to evaluate proof correctness.”\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "OrBdMHrkcNZ", "reviewer": "Reviewer_YcPJ", "summary": "This paper explores the prospect of theorem proving in natural mathematical language using large language models (LLMs). Two representative tasks are considered: generating the next step in a partial proof, and generating full proofs given only the statement of a theorem. A dataset for these tasks (based on the existing *NaturalProofs* benchmark) is contributed.\n\nUnfortunately, naive attempts to fine-tune GPT-3 on these tasks are shown to fail -- generated proofs often contain \"hallucinated\" references or logical errors. To address this, the work proposes \"NaturalProver\" to enforce the inclusion of certain background references in the output. Empirically, NaturalProver is shown to outperform GPT-3 on a number of metrics, including usefulness and correctness (as determined by human evaluators). \n", "questions": "1. Would a version of constrained decoding but with soft (rather than hard) constraints be well-motivated? To me, it seems like the stepwise beam search can almost be applied as-is to this other setting (or if not, please correct me). \n\n2. Is there a way to change NaturalProver to provide a measure of confidence in the correctness of the proof? This is arguably a key advantage of formal proof environments that's lost when dealing with natural language proofs. ", "limitations": "Yes, the limitations and societal impacts were addressed. ", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 4, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Originality**: Recent research explores theorem proving with inputs in the form of natural mathematical language, including the paper that proposed the NaturalProofs dataset [1]. As the authors note, these works often focus on auxiliary tasks, such as reference retrieval or translation to a formal mathematical representation. This work, on the other hand, considers the ambitious (but important) task of generating proofs and proof steps end-to-end, *from* natural math language *to* natural math language. This is a novel problem setting for theorem proving, to my knowledge. \n\n**Quality**: \n\n[Method]\nThe proposed method motivates the separation of the problem into two parts: reference retrieval (either by a neural network, or a human) followed by proof generation, conditioned upon these references. This is well-justified, especially given how GPT-3 is shown to fail on the end-to-end task. \n\nOne assumption that I did not agree with was that the relevant references would always appear in the final proof. This assumption holds in the experiments when the ground-truth set of references can be provided, but is too strong for practical uses. For unclear reasons, the proposed approach is not evaluated with references retrieved by a neural network. (Please also see question 1 below). \n\n[Experiments]\nThe various approaches are evaluated by human annotators on criteria that would otherwise be difficult to objectively measure. Automated metrics are proposed which correlate well with these criteria (with one exception). **I have a couple of concerns, which if addressed well would raise my score.**\n\n- GPT-3 with beam search decoding should be a baseline to fairly compare against NaturalProver++.\n- Error bars are missing on the main results, making it difficult to evaluate their significance. \n\n**Clarity**:\nThe paper is very well-written and clear. One part I could not understand was the meaning of the \"In-context\" column in Table 4. Does \"not in-context\" mean no references were conditioned upon, similar to the vanilla GPT-3 baseline? \n\n**Significance**:\nEnd-to-end theorem proving in natural mathematical language is a highly significant problem. This paper presents many interesting and useful insights on the problem, including why naive applications of LLMs fail and challenges for the future. One concern that may discourage future work is the lack of objective measures of success, but this work also takes steps to address this by proposing automated metrics of proof quality. One limitation to the main contributed approach (the one that uses constrained decoding) is that it was only shown to succeed when provided with ground-truth references. \n\n[1]: Welleck, Sean, et al. \"NaturalProofs: Mathematical Theorem Proving in Natural Language.\" Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1). 2021. ", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "8doA8mPi-jj", "reviewer": "Reviewer_Cdcz", "summary": "The authors use the NaturalProofs-Gen dataset to fine-tune GPT3 using two new loss functions: proof generation using in-context references and reference reconstruction. Additionally, they perform constrained decoding by adding lexical constraints to encourage generations that contain the input references. They evaluate the system on multiple metrics like the usefulness and correctness of the proof steps. Lastly, they compare the model's errors by human evaluation on sampled subsets of the eval dataset.", "questions": "* What is the order of the training data shown to GPT3 during fine-tuning - between in-context and reference reconstruction? Is it just randomly sampled or do you first show some reference reconstruction and then an in-context example that uses the previously shown references?", "limitations": "The authors clearly discuss the main limitations of the work, along with a comprehensive error analysis", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n* Overall, the approach is very nicely presented and easy to follow through\n* The experiments and ablations are comprehensive and well presented\n* Error analysis of the model is pretty detailed and well-categorized. This will help future research in this area to solve these challenges.\n\nWeakness:\n* Please consider adding some details about the specific GPT-3 model being used here (curie) in the appendix. At the very least, cite the related papers/websites when describing baselines around lines 190-199.\n* It'd help to have some examples in the main text about the difference between using stepwise and stepwise++ for decoding. That would make these sections more accessible to new readers.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept