short-paper

Neuro-Symbolic Approach to Certified Scientific Software Synthesis

Authors:

Mehdi Mirakhorli,

Mohamad Fazelnia,

Ibrahim Mujhid,

Md Rashedul HasanAuthors Info & Claims

AIware 2024: Proceedings of the 1st ACM International Conference on AI-Powered Software

Pages 147 - 150

https://doi.org/10.1145/3664646.3664776

Published: 10 July 2024 Publication History

Abstract

Scientific software development demands robust solutions to meet the complexities of modern scientific systems. In response, we propose a paradigm-shifting Neuro-Symbolic Approach to Certified Scientific Software Synthesis. This innovative framework integrates large language models (LLMs) with formal methods, facilitating automated synthesis of complex scientific software while ensuring verifiability and correctness. Through a combination of technologies including a Scientific and Satisfiability-Aided Large Language Model (SaSLLM), a Scientific Domain Specific Language (DSL), and Generalized Planning for Abstract Reasoning, our approach transforms scientific concepts into certified software solutions. By leveraging advanced reasoning techniques, our framework streamlines the development process, allowing scientists to focus on design and exploration. This approach represents a significant step towards automated, certified-by-design scientific software synthesis, revolutionizing the landscape of scientific research and discovery.

References

[1]

[n. d.]. DOE Workshop report: The 2015 Cybersecurity for Scientific Computing Integrity-Research Pathways and Ideas Workshop. https://science.energy.gov/~{}/media/ascr/pdf/programdocuments/docs/ ASCR_Cybersecurity_20_Research_Pathways_and_Ideas_Workshop.pdf. Accessed: 2019-04-28.

[2]

