乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:47:58Z","timestamp":1743119278767,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031737404"},{"type":"electronic","value":"9783031737411"}],"license":[{"start":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T00:00:00Z","timestamp":1730332800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T00:00:00Z","timestamp":1730332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>We demonstrate how LLMs can be harnessed to synthesize runtime verification monitors from natural language specifications. We instruct the LLM through prompts to assemble the monitors through a sequence of stages. To start with, we employ the learned insights LLMs possess regarding linear temporal logic for translating natural language specifications into propositional past time LTL formulas. Next, we utilize a sequence of prompts to synthesize from the LTL specification a runtime verification monitor for the given formula. Part of these prompts enable the LLM to validate its own outputs, thereby significantly improving the probability of obtaining a correct monitor.<\/jats:p>","DOI":"10.1007\/978-3-031-73741-1_23","type":"book-chapter","created":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:54:58Z","timestamp":1730300098000},"page":"362-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["End-to-End AI Generated Runtime Verification from\u00a0Natural Language Specification"],"prefix":"10.1007","author":[{"given":"Itay","family":"Cohen","sequence":"first","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,31]]},"reference":[{"issue":"3","key":"23_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"23_CR2","unstructured":"Anil, R., et\u00a0al.: Gemini: a family of highly capable multimodal models. CoRR abs\/2312.11805 (2023)"},{"issue":"3","key":"23_CR3","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. J. Log. Comput. 20(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015). https:\/\/doi.org\/10.1145\/2699444","DOI":"10.1145\/2699444"},{"key":"23_CR6","unstructured":"Brown, T.B., et al.: Language models are few-shot learners. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, 6\u201312 December 2020, virtual (2020)"},{"key":"23_CR7","unstructured":"Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL formulas from natural language texts: State of the art and research directions. In: Gamper, J., Pinchinat, S., Sciavicco, G. (eds.) 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, 16\u201319 October 2019, M\u00e1laga, Spain. LIPIcs, vol.\u00a0147, pp. 17:1\u201317:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"23_CR8","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, 1st Edition. MIT Press, Cambridge (2001). http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC"},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, LNCS, vol. 13965, pp. 383\u2013396. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pp. 166\u2013174. IEEE Computer Society (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL - a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: Williams, B., Chen, Y., Neville, J. (eds.) Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, 7\u201314 February 2023, pp. 16428\u201316430. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"23_CR12","unstructured":"Hahn, C., Schmitt, F., Tillman, J.J., Metzger, N., Siber, J., Finkbeiner, B.: Formal specifications from natural language. CoRR abs\/2206.01962 (2022)"},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 56(1), 1\u201321 (2020). https:\/\/doi.org\/10.1007\/S10703-018-00327-4","DOI":"10.1007\/S10703-018-00327-4"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"23_CR15","unstructured":"Jiang, A.Q., et al.: Mistral 7b. CoRR abs\/2310.06825 (2023)"},{"issue":"5","key":"23_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Methods Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"23_CR17","unstructured":"Liu, J.X., Yang, Z., Idrees, I., Liang, S., Schornstein, B., Tellex, S., Shah, A.: Grounding complex natural language commands for temporal tasks in unseen environments. In: Tan, J., Toussaint, M., Darvish, K. (eds.) Conference on Robot Learning, CoRL 2023, 6-9 November 2023, Atlanta, GA, USA. Proceedings of Machine Learning Research, vol.\u00a0229, pp. 1084\u20131110. PMLR (2023)"},{"key":"23_CR18","unstructured":"Radford, A., Narasimhan, K., Salimans, T., Sutskever, I., et\u00a0al.: Improving language understanding by generative pre-training. OpenAI (2018)"},{"key":"23_CR19","unstructured":"Tan, C.W., Guo, S., Wong, M., Hang, C.N.: Copilot for xcode: exploring AI-assisted programming by prompting cloud-based large language models. CoRR abs\/2307.14349 (2023)"},{"key":"23_CR20","unstructured":"Touvron, H., et al.: Llama: open and efficient foundation language models. CoRR abs\/2302.13971 (2023)"},{"key":"23_CR21","unstructured":"Vaswani, A., et al.: Attention is all you need. In: Guyon, I., et al. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4\u20139 December 2017, Long Beach, CA, USA, pp. 5998\u20136008 (2017)"},{"key":"23_CR22","unstructured":"Wang, C., Ross, C., Kuo, Y., Katz, B., Barbu, A.: Learning a natural-language to LTL executable semantic parser for grounded robotics. In: Kober, J., Ramos, F., Tomlin, C.J. (eds.) 4th Conference on Robot Learning, CoRL 2020, 16\u201318 November 2020, Virtual Event\/Cambridge, MA, USA. Proceedings of Machine Learning Research, vol.\u00a0155, pp. 1706\u20131718. PMLR (2020)"}],"container-title":["Lecture Notes in Computer Science","Bridging the Gap Between AI and Reality"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73741-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T15:01:36Z","timestamp":1730300496000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73741-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,31]]},"ISBN":["9783031737404","9783031737411"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73741-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,31]]},"assertion":[{"value":"31 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Bridging the Gap between AI and Reality","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aisola2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2023-aisola.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}