miniCTX: Neural Theorem Proving with (Long-)Contexts

Authors: jiewen  hu
thomas  zhu
sean  welleck
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-25 00:39:05

Abstract: Real-world formal theorem proving often depends on rich prior contexts, including definitions, lemmas, comments, file structure, and other information. We introduce $\texttt{miniCTX}$, which tests a model's ability to prove formal mathematical theorems that depend on new context not encountered in training. $\texttt{miniCTX}$ contains theorems sourced from real Lean projects and textbooks, each associated with a context that can span tens of thousands of tokens. Models are tasked with proving a theorem given access to code from the theorem's repository, which contains context that is needed for the proof. As a baseline for $\texttt{miniCTX}$, we tested fine-tuning and prompting methods that condition theorem proving on preceding context. Both approaches substantially outperform traditional methods that rely solely on state information. We found that this ability to utilize context is not captured by previous benchmarks such as $\texttt{miniF2F}$. Alongside $\texttt{miniCTX}$, we offer $\texttt{ntp-toolkit}$ for automatically extracting and annotating theorem proving data, making it easy to add new projects into $\texttt{miniCTX}$ to ensure that contexts are not seen during training. $\texttt{miniCTX}$ offers a challenging and realistic evaluation of neural theorem provers.

Main paper: 
 introduction: 
 Formal theorem proving in interactive theorem provers (ITPs) provides a testbed for evaluating the reasoning capabilities of large language models (LLMs). Theorem proving capabilities can then directly translate to automation for mathematicians, such as via tools that complete or formalize proofs [1] [2] [3] [4] . However, despite their promise, we see a gap between the evaluation of current language model-based provers and the complexity of real-world theorem proving.Our motivating observation is that theorems and proofs depend on various forms of context, such as newly-defined definitions and lemmas. For instance, to prove results about a square, one might first formalize a definition of a rectangle, prove some results about rectangles, then specialize them to a newly-defined square [5] (Figure 1 ). However, existing methods for training and evaluating LLM-based theorem provers often fail to incorporate the full range of contextual information available in real-world projects. For example, benchmarks often focus on proving standalone competition problems (e.g., miniF2F [6] ) or theorems from a library that the model has trained on (e.g., Mathlib [7, 8] ), and state-of-the-art LLM-based provers are trained to accept only a proof state as input, making them unaware of new theorems and definitions [9] [10] [11] . While some existing work, including premise selection techniques [12, 13, 8] and datasets like CoqGym [14] , have explored theorem proving based on information beyond the current state, they often focus on a subset of the available information. They primarily focus on providing relevant premises, such as lemmas, to assist in proof construction.Building on these foundations, we propose miniCTX: a benchmark that seeks to expand the scope of context used in theorem proving. We extend beyond traditional premise selection explored in prior benchmarks (e.g., [8, 14] ) by incorporating a more comprehensive set of contextual elements. This includes premises, but also prior proofs, comments, notation, and structural components like imports and declarations. By doing so, miniCTX aims to drive the development of methods that understand [15] Lean ✗ ✓ ✓ ✗ LeanDojo [8] Lean ✓ ✗ ✗ ✗ LeanStep [7] Lean ✓ ✗ ✓ ✗ CoqGym [14] Coq ✓ ✗ ✓ ✗ PISA [16] Isabelle✗ ✗ ✓ ✗ miniCTX (Ours) Lean ✓ ✓ ✓ ✓and work with context that occurs in complex, real-world theorem proving tasks. Additionally, considering the common use of pre-trained language models we mitigate potential data contamination by continually and automatically updating miniCTX with new Lean projects, so that evaluated theorems are not seen during training. Our key contributions are:miniCTX Benchmark: We introduce miniCTX, the first benchmark designed specifically to evaluate theorem proving in real-world settings where proofs depend on in-file definitions, lemmas, and context from formal projects. miniCTX presents a unique challenge by requiring models to reason over long contexts and handle dependencies that arise in real-world theorem proving tasks.Baseline Evaluations: We evaluate miniCTX on several existing baseline models, including different fine-tuning and prompting strategies, as well as premise selection. We also propose file-tuning, a strong baseline method for training models using full file contexts, where both the theorem statements and their surrounding context are provided during training. This approach establishes a robust baseline for future work on context-dependent theorem proving.Figure 1 : Many state of the art provers are trained on a static dataset of theorems and proofs, then evaluated on standalone problems such as competition problems (left). We argue that neural provers must also operate in the realistic context-dependent setting, in which results depend on working with new mathematical objects and their facts, notations, and the structural elements of the project (imports, variables, etc.) (right). 
theorem proving with context: 
 Formal theorem proving involves two stages: defining mathematical objects and facts relevant to the desired result, then stating and proving the result itself. Many current language model-based provers focus on the proving process and are trained on static datasets that only use a fixed set of definitions. As a result, they lack the ability to recognize new definitions or lemmas at test time (Figure 1 ).Context-dependent proving. We study context-dependent theorem proving, where the goal is for a model to generate proofs y for new theorems x, based on a context c that includes background information such as definitions, lemmas, or natural language comments. Formally, the problem isEQUATIONwhere (x, c) ∼ p denotes a (theorem, context) pair from a context distribution p, M is a model that produces a proof y, and v returns 1 if the proof is correct and 0 otherwise.We choose Lean [17] as the verifier v, because of the large body of recent theorems in Lean that can be used as evaluation data, and the abundance of proving methods in Lean that we use as baselines.We treat a Lean repository as the distribution p. Each context c is a subset of the repository, including new definitions, lemmas, notations, imports, and comments that are relevant to the theorem.3 miniCTX: a benchmark for theorem proving with contextWe develop miniCTX, a Lean 4 theorem proving benchmark of theorems that depend on newlydefined lemmas, definitions, and proofs from within a project. miniCTX is currently based on 376 theorems from four projects: (1) Prime Number Theorem (Prime) [18] , (2) Polynomial Freman-Ruzsa Conjecture (PFR) [19] , (3) an introductory text on theorem proving (HTPI) [20] , (4) recent results from the standard mathematical library (Mathlib) [21] (motivation and details in §D), ( 5) high energy physics formalization in HepLean (HEP) [22] , and (6) scientific computing formalizations (SciLean) [23] .Each theorem in miniCTX consists of the theorem statement, preceding file contents up to the theorem statement, and metadata, in JSON (see §E.1).1. Theorem statement, 2. Preceding file contents up to the theorem statement, 3. Metadata, including file name, commit and time which the theorem was added, position and length of the theorem and proof, and the number and types of premises used in the human-written proof.Using our benchmark, users can easily reconstruct the complete context for each theorem, including both in-file and cross-file context. The in-file context is provided directly by preceding file contents, while the cross-file context can be reconstructed using the metadata, which includes information on imported modules. We open-source the dataset and evaluation code. 
key features and challenges: 
 miniCTX introduces several key features that distinguish it from other theorem proving benchmarks, addressing challenges that have not been tackled by previous benchmarks:Real-world theorem proving. Unlike popular benchmarks (e.g., miniF2F [6] , ProofNet [15] , FIMO [24] ) that focus on isolated competition problems, real-world research-level theorem proving is heavily dependent on rich mathematical contexts. Therefore, miniCTX includes real-world, complex theorems from a variety of ongoing Lean projects, such as Prime Number Theorem (Prime) and Polynomial Freiman-Ruzsa Conjecture (PFR). They rigorously test a model's ability in real-world formalization projects. This diversity contrasts with the LeanDojo benchmark [8] , which focuses solely on Mathlib, enabling miniCTX to better test a model's generalization in different settings.Contextual evaluation. Proving a theorem often depends on new definitions, lemmas, or other contextual information, which a model may not have seen during training. miniCTX includes theorems along with this new context. During evaluation, the model is expected to leverage the provided new context to help prove the theorem.Beyond previous datasets like LeanDojo [8] and CoqGym [14] , which include relevant definitions and theorems, miniCTX includes additional useful contextual information that may make some theorems easier to prove compared to standalone theorems. For instance, Lean source code can have natural language comments that may help constrain the space of possible proofs. Moreover, some proofs within a file often have analogous patterns or structure, which may make subsequent theorems easier to prove (see §E.2). These additional forms of context occur in the real-world process of formalization, yet their use in neural theorem proving is underexplored.Automatically updating the benchmark. Most modern neural theorem provers use a large language model as a backbone. Therefore, it is crucial to ensure that evaluation content is not seen during (pre-)training, a problem not addressed by previous benchmarks. miniCTX's format is amenable to periodically updating the benchmark with new projects to ensure that proofs are not seen by language models trained prior to a particular date. Future periodic updates will be automatically extracted from new Lean projects and commits using NTP-TOOLKIT ( §??). See Figure 2 for an illustration. 4 Experiments 
baselines: 
 We evaluate several baselines on miniCTX, demonstrating the importance of context in real-world theorem proving. Our investigation reveals several open challenges that we discuss in §A. See §B for a detailed description of the motivation, baselines, data extraction, and evaluation setup, and §H for full results and more detailed analysis. The baselines are as follows:Prompting LLMs. We first test the ability of a state of the art API-based model, GPT-4o, to generate the complete proof in one pass (pass@1) given the theorem statement, with several few-shot examples provided for guidance. We additionally test whether adding context in the form of preceding file contents improves the proof rate of GPT-4o.State-tactic prompting. Another common approach to theorem proving using language models is to let the model generate a tactic given the current proof state [7] [8] [9] 25] . Therefore, we test the statetactic prompting setting, which prompts a model specialized for mathematical tasks, Llemma-7b [26] , to output a tactic given a proof state. At test time, the model generates one tactic at a time, and we use a best-first search to construct full proofs [7] [8] [9] 1] .State-tactic tuning. We follow this state-tactic framework and fine-tune a state-tactic tuned model from DeepSeek-Coder-1.3b [27] to input proof states and output tactics, trained on human-written tactics in Mathlib, the main mathematical library in Lean, extracted by NTP-TOOLKIT.File-tuning. We then test whether supplying context, in the form of preceding file contents, to the model improves performance. Similar to state-tactic tuning, we fine-tune a 1.3b model to generate a tactic based on (proof state, context) pairs, resulting in the file-tuned model.Premise selection. To better simulate a complete context and evaluate on project-level generalization, we apply premise selection to extract relevant premises from imported files within the same repository. We use the premise retriever provided by LeanDojo [8] to identify the top 20 most relevant definitions or lemmas from imported modules and append them to the in-file context.Context-dependent methods improve theorem proving. Table 2 shows baseline performances on miniCTX. We see a dramatic improvement for the file-tuned model (trained on full file context) over the state-tactic model (trained only on proof states) (35.94% vs. 19.53%). Similarly, providing the preceding file context, which includes definitions and lemmas, to GPT-4o results in dramatic improvement compared to using just the proof state (27.08% vs. 11.72%). Figure 4 shows the performance of state-tactic tuned model and file-tuned model on problems with in-file dependencies compared to those without. These findings highlight the importance of providing models with rich For each theorem in miniCTX, we record as metadata whether its human-written proof depends on other definitions or theorems in the same file ("in-file") or in other files ("cross-file"), and test the performance of baselines on each type.contextual information beyond the immediate proof state, also demonstrating that miniCTX is able to measure this ability of context-dependent proving.Premise selection improves performance on high cross-file dependency splits. The results in Table 2 indicate that premise selection has a mixed impact on model performance. For the GPT-4o, premise selection improves performance on high cross-file dependency splits, such as PFR, PFR cross , and SciLean. This suggests that premise selection helps capture the cross-file context, enabling GPT-4o to make better use of cross-file information. However, for the file-tuned model, premise selection does not consistently improve results, and even performs worse on the PFR cross split, which was designed to evaluate the effective use of cross-file premises. Also shown in Figure 4 , GPT-4o benefits significantly from premise selection on problems with high cross-file dependencies, but degrades in other cases. This suggests that the retrieved premises differ significantly from the in-file context. Therefore, developing methods that effectively support the integration of cross-file context (e.g., premise selection) alongside in-file context remains an interesting open research direction for improving performance on the miniCTX benchmark.Evaluation on miniF2F. We evaluate baselines on miniF2F, a standard benchmark based on competition problems that do not require context. The file-tuned model improves very little beyond the state-tactic model (33.61% vs. 32.79%), showing that the dramatic difference in context-dependent proving abilities seen on miniCTX cannot be captured by miniF2F.Additional analysis. Further analysis shows that file-tuning delivers greater gains on problems with stronger dependencies on new lemmas. Both definitions and theorems are crucial in the context, and models show ability to learn proof structure from previous lemmas. See §?? for more details. 
conclusion: 
 We studied the realistic setting of proving theorems that depend on new information and project constraints, and formulated an evaluation framework for testing generalization using real Lean projects. We built miniCTX, and found that the predominant method for training neural theorem provers fails to enable context dependent proving. Our file tuning method provides a strong starting point for the new challenges opened by our investigation into theorem proving with context. 
 
 Appendix: A Discussion and future challengesIn addition to general improvements in performance, we comment on some specific open challenges.Making better use of long-contexts. Our file-tuning method simply truncates contexts to be within a token budget (1024), which can discard useful contextual information. We found gains in providing GPT-4o 8,000 tokens of context compared to not providing it context, but its absolute performance was still low. There are several possible strategies that can be explored in future work, including feeding in the entire context, retrieval, or mixtures of the two.Repository-level context. We focused on evaluating in-file context in this paper. As shown in §H. The traditional approach to training a language model for theorem proving is to train a model on (state, tactic) pairs, i.e., train it to predict the next step of a proof (i.e., the tactic), given the state provided by the proof assistant (i.e., the proof state) [9, 7, 25, 8] . A drawback to this approach is that at test time, the model is not aware of new context outside of the proof state, such as new lemmas. We will see later on that models trained with this state-tactic approach fail at context-dependent proving.As a stronger baseline for context-dependent proving, we present file-tuning, a simple recipe that trains with (preceding file context, proof state, next-tactic) tuples instead of training with (proof state, next-tactic) pairs (Figure 3 ). This lets the model use new definitions, theorems, or other information that are defined prior to the current tactic at training or at test time. In practice, file-tuning requires extracting contexts and proof states from Lean, which is done by NTP-TOOLKIT.We ran File-tuning. Next, we fine-tune a language model on the union of file-tuning and state-tactic examples. We use the DeepSeek-Coder-1.3b language model [27] based on its performance on code generation tasks and its size, which allowed us to fine-tune with our computational budget. We finetune the model for 3 epochs and select the model based on held-out validation perplexity evaluated every 4,000 steps. The model is available at l3lab/ntp-mathlib-context-deepseek-coder-1.3b.State-tactic tuning. We fine-tune a similar model on l3lab/ntp-mathlib-instruct-st using the same hyperparameters. The model is available at l3lab/ntp-mathlib-st-deepseek-coder-1.3b.We evaluate models for the task of tactic-based theorem proving: given a theorem statement, a model generates one tactic at a time while receiving states from the proof assistant. We use a standard best-first search strategy [9, 7, 28, 8, 1] which prioritizes partial proofs based on the model's average log probabilities. This search method is parameterized by the number of generated tactics per iteration S, and the maximum number of iterations T . We use the setting from [26, 1] (S = 32, and T = 100).We evaluate five types of baselines: (1) pass@1 full proof generation using GPT-4o: we prompt the model with only the theorem statement and require it to generate a complete proof (see Appendix ( §G.2) for details of the prompts and few-shot examples); (2) pass@1 full proof generation with in-file context using GPT-4o: we supplement the theorem statement with up to 8000 tokens of in-file context;(3) the file-tuning model described in ( §4.1); (4) the state-tactic model described in ( §4.1); and (5) a state-tactic prompting model: we prompt a pre-trained language model with (state, tactic) examples, using Llemma-7b [26] .We analyze the baseline models on miniCTX further along several axes, including the kinds of contextual dependencies, the difficulty, and the content made available in the context.File-tuning especially helps on problems with infile dependencies. We use the miniCTX metadata to categorize theorems based on their in-file dependencies. Figure 6 shows the performance of state-tactic tuned model and file-tuned model on problems with in-file dependencies compared to those without. We also show miniF2F as an additional reference point for problems without in-file dependencies. The file-tuned model shows a marked improvement over the state-tactic tuned model, especially in problems that have dependencies on context. We conclude that file-tuning specifically helps in the realistic setting of theorem proving with new definitions and theorems in context.Premise selection helps but may interfere with in-file context. We use miniCTX metadata to categorize problems based on their cross-file dependencies, evaluating the impact of premise selection across the entire dataset. As shown in Figure 4 , GPT-4o benefits significantly from premise selection on problems with high cross-file dependencies, showing improved performance when leveraging relevant premises from imported files. However, we also observe that premise selection can interfere with in-file context, leading to inconsistent results, particularly when the available in-file context is relatively short. This suggests that adding cross-file premises may sometimes disrupt the model's ability to focus on the in-file information. Further analysis of this interference is included in §H.3. This highlights the need for more sophisticated integration strategies that can balance both in-file and cross-file contexts effectively.Models can learn from previous proofs in the file context. To determine the contribution of different components in the in-file context, we conducted an ablation study on the PFR.ForMathlib.Entropy.Basic file, which contains numerous co-related lemmas and rich natural language comments, making it an ideal candidate to investigate the influence of different context components. In this ablation, we systematically removed specific parts of the in-file context and evaluated the model's ability to generate proofs under these modified conditions. As shown in Table 3 , both the file-tuned model and GPT-4o benefit from the inclusion of previous proofs in the file context. This indicates that models are capable of learning proof strategies from existing proofs in the file and effectively applying them to new problems (see §H. 4 for more examples). Natural language comments contribute in certain settings. Our ablation also explored the effect of natural language comments in the in-file context. Though the impact was not dramatic, comments written in natural language were found to be helpful in certain settings. In scenarios where proofs were excluded from the context, adding comments resulted in slight performance gains for both models. For the file-tuned model, these gains were further amplified when proofs were included alongside comments, demonstrating the value of combining formal context with explanatory natural language. However, for GPT-4o, the presence of comments when proofs were included led to a slight decrease in performance, suggesting that effective context selection may vary depending on the model architecture and underlying training characteristics.File-tuning improves across all difficulty levels and context lengths. Finally, Appendix §H.2 shows performance on problems categorized by the length of the human-written proof (when available), which we take as a rough proxy of the problem difficulty. The file-tuned model improved on all three difficulty categories. Appendix §H.2 also shows that file-tuning had improved accuracy across context lengths, particularly for problems with longer contexts. Longer contexts may imply more dependencies, suggesting that these problems can benefit more from file-tuning.To demonstrate an additional kind of contextdependence, we perform an additional analysis on Math2001 [20] , which is another Lean textbook setting. 1 In particular, the textbook code disables powerful automation tactics including simp and linarith to promote manual reasoning, akin to traditional textbook exercises. For example, Math2001 includes numerous arithmetic problems that are trivial with automation tactics (e.g., linarith) but are challenging for models to explicitly prove with step-by-step reasoning (e.g., via calc). In Table 6 we evaluate models with the automation disabled, and observe substantial performance drops, confirming the reliance on automation tactics. We also find that the state-tactic tuned model relies on simp for unseen definitions, making it performing similarly well to the file-tuned model on theorems that only rely on new definitions ( §H.6).Prime Number Theorem. PrimeNumberTheoremAnd [18] is a project started in January 2024 that formalizes the prime number theorem in Lean as well as related concepts, such as residue calculus on rectangles in C. We find the files Rectangle.lean and ResidueCalcOnRectangles.lean suitable for our purpose of testing context-dependent theorem proving, especially when we use preceding file content as context, as each file is self-contained within the project and contains new definitions (rectangles, squares) and many interdependent lemmas. See §E.2 for an illustration of such lemmas. In addition, most theorems from ResidueCalcOnRectangles.lean rely on the definitions from Rectangle.lean, which serves as a perfect example of cross-file dependencies. We extracted 87 theorems from these files. Assuming that a model was trained prior to January 2024, this split guarantees the evaluation of project-level, context-level, and theorem-level generalization.PFR. PFR [19] is a project started in November 2023 that formalizes a proof of the Polynomial Freiman-Ruzsa (PFR) conjecture. We included 54 theorems from PFR. We find that proofs of theorems in PFR tend to be much more monolithic and longer in length than those in Mathlib or other libraries. PFR also defines custom mathematical concepts and notations (such as Ruzsa distance) and a proof typically depends on many lemmas in PFR outside the current file. All of the theorems were added to PFR after November 2023. Assuming that the model was trained prior to this date, this split guarantees the evaluation of project-level, context-level, and theorem-level generalization.Recent Mathlib Commits. Lean's mathematical library, Mathlib [21] , is a community-maintained Lean repository including mathematical concepts as well as programming APIs and common tactics. HTPI. HTPI contains the Lean code for the book How to Prove It (HTPI) [29] , which explains a systematic approach to constructing mathematical proofs with Lean. It covers various topics, including elementary logic, number theory, and proving techniques like mathematical induction, along with their implementation in Lean. As supplementary material to the textbook, the problems in HTPI are formulated in a similar fashion: the files typically start with basic definitions and lemmas that might be used throughout the entire file, followed by exercises and several example problems. 2Therefore, models can utilize definitions, lemmas, and proof structures from example problems to solve similar exercises. Intuitively, the model must understand and apply the context provided within each file, making it an effective benchmark for testing context-aware theorem-proving models.Here we give some examples of the miniCTX and its sources to illustrate the format of the data and how and why we collect certain theorems.An entry in the miniCTX dataset consists of the theorem statement, preceding file contents, and metadata information. For example, given the following theorem s_eq_pow_two in context: We collect its data into miniCTX, formatted in JSON as follows:{ # Preceding file content "srcContext": "import␣Mathlib.Data.Real.Basic\\n\\n/-!\\n#␣Square␣function\\nWe␣ define␣the␣squaring␣function␣`s␣:␣\\u211d␣\\u2192␣\\u211d`␣to␣be␣`s␣x␣:=␣x␣*␣ x`.\\n-/\\n\\ndef␣s␣(x␣:␣\\u211d)␣:␣\\u211d␣:=␣x␣*␣x\\n\\n", # Theorem statement "theoremStatement": "lemma␣s_eq_pow_two␣{x␣:␣\\u211d}␣:␣s␣x␣=␣x␣^␣2", # Fully qualified theorem name "theoremName": "s_eq_pow_two", # Temporal metadata "fileCreated": "(git␣commit)", "theoremCreated": "(git␣commit)", # Source metadata "file": "MyProject/Square.lean", "module": "MyProject.Square", "positionMetadata": { # Line number the theorem is on "lineInFile": 10, # Number of tokens before the theorem "tokenPositionInFile": 152, # Number of premises (definitions, theorems) before the theorem "theoremPositionInFile": 1 }, # Dependency metadata "dependencyMetadata": { # Number of definitions or lemmas defined in this file that the theorem uses "inFilePremises": true, "numInFilePremises": 1, # Number of definitions or lemmas defined in this repository that the theorem uses (including in-file ones) "repositoryPremises": true "numRepositoryPremises": 1, # Number of total premises (in file, repository, or otherwise) "numPremises": 2, # Modules imported in the current file "importedModules": ["Mathlib.Data.Real.Basic", ...] }, # Proof metadata "proofMetadata": { "hasProof": true, "proof": "by\n␣␣rw␣[s,␣pow_two]", "proofType": "tactic", "proofLengthLines": 2, "proofLengthTokens": 20 } }In additional to individual entries, we also record the version (git commit) of the repository.We collect theorems from the Rectangle.lean file in PrimeNumberTheoremAnd. The following excerpt from Rectangle.lean demonstrates the scenario that often arises in a theorem proving environment where context is critical to producing a proof: When proving the final lemma symm_re, a model can benefit much from the preceding file contents, which include (1) the existing imports from Mathlib, variable declarations, and open namespaces that provide a syntactic context for this theorem, (2) the new definition Rectangle in the context, which the model has not seen in training, (3) natural language and LaTeX documentation of the file and Rectangle definition, (4) the analogous (in this case identical) proof of the preceding theorem symm. We demonstrate that performance on Rectangle.lean is indeed much higher when preceding file contents are given as context to a model.For future data added to miniCTX that specifically test the preceding file contents as context, we will ensure it is standalone like Rectangle.lean, i.e. it does not import any other unseen files from the same repository, so the preceding file contents already contain all important information relevant to the proof.In addition to problems in miniCTX, we also evaluated other datasets that are not included due to copyright reasons.Math2001 [20] contains the Lean code for the book The Mechanics of Proof by Heather Macbeth, an introductory text on mathematical theorem proving with accompanying Lean code. Each chapter of The Mechanics of Proof covers an introductory topic and walks through how to write the associated mathematics in Lean, along with exercises. The topics include proofs by calculation, proofs with structure, parity and divisibility, logic, induction, number theory, functions, sets, and relations. A unique aspect of Math2001 is that it disables common Lean automation for pedagogical purposes. For example, a student must write out an equality proof in detail, with each step justified. It also defines new tactics and definitions separate from the common Lean libraries. Typically a file in the textbook will show examples of such proofs, followed by exercises for a student to complete. We can view this as a form of contextual adaptation: a model must prove the theorem according to the constraints of the textbook. Math2001 has 41 files that include examples and exercises. We selected 1 to 2 theorems from each file (depending on the length of the file), for a total of 50 theorems. Of these, 31 have no proof in the Math2001 repository, hence testing theorem-level generalization.Context-aware models surpass state-based models Table 5 shows the performance comparison of different models. Both the GPT-4o model, which includes context in the input, and the file-tuned model perform significantly better than the other models. This demonstrates the importance of context information in context-dependent textbook-style problems.Models rely on common symbolic automation. The Math2001 split originally disables powerful automation tactics including simp and nlinarith to promote manual reasoning, akin to traditional textbook exercises. In Table 6 we evaluate models with the automation disabled, and observe substantial performance drops, confirming a heavy reliance of current models on these automation tactics. An examination of the training corpus further revealed a general dependency on automated tactics within real Lean projects, indicating that our models have learned to rely on these tactics. { "state": # tactic state , "nextTactic": # pretty-printed next tactic, "srcUpToTactic": # source code in the file up to the tactic invocation, "decl": # declaration without proof (e.g., statement of a theorem), "declUpToTactic": # source code in the declaration up to the tactic invocation, "declId": # unique identifier of the declaration }The full proof data is suitable for making evaluation examples of the form (context, theorem, proof):{ "srcUpToDecl": # source code in the file up to the declaration, "decl": # declaration without proof (e.g., statement of a theorem), "declId": # unique identifier of the declaration, "proof": # proof } Full proof data is also suitable for training a model to directly generate a full proof, and NTP-TOOLKIT also provides Lean source with proof states interleaved, both of which we do not explore in this work.G.2 Input-output formatting.Below we show the inputs and outputs for file-tuning and state-tactic tuning. In the paper we refer to the natural language description at the beginning of the input as an "instruction", and refer to a set of inputs and outputs as described below as "instruction-tuning data".G.2.1 File tuning.Given an example containing a state, next-tactic, and preceding file contents (srcUpToTactic), the data is formatted as: Total size of retrieved premises, as proportion of promptInput: /-Performance by size of retrieved premises Success FailureFigure 8 : Impact of length of retrieved premises on GPT-4o model performance. A higher premiseto-context length ratio is correlated with lower success rates, suggesting that too much premise in context overwhelms the model.The file-tuned model is able to utilize the proofs in the context. Here is an example of the model making minimal modification to the proofs from the context: Input:... The file-tuned model is able to utilize the stated theorems in the context. Here is an example of the model using the previously defined theorem in the proof: Input: The state-tactic tuned model is able to utilize the unseen definitions that appear in the proof state. In the following example Set.uIoo is a newly defined definition, which is never seen for state-tactic tuned model: This leads the state-tactic tuned model to perform similarly well as the file-tuned model on problems that only rely on new definitions, and not new theorems (see Figure 6 ).38th Conference on Neural Information Processing Systems (NeurIPS 2024).See Appendix F.1 for further details on Math2001. Due to licensing we do not include it in miniCTX.The main chapter and exercises are separated in the original project: HTPILeanPackage. We manually merged them for evaluation in the fork: HTPILeanPackage4.7. 



Reviews: review: title: title: Official Review
main_review: main_review: Summary: In this submission, the authors recognize as a problem that many neural theorem-proving works are geared to competition-problem solving, but this does not reflect the kind of formalization work actually done by mathematicians. Further, this formalization work is heavily dependent on previously written lemmas and definitions. Other works usually do not provide these as direct context to the model, instead expecting an understanding to be learned during training. However, directly working with background context better reflects a mathematician's formalization workflow. They produce a new benchmark based on testing models ability to operate with context on a number of prior formalization projects, including research-level repositories like PFR and PNT. They also perform some experiments on the benchmark like LLM prompting, BFS with state-tactic prediction, and file-tuning.

Significance: Many formalization projects span many files with many definitions that have been carefully constructed for the particular task. To automate the formalizing workflow, a model must be aware of all these definitions but this can be difficult with a model that has not been trained on all this context. 

1. The authors identify a valuable problem and produce a benchmark that is relevant for the overall task. It is also time-robust and can be updated mostly automatically (clarification: when being updated you will still need to choose new repositories to include in the benchmark, right?) The benchmark also has a varied difficulty, which can be useful for testing out different kinds of models.
2. The experiments are useful for building an intuition for how popular approaches perform with and without context. It should be relevant to further explorations of the problem statement.

Overall, I judge this work to be valuable, especially for the AI-4-math community.
title: title: Solid work on new benchmarks but could use some improvement
main_review: main_review: ### Summary:

This work introduces a benchmark to evaluate automated theorem provers when a local context (e.g., repository-wide) is necessary, as well as a supporting tool to extract and update the benchmark to ensure it stays uncontaminated.

### Strengths:

This work focuses on a benchmark that requires a strong understanding of the context.

This work can be updated continuously to prevent data contamination.

### Limitations:

There are few model evaluations (GPT-4o and Deepseek Coder 1.3B) only.

The benefits over other benchmarks are not extremely clear.
title: title: Positive contribution to the community, clear acceptance
main_review: main_review: ## Strengths

- The work provides a robust evaluation dataset for neural theorem proving, which is very much needed in the community, as previous evaluation suites had serious issues (not only regarding context, but also contamination).
  - The authors utilize knowledge cutoffs to robustly evaluate models' performance without worrying about contamination, and include preceding file contents to better specify the intent.
- Both the eval and train sets are quite large (583k train, 15k dev, and 15k test), allowing for extensive evaluation and training.
- The authors release their code and dataset, making it a valuable contribution that can be used by the community.

## Weaknesses

- Figures could have been made crisper. Figure 1 is hard to read without zooming in, and the lack of vectorization makes it appear pixelated.
- The paper lacks hyperpameters used for both inference and training, making it hard to reproduce results.
title: title: Context-Dependent Theorem Proving with miniCTX: Valuable Contribution, but Needs Clearer Presentation
main_review: main_review: ### **Summary and Final Decision**

The paper introduces the miniCTX dataset and NTP-TOOLKIT, making significant contributions to context-dependent theorem proving. The experiments demonstrate that providing models with context improves performance, particularly through file-tuning. However, explanations of key results, especially comparisons between miniCTX and miniF2F, need more depth. Additionally, the structure could be improved for better readability, and broader implications of the work could be explored more fully. Overall, the contributions are valuable but need clearer presentation of results and smoother transitions.

Rating: 6 (Marginally above acceptance threshold)

### **Strengths:**

1. **Innovative Benchmark (miniCTX):**  
   The introduction of miniCTX as a dataset to test context-dependent theorem proving is a significant contribution. It addresses a critical gap in evaluating models' abilities to handle long, complex contexts, making it a valuable tool for future research in the field.

2. **Practical Toolkit (NTP-TOOLKIT):**  
   The development of NTP-TOOLKIT for data extraction and evaluation is a strong point, enabling reproducibility and simplifying the process of extending the benchmark. This adds practical value and allows for further exploration by other researchers.

3. **Clear Experimental Setup:**  
   The experimental setup is well-structured, comparing different approaches (file-tuning, state-tactic, GPT-4o) across datasets. The choice to compare models with and without context helps demonstrate the importance of leveraging background information in theorem proving.

---

### **Areas for Improvement:**

1. **Insufficient Explanation of Results:**  
   The comparison between miniCTX and miniF2F, while valuable, lacks a clear explanation of why file-tuning performs significantly better in one case but not the other. More detailed analysis is needed to help readers understand the factors influencing these results.

2. **Limited Exploration of Broader Impacts:**  
   The paper focuses heavily on theorem proving but misses an opportunity to discuss broader implications, such as how this approach could be applied to other domains like mathematical education or AI-driven mathematical discovery. Expanding the discussion would enhance the paper’s impact.

3. **Clarity of Language and Structure:**  
   While the structure of the paper is generally sound, certain sections (particularly around the experimental results) could be more cohesive. Transitions between key concepts could be smoother, and the narrative could benefit from more detailed explanations, especially when discussing the significance of the results. Improving the flow would enhance readability and comprehension.

4. **Limited Quantitative Comparisons:**  
   The paper mainly provides qualitative comparisons between datasets like miniCTX and miniF2F. Including more quantitative comparisons, such as how models perform on the same theorems across multiple datasets, would give a stronger empirical foundation to the claims.




### **Evaluation Criteria:**

1. **Relevance to the Journal (5/5):**  
   The paper aligns very well with the journal's focus on AI and mathematical reasoning. It explores an important intersection—leveraging large language models (LLMs) for theorem proving—while addressing key challenges in context-dependent proving. This fits the theme of mathematical comprehension and reasoning capabilities of AI models.

2. **Clarity of Language and Structure (3/5):**  
   The structure of the paper is generally clear, but some sections (e.g., explanations of results) would benefit from more detailed discussion. The transitions between key concepts, especially around the experimental results, could be improved for better readability and flow.

3. **Experimentation Procedure (3/5):**  
   While the experiments are generally well-designed, some results (such as those on miniF2F) lack depth in explanation. It would be helpful if the authors provided more detailed insights into why file-tuning works well in some cases but not others. A more controlled comparison across datasets would strengthen the experimental procedure.

4. **Innovation and Original Contribution (4/5):**  
   The introduction of the miniCTX benchmark is a valuable contribution, but the paper could go further in exploring real-world implications of context-dependent proving. The novelty of the toolkit is commendable, but expanding on potential applications and future use cases would increase the impact of the work.


### Line-By-Line Review

- **Line 3:** "We introduce miniCTX, which tests a model’s ability to prove formal mathematical theorems that depend on new context not encountered in training."

  **Comment:** Specify that miniCTX is a dataset to make this clearer. Without this, it may not be immediately obvious to the reader what miniCTX refers to.

---

- **Line 12:** "We found that this ability to use context is not captured by previous benchmarks such as miniF2F."

  **Comment:** Clarify whether miniF2F is a dataset. Consistently defining these terms is important for avoiding confusion later in the paper when multiple datasets are referenced.

---

- **Lines 61-62:** "Where (x, c) ∼ p denotes a (theorem, context) pair from a context distribution p, M is a model that produces a proof y, and v returns 1 if the proof is correct and 0 otherwise."

  **Comment:** The text only mentions evaluating fully correct proofs, but what about partial proofs? Including an evaluation of partial proofs would provide more insights into model performance, especially for complex problems.

---

- **Line 70:** "Table 1 provides a qualitative comparison with other datasets."

  **Comment:** The table provides a good qualitative comparison, but it would be interesting to see a **quantitative comparison** as well. For example, if the same theorem appears across multiple datasets, it would be valuable to compare how well models trained on miniCTX perform relative to other datasets. This would strengthen the empirical evidence in the paper.

---

- **Lines 124-136:** "We see a dramatic improvement for the file-tuned model over the state-tactic methods (31.65% vs. 9.31%). Similarly, providing preceding file context to GPT-4o results in dramatic improvement (22.07% vs. 5.59%)."

  **Comment:** The results don't provide enough insight into why file-tuning performs much better on miniCTX but not on miniF2F. This comparison between datasets feels incomplete. A better comparison would be to evaluate multiple datasets using the same test data and show how miniCTX excels at proving theorems under those conditions. 

---

- **Line 131:** "The file-tuned model improves very little beyond the state-tactic model (33.61% vs. 32.79%) on miniF2F."

  **Comment:** It’s unclear what this small improvement on miniF2F is meant to prove. The authors should explain why file-tuning does not yield similar gains in miniF2F as it does in miniCTX, or clarify the significance of this result.