miniCTX: Neural Theorem Proving with (Long-)Contexts

Thank you for your review and your feedback on our paper. We address your questions and concerns below.

1. 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?

Thank you for pointing this out! We provide only the imported modules as context when evaluating miniF2F. In the comparison between state-tactic tuning and file tuning on miniF2F, the inputs are almost identical. This experiment is designed to demonstrate that the file-tuning method maintains the same level of reasoning ability as traditional methods when context is limited or absent. We have updated our paper to state this.

2. 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.

We initially did not report the GPT-4o result on miniF2F, because the focus of our work is on the $`miniCTX`$ benchmark and context-aware setting. However, we agree it is better to include them for completeness of evaluation, and comparison to $`miniCTX`$ and previous works. Using the same prompt in a pass@8 setup, GPT-4o achieves 13.52% accuracy on the miniF2F test split. We have updated Table 3 to include GPT-4o performance on miniF2F in our paper.

Thank you for your review and your feedback on our paper. We address your questions and concerns below.

1. $`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.

We thank the reviewer for this suggestion. Indeed, we are planning to add a validation split to $`miniCTX`$. While the extraction process using our toolkit only takes a few minutes, evaluating all models on the new split will require additional time. We plan to include the validation split as well as corresponding evaluation in the final camera-ready version.

2. It seems that some problems in $`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 $`miniCTX`$ could be transformed into context-free problems under certain efforts.

The in-line transformation is indeed applicable to the examples in Appendix A.1 and A.2. It more generally holds for theorems whose statement involves only new Lean defs or abbrevs, essentially amounting to calling using the tactic unfold in the first line of the proof. This transforms a context-dependent problem into a context-free problem (while losing information such as previous proofs and lemmas).

From a manual inspection, many theorems in $`miniCTX`$ can technically be transformed in this way, by recursively unfolding definitions. We note that this cannot be applied to class, structure, or inductive type definitions, or certain recursive definitions: e.g. there is no easy way to rewrite Nat.add a b to a form without Nat.add.

However, we do not believe unfolding definitions is a valid approach to proving context-dependent problems. For example, a later theorem in Rectangle.lean [1] is: square_neg (p : ℂ) (c : ℝ) : Square p (-c) = Square p c. While we can transform this by definition of Square p c = Rectangle (-c - c * I + p) (c + c * I + p) and then recursively Square p c = [[(-c - c * I + p).re, (c + c * I + p).re]] ×ℂ [[(-c - c * I + p).im, (c + c * I + p).im]], the actual proof benefits from the fact that a Square is a Rectangle and the lemma Rectangle.symm (proved in the example given in Appendix A.2). In other words, even if the theorem statement itself can be transformed to a context-free problem, the actual proof might benefit from the lemmas in the context, which are furthermore stated in an unexpanded format. It is up to the prover whether the definitions should be unfolded, and whether lemmas in context should be used. Moreover, the transformed statement can be exceedingly long, if there are multiple levels of definition (consider let s x := x * x, t x := s (s x), u x := t (t x), and then u e for some long e becomes (((e * e) * (e * e)) * ((e * e) * (e * e))) * (((e * e) * (e * e)) * ((e * e) * (e * e))); long chains of definitions are common in e.g. the HepLean split).

[1] https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Rectangle.lean

3. Is the 1.3b model in L349 the same as the DeepSeek Coder 1.3b in L343?

Yes. We thank the reviewer for pointing this out, and we have revised the relevant part in our paper.

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

Yes, the “'Environment” includes imports, open namespace statements, variable declarations, and other contextual elements necessary for the theorem's setup. To distinguish it from definitions and lemmas, the environment does not introduce new information.

I appreciate the author's response. My questions and concerns are properly addressed. I put my confidence and trust for the authors for their commitment of maintaining a temporal split and I believe miniCTX, along with the Tookit, could be valuable assets to the community.

I will maintain my score and recommend an acceptance.

Thank you for your review and your feedback on our paper.

1. 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?

