{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T09:12:37Z","timestamp":1784106757597,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T00:00:00Z","timestamp":1783209600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,7,5]]},"DOI":"10.1145\/3805760.3814906","type":"proceedings-article","created":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T08:46:13Z","timestamp":1783241173000},"page":"160-167","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["VeriTrans: Fine-Tuned LLM-Assisted NL\u2192PL Translation via a Deterministic Neuro-symbolic Pipeline"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7767-2983","authenticated-orcid":false,"given":"Xuan","family":"Liu","sequence":"first","affiliation":[{"name":"Pennsylvania State University, University Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0182-9000","authenticated-orcid":false,"given":"Dheeraj","family":"Kodakandla","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, University Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8778-5184","authenticated-orcid":false,"given":"Kushagra","family":"Srivastva","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, University Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1754-4524","authenticated-orcid":false,"given":"Mahfuza","family":"Farooque","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, University Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"A. Beg et al. 2025. Leveraging LLMs for Formal Software Requirements. arXiv preprint arXiv:2507.14330 (2025). doi:10.48550\/arXiv.2507.14330 10.48550\/arXiv.2507.14330","DOI":"10.48550\/arXiv.2507.14330"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2025.1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2507.00877"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Alessio Ferrari et al. 2025. Formal Requirements Engineering and Large Language Models: Opportunities and Challenges. Information and Software Technology (2025). doi:10.1016\/j.infsof.2025.107697 10.1016\/j.infsof.2025.107697","DOI":"10.1016\/j.infsof.2025.107697"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Francesco Fuggitti et al. 2023. NL2LTL: A Python Package for Converting Natural Language Instructions to Linear Temporal Logic. In AAAI 2023 (Demo Track). doi:10.1609\/aaai.v37i13.27068 10.1609\/aaai.v37i13.27068","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.emnlp-main.1229"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2025"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"S. Hazra et al. 2025. SATQuest: A Verifier for Logical Reasoning Evaluation and Benchmarks. arXiv preprint arXiv:2509.00930 (2025). doi:10.48550\/arXiv.2509.00 930 10.48550\/arXiv.2509.00930","DOI":"10.48550\/arXiv.2509.00"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.196"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3703155"},{"key":"e_1_3_2_1_11_1","volume-title":"ALTA 2024","author":"Marcus Lok Hin","year":"2024","unstructured":"Lok Hin Marcus Lam et al. 2024. A Closer Look at Tool-based Logical Reasoning with LLMs. In ALTA 2024. https:\/\/aclanthology.org\/2024.alta-1.4.pdf"},{"key":"e_1_3_2_1_12_1","volume-title":"FVEL: Interactive Formal Verification Environment with Large Language Models. In NeurIPS","author":"Xuefeng Lin","year":"2024","unstructured":"Xuefeng Lin et al. 2024. FVEL: Interactive Formal Verification Environment with Large Language Models. In NeurIPS 2024."},{"key":"e_1_3_2_1_13_1","volume-title":"P-FOLIO: Evaluating and Improving Logical Reasoning with First-Order Logic Proofs. arXiv preprint arXiv:2410.09207","author":"Liu Yixin","year":"2024","unstructured":"Yixin Liu, Shiyu Han, Tianyu Zhang, Xiang Ren, and He He. 2024. P-FOLIO: Evaluating and Improving Logical Reasoning with First-Order Logic Proofs. arXiv preprint arXiv:2410.09207 (2024)."},{"key":"e_1_3_2_1_14_1","unstructured":"Ricardo Mendoza Caroline Trippel et al. 2024. Translating Natural Language to Temporal Logics with Large Language Models. In Formal Methods in Computer- Aided Design (FMCAD)."},{"key":"e_1_3_2_1_15_1","unstructured":"OpenAI. 2025. OpenAI Fine-Tuning API Documentation. https:\/\/platform.opena i.com\/docs\/guides\/fine-tuning."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2305.12295"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISNCC66965.2025.11250432"},{"key":"e_1_3_2_1_18_1","volume-title":"Large Language Models Meet Symbolic Solvers for Faithful Logical Reasoning. In ICLR","author":"Qi Chen","year":"2025","unstructured":"Chen Qi, Xinyu Zhang, Jiayi Guo, and Dongxu Han. 2025. Large Language Models Meet Symbolic Solvers for Faithful Logical Reasoning. In ICLR 2025."},{"key":"e_1_3_2_1_19_1","volume-title":"HotOS","author":"Qin Jianxing","year":"2025","unstructured":"Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Dapeng Zhuo. 2025. Can Large Language Models Verify System Software?. In HotOS 2025."},{"key":"e_1_3_2_1_20_1","volume-title":"Divide and Translate: Compositional First-Order Logic Translation and Verification. In ICLR","author":"Ryu Hyun","year":"2025","unstructured":"Hyun Ryu, Gyeongman Kim, Hyemin S. Lee, and Eunho Yang. 2025. Divide and Translate: Compositional First-Order Logic Translation and Verification. In ICLR 2025."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-NIER66352.2025.0"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2509.22338"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"J. Wang et al. 2025. ConformalNL2LTL: Uncertainty-Aware Natural Language to Temporal Logic Translation with Large Language Models. arXiv preprint arXiv:2504.21022 (2025). doi:10.48550\/arXiv.2504.21022 10.48550\/arXiv.2504.21022","DOI":"10.48550\/arXiv.2504.21022"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2510.10703"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2505.14615"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2201.11903"},{"key":"e_1_3_2_1_27_1","volume-title":"NeurIPS","author":"Wu Yuhuai","year":"2022","unstructured":"Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with Large Language Models. In NeurIPS 2022."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acl-long.720"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Kexun Yang et al. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In NeurIPS 2023.","DOI":"10.52202\/075280-0944"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acllong.375"},{"key":"e_1_3_2_1_31_1","volume-title":"NeurIPS","author":"Ye Xi","year":"2023","unstructured":"Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. SatLM: Satisfiability- Aided Language Models Using Declarative Prompting. In NeurIPS 2023."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Tong Zheng Lichang Chen Simeng Han R. Thomas McCoy and Heng Huang. 2025. Learning to Reason via Mixture-of-Thought for Logical Reasoning. arXiv:2505.15817 [cs.CL] doi:10.48550\/arXiv.2505.15817 10.48550\/arXiv.2505.15817","DOI":"10.48550\/arXiv.2505.15817"}],"event":{"name":"AIware '26: 3rd ACM International Conference on AI-Powered Software","location":"Montreal QC Canada","acronym":"AIware '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 3rd ACM International Conference on AI-Powered Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3805760.3814906","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T08:51:01Z","timestamp":1783241461000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3805760.3814906"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,5]]},"references-count":32,"alternative-id":["10.1145\/3805760.3814906","10.1145\/3805760"],"URL":"https:\/\/doi.org\/10.1145\/3805760.3814906","relation":{},"subject":[],"published":{"date-parts":[[2026,7,5]]},"assertion":[{"value":"2026-07-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}