REVIEW 6 cited by
NaturalProofs: Mathematical Theorem Proving in Natural Language
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
NaturalProofs: Mathematical Theorem Proving in Natural Language
read the original abstract
Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization. Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.
Forward citations
Cited by 6 Pith papers
-
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
MiniF2F is a new cross-system benchmark containing 488 Olympiad-level mathematics problems formalized in Metamath, Lean, Isabelle, and HOL Light, together with baseline results from a GPT-3-based prover.
-
TheoremGraph: Bridging Formal and Informal Mathematics
TheoremGraph builds a unified statement-level dependency graph across informal arXiv math and formal Lean code via parsing, embeddings, and LLM validation, releasing the data and APIs for search and retrieval.
-
Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
Current embedding models fail to capture mathematical equivalence across lexical variants, but contrastive alignment of informal and formal statements improves retrieval on both equivalence and formalization tasks.
-
Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
Re²Math is a new benchmark that evaluates AI models on retrieving and verifying the applicability of theorems from math literature to advance steps in partial proofs, accepting any sufficient theorem while controlling...
-
Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
Embedding models fail to capture mathematical equivalence due to lexical bias, but contrastive training on informal-formal pairs improves performance on MELD and retrieval tasks.
-
Rethinking Wireless Communications through Formal Mathematical AI Reasoning
Proposes a three-layer framework using formal AI reasoning for verification, derivation, and discovery in wireless communications theory.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.