Dalal Alrajeh, Jef Kramer, Alessandra Russo, and Sebastin Uchitel. 2009. Learning operational requirements from goal models. In Proceedings of the 31st International Conference on Software Engineering (ICSE '09). IEEE Computer Society, USA, 265-275. https://doi.org/10.1109/ICSE. 2009.5070527

Digital Library

[3]

Rizwan A. Ashraf, Saurabh Hukerikar, and Christian Engelmann. 2018. Patternbased Modeling of Multiresilience Solutions for High-Performance Computing. In Proceedings of the 2018 ACM/SPEC International Conference on Performance Engineering, ICPE 2018, Berlin, Germany, April 09-13, 2018. 80-87. https://doi.org/ 10.1145/3184407.3184421

Digital Library

[4]

Hamid Bagheri, Eunsuk Kang, and Niloofar Mansoor. 2020. Synthesis of assurance cases for software certification. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results (Seoul, South Korea) (ICSE-NIER '20). Association for Computing Machinery, New York, NY, USA, 61-64. https://doi.org/10.1145/3377816.3381728

Digital Library

[5]

David E. Bernholdt, Benjamin A. Allan, Robert C. Armstrong, Felipe Bertrand, Kenneth Chiu, Tamara Dahlgren, Kostadin Damevski, Wael R. Elwasif, Thomas Epperly, Madhusudhan Govindaraju, Daniel S. Katz, James Arthur Kohl, Manojkumar Krishnan, Gary Kumfert, Jay Walter Larson, Sophia Lefantzi, Michael J. Lewis, Allen D. Malony, Lois C. McInnes, Jarek Nieplocha, Boyana Norris, Steven G. Parker, Jaideep Ray, Sameer Shende, Theresa L. Windus, and Shujia Zhou. 2006. A Component Architecture for High-Performance Scientific Computing. IJHPCA 20, 2 ( 2006 ), 163-202. https://doi.org/10.1177/1094342006064488

Digital Library

[6]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Eficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 4963 ), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, 337-340. https://doi.org/ 10.1007/978-3-540-78800-3_24

[7]

Anshu Dubey and Lois Curfman McInnes. 2017. Proposal for a Scientific Software Lifecycle Model. In Proceedings of the 1st International Workshop on Software Engineering for High Performance Computing in Computational and Data-enabled Science & Engineering (Denver, CO, USA) ( SE-CoDeSE'17). ACM, New York, NY, USA, 22-26. https://doi.org/10.1145/3144763.3144767

Digital Library

[8]

Zhiyu Fan, Xiang Gao, Martin Mirchev, Abhik Roychoudhury, and Shin Hwei Tan. 2023. Automated repair of programs from large language models. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 1469-1481.

Digital Library

[9]

Wolfgang Frings, Dong H. Ahn, Matthew LeGendre, Todd Gamblin, Bronis R. de Supinski, and Felix Wolf. 2013. Massively Parallel Loading. In Proceedings of the 27th International ACM Conference on International Conference on Supercomputing (Eugene, Oregon, USA) ( ICS '13). ACM, New York, NY, USA, 389-398. https: //doi.org/10.1145/2464996.2465020

Digital Library

[10]

Todd Gamblin, Matthew LeGendre, Michael R. Collette, Gregory L. Lee, Adam Moody, Bronis R. de Supinski, and Scott Futral. 2015. The Spack Package Manager: Bringing Order to HPC Software Chaos. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (Austin, Texas) (SC '15). ACM, New York, NY, USA, Article 40, 12 pages. https://doi.org/10.1145/2807591.2807623

Digital Library

[11]

Dimitra Giannakopoulou, Corina S. P "s"reanu, and Howard Barringer. 2002. Assumption Generation for Software Component Verification. In Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE '02). IEEE Computer Society, USA, 3.

Digital Library

[12]

Michael A. Heroux. 2009. Software Challenges for Extreme Scale Computing: Going From Petascale to Exascale Systems. The International Journal of High Performance Computing Applications 23, 4 ( 2009 ), 437-439. https://doi.org/10. 1177/1094342009347711 arXiv:https://doi.org/10.1177/1094342009347711

Digital Library

[13]

Sheng-Kuei Hsu and Shi-Jen Lin. 2011. MACs: Mining API code snippets for code reuse. Expert Systems with Applications 38, 6 ( 2011 ).

[14]

Saurabh Hukerikar and Christian Engelmann. 2017. Resilience Design Patterns: A Structured Approach to Resilience at Extreme Scale. CoRR abs/1708.07422 ( 2017 ). arXiv: 1708.07422 http://arxiv.org/abs/1708.07422

[15]

Jinseong Jeon, Xiaokang Qiu, Jefrey S. Foster, and Armando Solar-Lezama. 2015. JSketch: sketching for Java. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30-September 4, 2015. 934-937. https://doi.org/10.1145/2786805.2803189

Digital Library

[16]

D. S. Katz, L. C. McInnes, D. E. Bernholdt, A. C. Mayes, N. P. C. Hong, J. Duckles, S. Gesing, M. A. Heroux, S. Hettrick, R. C. Jimenez, M. Pierce, B. Weaver, and N. Wilkins-Diehr. 2019. Community Organizations: Changing the Culture in Which Research Software Is Developed and Sustained. Computing in Science Engineering 21, 2 (March 2019 ), 8-24. https://doi.org/10.1109/ MCSE. 2018.2883051

Digital Library

[17]

T. Kelly and R. Weaver. 2004. The Goal Structuring Notation-A Safety Argument Notation. In Dependable Systems and Networks (DSN) Workshop on Assurance Cases.

[18]

Chao Lei, Nir Lipovetzky, and Krista A. Ehinger. 2024. Generalized Planning for the Abstraction and Reasoning Corpus. arXiv: 2401.07426 [cs.AI]

[19]

Patrick S. et al. McCormic. 2014. Exploring the Construction of a DomainAware Toolchain for High-Performance Computing. In 2014 Fourth International Workshop on Domain-Specific Languages and High-Level Frameworks for High Performance Computing. 1-10.

[20]

J. P. Near, A. Milicevic, E. Kang, and D. Jackson. 2011. A Lightweight Code Analysis and Its Role in Evaluation of a Dependability Case. In ICSE. ACM, 31-40.

[21]

S. Pernsteiner, C. Loncaric, E. Torlak, Z. Tatlock, X. Wang, M. D. Ernst, and J. Jacky. 2016. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. In Proceedings of CAV. 23-41.

[22]

Rui Qiu, Corina S. Pasareanu, and Sarfraz Khurshid. 2016. Certified Symbolic Execution. In Automated Technology for Verification and Analysis-14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9938 ), Cyrille Artho, Axel Legay, and Doron Peled (Eds.). 495-511. https://doi.org/10.1007/978-3-319-46520-3_31

[23]

Armando Solar-Lezama. 2009. The Sketching Approach to Program Synthesis. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (Seoul, Korea) ( APLAS '09). Springer-Verlag, Berlin, Heidelberg, 4-13. https: //doi.org/10.1007/978-3-642-10672-9_3

Digital Library

[24]

Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, and Jefrey S. Foster. 2011. Path-based Inductive Synthesis for Program Inversion. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (San Jose, California, USA) ( PLDI '11). ACM, New York, NY, USA, 492-503. https://doi.org/10.1145/1993498.1993557

Digital Library

[25]

U.S. Food and Drug Administration (FDA). [n. d.]. List of Device Recalls. https: //www.fda.gov/medicaldevices/safety/listofrecalls. Accessed: 2018-11-14.

[26]

U.S. Food and Drug Administration (FDA). 2017. General principles of software validation; final guidance for industry and FDA staf. https://www.fda.gov/ downloads/medicaldevices/.../ucm085371.pdf.

[27]

Hao Yu, Bo Shen, Dezhi Ran, Jiaxin Zhang, Qi Zhang, Yuchi Ma, Guangtai Liang, Ying Li, Qianxiang Wang, and Tao Xie. 2024. CoderEval: A Benchmark of Pragmatic Code Generation with Generative Pre-trained Models. In Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, ICSE 2024, Lisbon, Portugal, April 14-20, 2024. ACM, 37 : 1-37 : 12. https: //doi.org/10.1145/3597503.3623316

Digital Library

Cited By

Fazelnia MMirakhorli MBagheri HFilkov VRay BZhou M(2024)Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting RequirementsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695302(2294-2298)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695302

Index Terms

Neuro-Symbolic Approach to Certified Scientific Software Synthesis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

AIware 2024: Proceedings of the 1st ACM International Conference on AI-Powered Software

July 2024

182 pages

ISBN:9798400706851

DOI:10.1145/3664646

General Chairs:
Bram Adams
Queen’s University, Canada
,
Thomas Zimmermann
Microsoft Research, USA
,
Ipek Ozkaya
Carnegie Mellon University, USA
,
Program Chairs:
Dayi Lin
Huawei, Canada
,
Jie M. Zhang
King’s College London, United Kingdom

Copyright © 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 July 2024

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Funding Sources

NSF (National Science Foundation)

Conference

AIware '24

Sponsor:

SIGSOFT

AIware '24: 1st ACM International Conference on AI-Powered Software

July 15 - 16, 2024

Porto de Galinhas, Brazil

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
53
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)14

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Fazelnia MMirakhorli MBagheri HFilkov VRay BZhou M(2024)Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting RequirementsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695302(2294-2298)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695302

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents