{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:09:17Z","timestamp":1784200157731,"version":"3.55.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1762299, CCF-1918889, CNS-1908304, CCF-1901376, CNS-2120696, CCF- 2210831, CCF-2319471"],"award-info":[{"award-number":["CCF-1762299, CCF-1918889, CNS-1908304, CCF-1901376, CNS-2120696, CCF- 2210831, CCF-2319471"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-style proofs, learning higher-level custom tactics is crucial for proof modularity and automation. This paper presents a novel approach to tactic discovery, which leverages Tactic Dependence Graphs (TDGs) to identify reusable proof strategies across multiple proofs. TDGs capture logical dependencies between tactic applications while abstracting away irrelevant syntactic details, allowing for both the discovery of new tactics and the refactoring of existing proofs into more modular forms. We have implemented this technique in a tool called\n                    <jats:sc>TacMiner<\/jats:sc>\n                    and compare it against an anti-unification-based approach (\n                    <jats:sc>Peano<\/jats:sc>\n                    ) to tactic discovery. Our evaluation demonstrates that\n                    <jats:sc>TacMiner<\/jats:sc>\n                    can learn 3\u00d7 as many tactics as\n                    <jats:sc>Peano<\/jats:sc>\n                    and reduces the size of proofs by 26% across all benchmarks. Furthermore, our evaluation demonstrates the benefits of learning custom tactics for proof automation, allowing a state-of-the-art proof automation tool to achieve a relative increase of 172% in terms of success rate.\n                  <\/jats:p>","DOI":"10.1145\/3763121","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1974-2001","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Discovery of Tactic Libraries for Interactive Theorem Proving"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-7608-1873","authenticated-orcid":false,"given":"Yutong","family":"Xin","sequence":"first","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7293-6579","authenticated-orcid":false,"given":"Jimmy","family":"Xin","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7058-8428","authenticated-orcid":false,"given":"Gabriel","family":"Poesia","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9176-8802","authenticated-orcid":false,"given":"Noah D.","family":"Goodman","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4680-5157","authenticated-orcid":false,"given":"Qiaochu","family":"Chen","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"I\u015f\u0131l","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/800028.808479"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660203"},{"key":"e_1_3_2_4_2","unstructured":"Emilio Jes\u00fas Gallego Arias. [n. d.]. Coq SerAPI Library. https:\/\/github.com\/ejgallego\/coq-serapi"},{"key":"e_1_3_2_5_2","first-page":"454","article-title":"HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving","author":"Bansal Kshitij","year":"2019","unstructured":"Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of the 36th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 97), Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 454\u2013463. https:\/\/proceedings.mlr.press\/v97\/bansal19a.html","journal-title":"In Proceedings of the 36th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 97)"},{"key":"e_1_3_2_6_2","volume-title":"The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin, Heidelberg."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_17"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.29007\/wg1q"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571234"},{"key":"e_1_3_2_10_2","unstructured":"Tom B Brown Benjamin Mann Nick Ryder Melanie Subbiah Jared Kaplan Prafulla Dhariwal Arvind Neelakantan Pranav Shyam Girish Sastry Amanda Askell et al. 2020. Language models are few-shot learners. In Advances in Neural Information Processing Systems Vol. 33. 1877\u20131901."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385988"},{"key":"e_1_3_2_13_2","unstructured":"Coq Community. 2024. Coq-Art: Practical Foundations for Programming with Dependent Types. https:\/\/github.com\/coqcommunity\/coq-art. Accessed: 2024-11-04."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"\u0141ukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning 61 1 (2018) 423\u2013453. https:\/\/doi.org\/10.1007\/s10817-018-9458-4 10.1007\/s10817-018-9458-4","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Ana de Almeida Borges Annal\u00ed Casanueva Art\u00eds Jean-R\u00e9my Falleri Emilio Jes\u00fas Gallego Arias \u00c9rik Martin-Dorel Karl Palmskog Alexander Serebrenik and Th\u00e9o Zimmermann. 2023. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 268) Adam Naumowicz and Ren\u00e9 Thiemann (Eds.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 12:1\u201312:18. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.12 10.4230\/LIPIcs.ITP.2023.12","DOI":"10.4230\/LIPIcs.ITP.2023.12"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1765236.1765246"},{"key":"e_1_3_2_17_2","unstructured":"Reinhard Diestel. 2024. Graph theory. Springer (print edition); Reinhard Diestel (eBooks)."},{"key":"e_1_3_2_18_2","volume-title":"In Advances in Neural Information Processing Systems","author":"Ellis Kevin","year":"2018","unstructured":"Kevin Ellis, Lucas Morales, Mathias Sabl\u00e9-Meyer, Armando Solar-Lezama, and Josh Tenenbaum. 2018. Learning Libraries of Subroutines for Neurally\u2013Guided Bayesian Program Induction. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.), Vol. 31. Curran Associates, Inc. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/7aa685b3b1dc1d6780bf36f7340078c9-Paper.pdf"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454080"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Yu Feng Saswat Anand Isil Dillig and Alex Aiken. 2014. Apposcopy: Semantics-based detection of android malware through static analysis. In Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering. 576\u2013587.","DOI":"10.1145\/2635868.2635869"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"Yu Feng Osbert Bastani Ruben Martins Isil Dillig and Saswat Anand. 2017. Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. In 24th Annual Network and Distributed System Security Symposium NDSS 2017 San Diego California USA February 26 - March 1 2017. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2017\/ndss-2017-programme\/automated-synthesis-semantic-malware-signatures-using-maximum-satisfiability\/","DOI":"10.14722\/ndss.2017.23379"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Yu Feng Ruben Martins Osbert Bastani and Isil Dillig. 2018. Program synthesis using conflict-driven learning. ACM SIGPLAN Notices 53 4 (2018) 420\u2013435.","DOI":"10.1145\/3296979.3192382"},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Jeanne Ferrante Karl J Ottenstein and Joe D Warren. 1987. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems (TOPLAS) 9 3 (1987) 319\u2013349.","DOI":"10.1145\/24039.24041"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368132"},{"key":"e_1_3_2_27_2","unstructured":"Daniel Huang Prafulla Dhariwal Dawn Song and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7"},{"key":"e_1_3_2_28_2","unstructured":"Aaron Hurst Adam Lerer Adam P Goucher Adam Perelman Aditya Ramesh Aidan Clark AJ Ostrow Akila Welihinda Alan Hayes Alec Radford et al. 2024. GPT-4o System Card. arXiv preprint arXiv:2410.21276 (2024)."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D19-1545"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Cezary Kaliszyk and Josef Urban. 2015. Learning-assisted theorem proving with millions of lemmas. Journal of symbolic computation 69 (2015) 109\u2013128.","DOI":"10.1016\/j.jsc.2014.09.032"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Y. Kataoka M.D. Ernst W.G. Griswold and D. Notkin. 2001. Automated support for program refactoring using invariants. In Proceedings IEEE International Conference on Software Maintenance. ICSM 2001. 736\u2013743. https:\/\/doi.org\/10.1109\/ICSM.2001.972794 10.1109\/ICSM.2001.972794","DOI":"10.1109\/ICSM.2001.972794"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_33_2","unstructured":"Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao and Anima Anandkumar.2024. LeanAgent: Lifelong Learning for Formal Theorem Proving. arXiv:2410.06209 [cs.LG] https:\/\/arxiv.org\/abs\/2410.06209"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2993236.2993244"},{"key":"e_1_3_2_35_2","unstructured":"Xavier Leroy. 2021. Companion Coq development for Xavier Leroy\u2019s 2021 lectures on program logics. https:\/\/github.com\/xavierleroy\/cdf-program-logics. GitHub repository."},{"key":"e_1_3_2_36_2","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems 8th European Congress."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1150402.1150522"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695521"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","unstructured":"Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. ACM SIGPLAN Notices 50 6 (2015) 619\u2013630.","DOI":"10.1145\/2813885.2738007"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632870"},{"key":"e_1_3_2_41_2","unstructured":"Gordon D Plotkin. 1970. A note on inductive generalization. Machine intelligence 5 1 (1970) 153\u2013163."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Gabriel Poesia and Noah D. Goodman. 2023. Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A: Mathematical Physical and Engineering Sciences 381 2251 (2023) 20220044. https:\/\/doi.org\/10.1098\/rsta.2022.0044 10.1098\/rsta.2022.0044 arXiv: https:\/\/royalsocietypublishing.org\/doi\/pdf\/10.1098\/rsta.2022.0044","DOI":"10.1098\/rsta.2022.0044"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386001"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"Barbara G Ryder. 1979. Constructing the call graph of a program. IEEE Transactions on Software Engineering 3 (1979) 216\u2013226.","DOI":"10.1109\/TSE.1979.234183"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Alex Sanchez-Stern Yousef Alhessi Lawrence Saul and Sorin Lerner. 2020. Generating correctness proofs with neural networks. Association for Computing Machinery New York NY USA 1\u201310.https:\/\/doi.org\/10.1145\/3394450.3397466 10.1145\/3394450.3397466","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_3_2_47_2","first-page":"13","volume-title":"In Proceedings of the 34th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (NIPS \u201920)","author":"Shah Ameesh","year":"2020","unstructured":"Ameesh Shah, Eric Zhan, Jennifer J. Sun, Abhinav Verma, Yisong Yue, and Swarat Chaudhuri. 2020. Learning differentiable programs with admissible neural heuristics. In Proceedings of the 34th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (NIPS \u201920). Curran Associates Inc., Red Hook, NY, USA, Article 415, 13 pages."},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","unstructured":"Marc Shapiro and Susan Horwitz. 1997. Fast and accurate flow-insensitive points-to analysis. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1\u201314.","DOI":"10.1145\/263699.263703"},{"key":"e_1_3_2_49_2","unstructured":"Peiyang Song Kaiyu Yang and Anima Anandkumar. 2024. Towards large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534 (2024)."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Friedrich Steimann. 2018. Constraint-Based Refactoring. ACM Trans. Program. Lang. Syst. 40 1 Article 2 (Jan. 2018) 40 pages. https:\/\/doi.org\/10.1145\/3156016 10.1145\/3156016","DOI":"10.1145\/3156016"},{"key":"e_1_3_2_51_2","unstructured":"Amitayush Thakur George Tsoukalas Yeming Wen Jimmy Xin and Swarat Chaudhuri. 2024. An In-Context Learning Agent for Formal Theorem-Proving. In First Conference on Language Modeling. https:\/\/openreview.net\/forum?id=V7HRrxXUhN"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00161"},{"key":"e_1_3_2_53_2","unstructured":"Laurent Th\u00e9ry Benjamin Gr\u00e9goire Arnaud Spiwack Evgeny Makarov and Pierre Letouzey. 2026. Bignums. https:\/\/github.com\/coq-community\/bignums. GitHub repository."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Frank Tip Robert M. Fuhrer Adam Kie\u017cun Michael D. Ernst Ittai Balaban and Bjorn De Sutter. 2011. Refactoring using type constraints. ACM Trans. Program. Lang. Syst. 33 3 Article 9 (may 2011) 47 pages. https:\/\/doi.org\/10.1145\/1961204.1961205 10.1145\/1961204.1961205","DOI":"10.1145\/1961204.1961205"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314588"},{"key":"e_1_3_2_56_2","unstructured":"Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arXiv:1608.02644 [cs.AI] https:\/\/arxiv.org\/abs\/1608.02644"},{"key":"e_1_3_2_57_2","unstructured":"Huajian Xin Haiming Wang Chuanyang Zheng Lin Li Zhengying Liu Qingxing Cao Yinya Huang Jing Xiong Han Shi Enze Xie et al. 2023. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656 (2023)."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Yutong Xin. 2025. TacMiner: Automated Discovery of Tactic Libraries for Interactive Theorem Proving. https:\/\/doi.org\/10.5281\/zenodo.15761151 10.5281\/zenodo.15761151","DOI":"10.5281\/zenodo.15761151"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.findings-emnlp.146"},{"key":"e_1_3_2_60_2","unstructured":"Jin Peng Zhou Yuhuai Wu Qiyang Li and Roger Grosse. 2024. REFACTOR: Learning to Extract Theorems from Proofs. arXiv preprint arXiv:2402.17032 (2024)."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416541"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763121","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:03Z","timestamp":1784196603000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":60,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763121"],"URL":"https:\/\/doi.org\/10.1145\/3763121","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}