Overall Response
## 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.