miniCTX: Neural Theorem Proving with (Long-)Contexts

Authors: Jiewen Hu, Thomas Zhu, Sean Welleck
Primary area: datasets and benchmarks
Keywords: neural theorem proving, formal mathematics, benchmark dataset

Abstract:
Real-world formal theorem proving often depends on a wealth of context, 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 that is not seen during 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 use 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.

Decision: accept (oral)
Reviewer scores: 8, 8, 8

Reviews and discussion:
<thread>
creation date:
1729500604254

thread_type:
official_review

<thread_object>
creator: reviewer_jrzz

<content>
summary:
This work propose a new formal theorm proving dataset that tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. This work also reports the baseline results of the miniCTX dataset.

strengths:
* This work provides a new dataset for the theorem proving, which tests the model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. And the ability to use context is not captured by previous benchmarks such as miniF2F.
* The work provides baseline results on miniCTX, telling the difficulty of the proposed miniCTX.
* The work provides detailed analysis on the experiments.
* The work provides details of the miniCTX dataset and samples in the Appendix, which makes it easy to understand what the miniCTX looks like.

weaknesses:
* For the Table 3, how do you test the File tuning Model result on miniF2F, as the miniF2F only has the formal statement? You may: 1) only give the formal statement for File tuning Model and get the result; 2) Or, you provide addtional context information by any way?; 
* For Table 3, you do not report the result of GPT-4o (full proof), could you explain why? Previous works (DSP, LEGO-Prover or Lyra) all reports the results GPT-4 on miniF2F.

questions:
Please check the weakness
</content>
</thread_object>

</thread>
<thread>
creation date:
1730506258083

thread_type:
official_review

<thread_object>
creator: reviewer_uxmr

<content>
summary:
This paper introduces a new benchmark called miniCTX for evaluating a model's context-dependent theorem proving abilities, i.e., a model's ability to maximize Expectation_{(theorem, context) ~ repository} Expectation_{proof ~ model(. | theorem, context )} [theorem is valid proof in context]. In-file context includes the source code that precedes the theorem in the file while cross-context includes the in-file context and relevant premises from imported modules. The authors argue that this is a more realistic evaluation of a model's theorem proving abilities. Additionally, the paper introduces NTP-toolkit, a tool for constructing/extending miniCTX with future repositories and running baseline evaluations.

strengths:
- The paper introduces a useful tool (NTP-toolkit) and benchmark (miniCTX) for evaluating a model's theorem proving capabilities. The Python Lean REPL, provided that it is performant, is another useful component that will enable researchers to more easily evaluate models.
- A benchmark of context-dependent theorem proving and a model that performs well on it could potentially be useful for assisting humans using Lean for formal verification.
- The idea of file tuning, i.e., training model(tactic | theorem, context) is novel.

weaknesses:
- The differences between benchmarks shown in Table 1 is, in my perspective, superficial. For example, what fundamental reason is there from preventing other theorem-proving extraction tools from extracting a timestamp or saving the file name that a theorem is extracted from?
- There seem to be a few missing experiments. First, since the temporal split is emphasized, is there any empirical evidence to support the failure of other benchmarks to handle this properly? Second, for file-tuning, have other LLMs / those fine-tuned on Mathlib been tested with file-tuning to see if file-tuning works across different models? Third, In Table 4, I'd like to see context = environment + definition + lemma statement but without natural language comments. This way, we can see just how much having the lemma proof affects file-tuning to better support the claim that models can learn from previous proofs in context.
-  While the paper offers empirical evidence and some analysis, there isn't much in the form of hypotheses to guide the design of the benchmark or experiments. As an example hypothesis, while it might not be surprising that model(tactic | theorem, context) > model(tactic | theorem) since we condition on more information, we hypothesize that the gains come mostly from context = previous proofs since this offers the appropriate context as to when an automated tactic can be most beneficially applied. Such hypotheses would help guide and focus the experiments, and offer more insight into the success and failure cases of neural theorem proving with LLMs.

questions:
- The weaknesses section contains questions that I'd be curious to hear the answers to.
- Why doesn't the cross-file context include the source code of imported modules as opposed to just the premises? Is this just because of context-length limitations?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730557118249

thread_type:
official_review

<thread_object>
creator: reviewer_gdka

<content>
summary:
This paper introduces $\texttt{miniCTX}$, a benchmark of 384 problems with context-rich information, e.g., in-file definitions and lemmas, and evaluates the model's theorem-proving ability under new context, which claims to be closer to the real-world scenario when researchers develop the formal repository. The paper further includes the NTP-TOOLKIT that the authors use for data extraction. The authors provide several baseline experiments, including the common practice of state-tactic tuning and prompting methods (which works for standalone problems as presented in $\texttt{miniF2F}$) and file-tuning that works under such a context-rich setup.

strengths:
1. The $\texttt{miniCTX}$ benchmark fills the gap in the current community: it expands current benchmarks by addressing the limitations of standalone theorem proving and enabling evaluation in real-world scenarios where context is critical.

2. I appreciate the authors' commitment to automatically updating the benchmark and maintaining a temporal split to mitigate the data contamination, given that most LLMs nowadays crawl GitHub and train on it.

3. The authors present details for constructing the benchmark and the sources. The addition of the $\texttt{miniCTX}$ and the NTP-TOOLKIT will be valuable assets to the community. The authors also present solid baselines in Table 3 using inference-time methods with GPT-4o and fine-tuning methods using 1.3b model. An ablation of providing different contexts is also presented in Table 4 to show the source of gain from each context component.