$`miniCTX`$ differs from previous theorem-proving extraction tools in its motivation. We aim to test the theorem-proving ability of LLMs in a real-world, context-dependent setting that is safe from potential data contamination. This is a different motivation than benchmarks that test models without contextual information. $`miniCTX`$ is the first benchmark that incorporates full real-world context for theorem proving. As demonstrated in our context ablation analysis (Table 4), different components contribute to the performance differently, showing the importance of the full context. Second, our motivation is different from benchmarks extracted from a static snapshot of a project (e.g. LeanDojo [1]) that the model has also trained on. While in principle new snapshots might be re-extracted or carefully split based on time, these ideas have not been realized in a benchmark. Table 1 thereby reflects these differences, showing the position of $`miniCTX`$ among relevant work.

Our NTP-TOOLKIT is also the first unified, automated, and simple framework for extracting context-level data and creation timestamps from any Lean repository. It lowers the cost of extraction for future evaluations. We are also the first benchmark to provide a comprehensive evaluation on the importance of contextual information.

2. First, since the temporal split is emphasized, is there any empirical evidence to support the failure of other benchmarks to handle this properly?

Yes! All public static benchmarks in Lean such as LeanDojo’s extracted Mathlib [1] and miniF2F [2] are at risk of data contamination. For LeanDojo, any model (e.g. internLM [3], DeepSeek-Prover [4]) that has pre-trained on public GitHub data, including Mathlib, has seen the proofs in the eval and test splits of LeanDojo’s benchmark (note that Mathlib4 has large parts copied from its predecessor Mathlib3, which was created in 2017).

For another example in competition-style datasets, a significant portion of problems in miniF2F-test have solutions available on GitHub. In the original miniF2F repository [2], there are 72 test problems already stated with complete proofs. Additionally, the following IMO problems in miniF2F-test: 1959 P1, 1960 P2, 1977 P6, 1982 P1, 2001 P6, 2019 P1 are all fully formalized in Lean inside Mathlib’s Archive/Imo library [5]; 1962 P2, 1963 P5, 1964 P2, 1965 P2, 1968 P5, 1981 P6 are all fully formalized in Lean in Compfiles [6]. So at least 84/244 theorems in miniF2F-test, including 12/19 IMO problems, have full solutions on GitHub.

We have added a new Appendix G (referenced on L274) to support this claim, in order to provide a clearer motivation for the temporal split in $`miniCTX`$.

[1] 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.

[2] 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.

[3] Wu, Zijian, et al. "InternLM2. 5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems." arXiv preprint arXiv:2410.15700 (2024).

[4] Xin, Huajian, et al. "DeepSeek-Prover-V1. 5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search." arXiv preprint arXiv:2408.08152 (2024).

[5] https://github.com/leanprover-community/mathlib4/tree/master/Archive/Imo

[6] https://github.com/dwrensha/compfiles

3. 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?

Thank you for this suggestion! We are currently file-tuning a Llama 3 8B model and evaluating it on $`miniCTX`$, which we will hopefully complete before the discussion period ends (currently, our computational resources are limited).

The idea behind file-tuning is to provide the full file context to the model during proof generation. While we have demonstrated the effectiveness of file-tuning on DeepSeek-Coder-1.3B, we have also observed substantial performance improvements when using few-shot prompting with context for GPT-4o and Llemma-7B. Although these larger models were not fine-tuned using the file-tuning dataset, the underlying principle of leveraging full context remains consistent. So there is reasonable belief that file-tuning works across different models.

We sincerely thank the reviewers for their thoughtful and constructive feedback, as well as for recognizing the significance of our contributions.

We are pleased to share the results of our ongoing experiments with the Llama-3.1-8B model. Specifically, we tested both state-tactic tuning and file-tuning on this model, and its performance on the $`miniCTX`$ benchmark improved from 18.75% to 23.70%, demonstrating the effectiveness of the file-tuning method. However, the improvement is less pronounced compared to the DeepSeek-Coder model. We hypothesize that this is primarily due to the Llama-3.1 model lacking pretraining on formal math related data compared to other models we are testing. The full result is shown in the following table:

We thank the reviewers once again for their time and effort in providing detailed feedback and raising thoughtful questions. We hope that $`miniCTX`$, as a more comprehensive benchmark under realistic settings, will serve as a valuable resource for the formal mathematics community, inspiring further exploration into the potential of neural theorem provers.