{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:01:33Z","timestamp":1754161293021,"version":"3.41.2"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,23]]},"DOI":"10.1145\/3696630.3728705","type":"proceedings-article","created":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:10:43Z","timestamp":1753729843000},"page":"1679-1682","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Proof Generation: Fine-tuning and RAG in Reasoner vs. Math LLMs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0831-2805","authenticated-orcid":false,"given":"Juan Carlos","family":"Recio Abad","sequence":"first","affiliation":[{"name":"University of Malaga, M\u00e1laga, M\u00e1laga, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0944-5941","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Saborido","sequence":"additional","affiliation":[{"name":"University of Malaga, M\u00e1laga, M\u00e1laga, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1259-2990","authenticated-orcid":false,"given":"Francisco","family":"Chicano","sequence":"additional","affiliation":[{"name":"University of Malaga, M\u00e1laga, M\u00e1laga, Spain"}]}],"member":"320","published-online":{"date-parts":[[2025,7,28]]},"reference":[{"volume-title":"Frontiers of Combining Systems, Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.)","author":"Blanchette Jasmin Christian","key":"e_1_3_2_1_1_1","unstructured":"Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. 2011. Automatic Proof and Disproof in Isabelle\/HOL. In Frontiers of Combining Systems, Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 12\u201327."},{"key":"e_1_3_2_1_2_1","unstructured":"DeepSeek-AI Daya Guo and Zhen Zhang. 2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. arXiv:2501.12948 [cs.CL] https:\/\/arxiv.org\/abs\/2501.12948"},{"key":"e_1_3_2_1_3_1","volume-title":"The Faiss library. ArXiv abs\/2401.08281","author":"Douze Matthijs","year":"2024","unstructured":"Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Pierre-Emmanuel Mazar'e, Maria Lomeli, Lucas Hosseini, and Herv'e J'egou. 2024. The Faiss library. ArXiv abs\/2401.08281 (2024). https:\/\/api.semanticscholar.org\/CorpusID:267028372"},{"key":"e_1_3_2_1_4_1","unstructured":"Recio et al. 2025. Dataset with AFP Theories. https:\/\/huggingface.co\/datasets\/jcrecio\/AFP_Theories"},{"key":"e_1_3_2_1_5_1","unstructured":"Recio et al. 2025. Dataset with Generated Theories. https:\/\/huggingface.co\/datasets\/jcrecio\/afp_generated"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","author":"First Emily","year":"2023","unstructured":"Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (San Francisco, CA, USA) (ESEC\/FSE 2023). Association for Computing Machinery, New York, NY, USA, 1229\u20131241. 10.1145\/3611643.3616243"},{"key":"e_1_3_2_1_7_1","volume-title":"Hugging Face: The AI community building the future","author":"Face Hugging","year":"2024","unstructured":"Hugging Face. 2024. Hugging Face: The AI community building the future. Hugging Face Inc. https:\/\/huggingface.co"},{"key":"e_1_3_2_1_8_1","volume-title":"Jesse Michael Han, and Yuhuai Wu","author":"Jiang Albert Q.","year":"2021","unstructured":"Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. PISA: Portal to Isabelle. https:\/\/albertqjiang.github.io\/Portal-to-ISAbelle\/"},{"key":"e_1_3_2_1_9_1","unstructured":"Albert Q. Jiang Alexandre Sablayrolles Arthur Mensch Chris Bamford Devendra Singh Chaplot Diego de las Casas Florian Bressand Gianna Lengyel Guillaume Lample Lucile Saulnier L\u00e9lio Renard Lavaud Marie-Anne Lachaux Pierre Stock Teven Le Scao Thibaut Lavril Thomas Wang Timoth\u00e9e Lacroix and William El Sayed. 2023. Mistral 7B. arXiv:2310.06825 [cs.CL] https:\/\/arxiv.org\/abs\/2310.06825"},{"key":"e_1_3_2_1_10_1","volume-title":"David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra.","author":"Lewkowycz Aitor","year":"2022","unstructured":"Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. 2022. Solving Quantitative Reasoning Problems with Language Models. In Advances in Neural Information Processing Systems, Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (Eds.). https:\/\/openreview.net\/forum?id=IFXTZERXdM7"},{"key":"e_1_3_2_1_11_1","unstructured":"Zehan Li Xin Zhang Yanzhao Zhang Dingkun Long Pengjun Xie and Meishan Zhang. 2023. Towards General Text Embeddings with Multi-stage Contrastive Learning. arXiv:2308.03281 [cs.CL] https:\/\/arxiv.org\/abs\/2308.03281"},{"key":"e_1_3_2_1_12_1","unstructured":"Unsloth AI. [n. d.]. Unsloth Documentation. https:\/\/docs.unsloth.ai\/"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 36th International Conference on Neural Information Processing Systems","author":"Wei Jason","year":"2022","unstructured":"Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Conference on Neural Information Processing Systems (New Orleans, LA, USA) (NIPS '22). Curran Associates Inc., Red Hook, NY, USA, Article 1800, 14 pages."}],"event":{"name":"FSE Companion '25: 33rd ACM International Conference on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Clarion Hotel Trondheim Trondheim Norway","acronym":"FSE Companion '25"},"container-title":["Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696630.3728705","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:13:13Z","timestamp":1753729993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696630.3728705"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":13,"alternative-id":["10.1145\/3696630.3728705","10.1145\/3696630"],"URL":"https:\/\/doi.org\/10.1145\/3696630.3728705","relation":{},"subject":[],"published":{"date-parts":[[2025,6,23]]},"assertion":[{"value":"2025-07-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}