weaknesses:
1. $\texttt{miniCTX}$ does not have a valid/test set separation. Though it's not inherently an issue for a benchmark, separating a valid set could make the benchmark less gameable under Goodhart's law.

2. It seems that some problems in $\texttt{miniCTX}$ are with contexts that could be easily "in-lined" and transformed into context-less problems. For example, the example shown in Appendix A.1: one could easily in-line the square function $s$ definition into the lemma s\_eq\_pow\_two and make the statement to be $x * x = x ^ 2$ from $s \ x = x ^ 2$. The same in-line transformation seems to be also applied to the example in Appendix A.2 by inlining the Rectangle definition. It would be great for the author to assess how many problems in $\texttt{miniCTX}$ could be transformed into context-free problems under certain efforts.

questions:
1. Is the 1.3b model in L349 the same as the DeepSeek Coder 1.3b in L343?

2. What is the "Environment" in Table 4? Does it stand for the import statements / open namespace statements or something else?
</content>
</thread_object>

</thread>
<thread>
creation date:
1732148156613

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Overall Response

comment:
## General Response
We thank the reviewers for valuable and encouraging feedback. We are grateful to all three reviewers for recognizing the important contributions of a benchmark for context-dependent theorem proving in real-world scenarios, and the baseline evaluations presented on $\texttt{miniCTX}$. We appreciate reviewers gDKA and uXMR for acknowledging the utility of our data extraction tool NTP-TOOLKIT for the research community, and reviewers gDKA and jrzz for recognizing the details of dataset construction and analysis. We respond to each reviewer separately below. We have also revised our paper to incorporate the feedback.

We first summarize the motivation and main contributions of $\texttt{miniCTX}$.

In recent years, large language models have been applied to completing verified mathematical proofs in interactive theorem provers [1, 2]. However, existing benchmarks fail to evaluate this ability of LLMs—competition benchmarks such as miniF2F [3] do not incorporate the rich contextual information seen in real-world theorem proving settings, while benchmarks based on a library such as Mathlib [4, 5, 6] at most include a subset of the available context, such as premises. State-of-the-art LLM-based provers are also trained without incorporating the full context [7, 8]. Moreover, all existing benchmarks face significant risks of data contamination, undermining the accuracy of their evaluations.

$\texttt{miniCTX}$ is the first benchmark that evaluates formal theorem proving in a context-aware, real-world setting. Specifically, we:
- (1) provide the $\texttt{miniCTX}$ benchmark sourced from real-world projects, incorporating all contextual information necessary for a proof;
- (2) provide ntp-toolkit, which automatically extracts relevant theorems from Lean projects, while ensuring no data contamination by using a temporal split; 
- (3) evaluate several baselines on $\texttt{miniCTX}$, demonstrating that a simple but effective method, file-tuning, significantly helps real-world theorem proving.

We hope $\texttt{miniCTX}$ will enable richer and more accurate evaluations of theorem-proving abilities of LLMs.

## Revisions to the paper
* L349: “a 1.3b model” → “DeepSeek-Coder-1.3b”
* Added a new Appendix G (referenced on L274) showing data contamination issues in other benchmarks, to support the importance of temporal split
* Added evaluation setup details on miniF2F (L407)
* Added performance of GPT-4o on miniF2F (Table 3)

## Ongoing experiments
* To further strengthen our findings and verify if file-tuning generalizes across different models, we are currently evaluating file-tuning on Llama-3.1 8B.
* Evaluating baselines on a new test split

## Thank you
Thank you again for taking the time to review our paper, and we sincerely hope that you take these discussions into consideration when re-evaluating the work. We have also responded in more detail to your specific concerns below.

## Reference

[1] Sean Welleck and Rahul Saha. LLMSTEP: LLM proofstep suggestions in Lean. arXiv preprint arXiv:2310.18457, 2023. 

[2] Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024.

[3] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv.

[4] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact cotraining for theorem proving with language models. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=rpxJc9j04U.

[5] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023.

[6] Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019.

[7] Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. InternLM-Math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024.

[8] Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. DeepSeek-Prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024. URL https://arxiv.org/abs/2408.08152.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper introduces miniCTX, a novel benchmark for evaluating neural theorem-proving models in real-world, context-rich scenarios, alongside NTP-toolkit, an automated tool for data extraction and annotation. The propositions are well-motivated, addressing the limitations of existing benchmarks (e.g., miniF2F, which focuses on isolated problems) and emphasizing the importance of context in theorem proving. 

The reviewers unanimously appreciated the benchmark’s contribution to advancing formal mathematics research, particularly the attention to mitigating data contamination through temporal splits. Baseline evaluations and ablation studies were also thorough and insightful, showcasing the effectiveness of context-aware approaches like file-tuning.

There were some shared concerns among reviewers, including the absence of a validation split, the potential for simplifying problems into context-free forms, and incomplete experiments on additional models. However, the rebuttal addressed these issues to a reasonable extent, with the authors committing to further improvements (e.g., adding a validation split and additional experiments).

Overall, I agree with the reviewers that this paper offers significant contributions to the field. The authors are encouraged to incorporate the additional evaluations and clarifications discussed during the rebuttal phase when preparing the final version of the paper.