IsarStep: a Benchmark for High-level Mathematical Reasoning

By Wenda Li, Lei Yu, Yuhuai Wu, Lawrence Charles Paulson. 2021

72 citations recorded by the source corpus.

Subfields: Prompting & Reasoning, Evaluation & Benchmarks, Program Analysis & Verification, Automated Theorem Proving & Formal Methods

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Prompting & Reasoning

In Evaluation & Benchmarks

In Program Analysis & Verification

In Automated Theorem Proving & Formal Methods

Citations in the corpus

Formal Mathematics Statement Curriculum Learning (2022, methodology): “We depart from Polu & Sutskever (2020) and use a proofsize objective to guide our proof searches, which consists in generating one token that represents a proof size estimate bucket for the current goal (Lean tactic state): DECL”
Towards mental time travel: a hierarchical memory for reinforcement learning agents (2021, methodology): “Other works have used a hierarchy of transformers with different timescales for supervised tasks [33, 63, 60, 31], for example encoding sentences with one transformer, and then using these embeddings as higher-level tokens.”
Teaching Algorithmic Reasoning via In-context Learning (2022, background): “In addition to this class of benchmarks, formal mathematics in the form of theorem-proofs (Rabe et al., 2020; Li et al., 2020; Polu and Sutskever, 2020; Welleck et al., 2021; Jiang et al., 2022; Wu et al., 2022) has been considered extensively.”
NaturalProofs: Mathematical Theorem Proving in Natural Language (2021, methodology): “others use the Coq [19, 48], Metamath [44, 42, 30], Isabelle [24], or Lean [14, 49] environments.”
LILA: A Unified Benchmark for Mathematical Reasoning (2022, background): “A separate line of work in mathematical reasoning includes datasets testing mathematical theorem proving (e.g., Li et al., 2021; Wu et al., 2021; Welleck et al., 2021; Zheng et al., 2021; Han et al., 2021).”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “Existing tools and datasets can be divided by proof assistants: Coq has GamePad [51], CoqGym [9], and PRISM [52]; Isabelle has IsarStep [53] and PISA [15]; HOL Light has HOList [54] and HoLStep [55], and Lean has LeanStep [16] and lean-gym [19].”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, background): “While there exist environments and datasets for other formal mathematics libraries (Kaliszyk et al., 2017; Li et al., 2021; Huang et al., 2019; Kaliszyk & Urban, 2015a), L EAN S TEP is the ﬁrst and only tactic proof dataset for the Lean theorem prover.”
Symbolic Behaviour in Artificial Intelligence (2021, background): “Indeed, deep learning models are increasingly succeeding at difficult mathematical reasoning tasks like identifying the theorem needed to complete a proof [81], or solving difficult symbolic integration [5], without GOFAI or neuro-symbolic methods.”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, methodology): “We demonstrate that LIME pretrained models provide significant gains across four large mathematical reasoning benchmarks: IsarStep (Li et al., 2021), HOList Skip-tree (Rabe et al., 2021), MetaMathStep (Polu & Sutskever, 2020), and LeanStep (de Moura et al., 2015).”
Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning (2021, background): “IsarStep [Li et al., 2021] is a mathematical reasoning benchmark.”
Memorizing Transformers (2022, background): “…in natural language processing (Devlin et al., 2019; Brown et al., 2020), mathematical reasoning (Polu & Sutskever, 2020; Wang et al., 2020a; Rabe et al., 2021; Li et al., 2021; Hahn et al., 2021; Cobbe et al., 2021), and program synthesis (Austin et al., 2021; Chen et al., 2021; Li et al., 2022).”