{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T19:44:54Z","timestamp":1782848694907,"version":"3.54.5"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T00:00:00Z","timestamp":1782777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Major Program of the National Natural Science Foundation of China","award":["62192733\uff0c62192730"],"award-info":[{"award-number":["62192733\uff0c62192730"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>Interactive theorem proving (ITP) is a powerful approach to ensuring the correctness of complex software systems. However, it often requires substantial manual effort, which makes it costly to use in practice. Recently, neural network based approaches have shown promise in automatically generating proof tactics. Nevertheless, existing methods suffer from a long-tailed distribution in tactic usage within the training data. A few frequent tactics dominate the probability distribution, while many rare yet crucial ones are consistently suppressed in the model\u2019s candidate ranking. This distributional bias can cause potentially provable goals to be prematurely abandoned during proof search. In addition, the decision making process of neural networks when generating tactics lacks explicit reasoning traces, making it difficult for humans to explain or verify the underlying logic. To address these limitations, we propose ProofFusion, an adaptive retrieval-augmented reasoning framework that improves the proving capability of neural theorem provers without requiring retraining. Our key insight is inspired by the way human provers tackle a new theorem by consulting similar previously proven theorems to guide their own reasoning. Specifically, we develop a proof semantic-aware retriever that searches a knowledge base for semantically similar historical proof goals together with their tactic, producing a traceable set of reference decisions. We then employ a dual-track reranking fusion mechanism to integrate both the original predictions of the neural model and the retrieved reference tactics. Furthermore, to mitigate potential noise introduced by retrieval, we design a capability-adaptive retrieval mechanism that dynamically determines when retrieval should be applied. We conduct a systematic evaluation on 10,782 theorems from 26 Coq projects in a real ITP environment. Experimental results show that ProofFusion increases the number of theorems proved by four state-of-the-art neural theorem provers by an average of 6.89%, and additionally proves 17.50% of previously unprovable theorems. In addition, it substantially improves the explainability of proof steps, achieving an average explainable proof goal proportion of 82.1% across the four provers. Together, these results demonstrate that ProofFusion is a practical and effective complement to existing neural theorem proving systems, enhancing both performance and explainability.<\/jats:p>","DOI":"10.1145\/3797139","type":"journal-article","created":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T17:06:14Z","timestamp":1782839174000},"page":"479-502","source":"Crossref","is-referenced-by-count":0,"title":["ProofFusion: Improving Neural Theorem Proving via Adaptive Retrieval-Augmented Reasoning"],"prefix":"10.1145","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9086-0503","authenticated-orcid":false,"given":"Manqing","family":"Zhang","sequence":"first","affiliation":[{"name":"Northwestern Polytechnical University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9882-9121","authenticated-orcid":false,"given":"Yunwei","family":"Dong","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1730-2507","authenticated-orcid":false,"given":"Lingru","family":"Zhou","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3960-9248","authenticated-orcid":false,"given":"Bingxu","family":"Xiao","sequence":"additional","affiliation":[{"name":"Northwestern Polytechnical University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8147-8126","authenticated-orcid":false,"given":"Yepang","family":"Liu","sequence":"additional","affiliation":[{"name":"Southern University of Science and Technology, Shenzhen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,30]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-010-0025-6"},{"key":"e_1_2_1_2_1","volume-title":"Jelle Piepenbrock, and Vasily Pestun.","author":"Blaauwbroek Lasse","year":"2024","unstructured":"Lasse Blaauwbroek, Miroslav Ol\u0161\u00e1k, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. 2024. Graph2Tac: Online representation learning of formal math concepts. arXiv preprint arXiv:2401.02949 (2024)."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639168"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639085"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.00116"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1283920.1962298"},{"key":"e_1_2_1_7_1","volume-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 85-95","author":"Delahaye David","year":"2000","unstructured":"David Delahaye. 2000. A tactic language for the system Coq. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 85-95."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3617330"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acl-long.540"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.findings-emnlp.139"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11816508_24"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510138"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428299"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_15_1","volume-title":"First-order logic and automated theorem proving","author":"Fitting Melvin","unstructured":"Melvin Fitting. 2012. First-order logic and automated theorem proving. Springer Science & Business Media."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3694987"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/cvpr46437.2021.01484"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/icsme58944.2024.00028"},{"key":"e_1_2_1_20_1","volume-title":"HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement. arXiv preprint arXiv:2505.15740","author":"Hu Jilin","year":"2025","unstructured":"Jilin Hu, Jianyu Zhang, Yongwang Zhao, and Talia Ringer. 2025. HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement. arXiv preprint arXiv:2505.15740 (2025)."},{"key":"e_1_2_1_21_1","first-page":"113","article-title":"The coq proof assistant a tutorial","volume":"178","author":"Huet G\u00e9rard","year":"1997","unstructured":"G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. 1997. The coq proof assistant a tutorial. Rapport Technique 178 (1997), 113.","journal-title":"Rapport Technique"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.naacl-long.389"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.emnlp-main.550"},{"key":"e_1_2_1_24_1","volume-title":"Nearest neighbor machine translation. arXiv preprint arXiv:2010.00710","author":"Khandelwal Urvashi","year":"2020","unstructured":"Urvashi Khandelwal, Angela Fan, Dan Jurafsky, Luke Zettlemoyer, and Mike Lewis. 2020. Nearest neighbor machine translation. arXiv preprint arXiv:2010.00710 (2020)."},{"key":"e_1_2_1_25_1","volume-title":"Generalization through memorization: Nearest neighbor language models. arXiv preprint arXiv:1911.00172","author":"Khandelwal Urvashi","year":"2019","unstructured":"Urvashi Khandelwal, Omer Levy, Dan Jurafsky, Luke Zettlemoyer, and Mike Lewis. 2019. Generalization through memorization: Nearest neighbor language models. arXiv preprint arXiv:1911.00172 (2019)."},{"key":"e_1_2_1_26_1","volume-title":"Supervised contrastive learning. Advances in neural information processing systems 33","author":"Khosla Prannay","year":"2020","unstructured":"Prannay Khosla, Piotr Teterwak, Chen Wang, Aaron Sarna, Yonglong Tian, Phillip Isola, Aaron Maschinot, Ce Liu, and Dilip Krishnan. 2020. Supervised contrastive learning. Advances in neural information processing systems 33 (2020), 18661-18673."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/d14-1181"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538"},{"key":"e_1_2_1_30_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th","author":"Leroy Xavier","year":"2016","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"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.00009"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3728884"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2025.3558403"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639122"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/tai.2022.3207112"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/apsec57359.2022.00048"},{"key":"e_1_2_1_37_1","volume-title":"A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939","author":"Li Zhaoyu","year":"2024","unstructured":"Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. 2024. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939 (2024)."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3404835.3463238"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1162\/tacl_a_00556"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3671016.3672506"},{"key":"e_1_2_1_41_1","volume-title":"Retrieval-augmented generation for code summarization via hybrid GNN. arXiv preprint arXiv:2006.05405","author":"Liu Shangqing","year":"2020","unstructured":"Shangqing Liu, Yu Chen, Xiaofei Xie, Jingkai Siow, and Yang Liu. 2020. Retrieval-augmented generation for code summarization via hybrid GNN. arXiv preprint arXiv:2006.05405 (2020)."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-025-09728-1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.36"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.acllong.817"},{"key":"e_1_2_1_45_1","volume-title":"A survey of interactive theorem proving. Zbornik radova 18, 26","author":"Maric Filip","year":"2015","unstructured":"Filip Maric. 2015. A survey of interactive theorem proving. Zbornik radova 18, 26 (2015), 173-223."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2025.acl-industry.72"},{"key":"e_1_2_1_47_1","volume-title":"A survey on theorem provers in formal methods. arXiv preprint arXiv:1912.03028","author":"Nawaz M Saqib","year":"2019","unstructured":"M Saqib Nawaz, Moin Malik, Yi Li, Meng Sun, and M Lali. 2019. A survey on theorem provers in formal methods. arXiv preprint arXiv:1912.03028 (2019)."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.findings-emnlp.232"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3539618.3591796"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Stephen Robertson Hugo Zaragoza et al. 2009. The probabilistic relevance framework: BM25 and beyond. Foundations and Trends\u00ae in Information Retrieval 3 4 (2009) 333-389. doi:10.1561\/1500000019 10.1561\/1500000019","DOI":"10.1561\/1500000019"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.0"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.emnlp-main.372"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2652524.2652551"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/ase56229.2023.00090"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.00161"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464689"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616256"},{"key":"e_1_2_1_60_1","volume-title":"Minilm: Deep self-attention distillation for task-agnostic compression of pre-trained transformers. Advances in neural information processing systems 33","author":"Wang Wenhui","year":"2020","unstructured":"Wenhui Wang, Furu Wei, Li Dong, Hangbo Bao, Nan Yang, and Ming Zhou. 2020. Minilm: Deep self-attention distillation for task-agnostic compression of pre-trained transformers. Advances in neural information processing systems 33 (2020), 5776-5788."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2024.3382361"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Shangyu Wu Ying Xiong Yufei Cui Haolun Wu Can Chen Ye Yuan Lianming Huang Xue Liu Tei-Wei Kuo Nan Guan et al. 2024. Retrieval-augmented generation for natural language processing: A survey. arXiv preprint arXiv:2407.13193 (2024). doi:10.21203\/rs.3.rs-6959723\/v1 10.21203\/rs.3.rs-6959723\/v1","DOI":"10.21203\/rs.3.rs-6959723\/v1"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/esem64174.2025.00038"},{"key":"e_1_2_1_64_1","volume-title":"Approximate nearest neighbor negative contrastive learning for dense text retrieval. arXiv preprint arXiv:2007.00808","author":"Xiong Lee","year":"2020","unstructured":"Lee Xiong, Chenyan Xiong, Ye Li, Kwok-Fung Tang, Jialin Liu, Paul Bennett, Junaid Ahmed, and Arnold Overwijk. 2020. Approximate nearest neighbor negative contrastive learning for dense text retrieval. arXiv preprint arXiv:2007.00808 (2020)."},{"key":"e_1_2_1_65_1","volume-title":"International Conference on Machine Learning. PMLR, 6984-6994","author":"Yang Kaiyu","year":"2019","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning. PMLR, 6984-6994."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.52202\/075280-0944"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/icse55347.2025.00214"},{"key":"e_1_2_1_68_1","volume-title":"Rag-enhanced commit message generation. arXiv preprint arXiv:2406.05514","author":"Zhang Linghao","year":"2024","unstructured":"Linghao Zhang, Hongyi Zhang, Chong Wang, and Peng Liang. 2024. Rag-enhanced commit message generation. arXiv preprint arXiv:2406.05514 (2024)."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","unstructured":"Manqing Zhang Yunwei Dong Lingru Zhou Bingxu Xiao and Yepang Liu. 2025. Replication Package for ProofFusion. https:\/\/doi.org\/10.5281\/zenodo.17096183. 10.5281\/zenodo.17096183","DOI":"10.5281\/zenodo.17096183"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2025.3545970"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3721128"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s41019-025-00335-5"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/cvpr46437"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3797139","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:54:14Z","timestamp":1782845654000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3797139"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,30]]},"references-count":73,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3797139"],"URL":"https:\/\/doi.org\/10.1145\/3797139","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,30]]}}}