research-article

Open access

Explainable Program Synthesis by Localizing Specifications

Authors:

Amirmohammad Nazari,

Roopsha Samanta,

Arjun Radhakrishna,

Mukund RaghothamanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2

Article No.: 298, Pages 2171 - 2195

https://doi.org/10.1145/3622874

Published: 16 October 2023 Publication History

Abstract

The traditional formulation of the program synthesis problem is to find a program that meets a logical correctness specification. When synthesis is successful, there is a guarantee that the implementation satisfies the specification. Unfortunately, synthesis engines are typically monolithic algorithms, and obscure the correspondence between the specification, implementation and user intent. In contrast, humans often include comments in their code to guide future developers towards the purpose and design of different parts of the codebase. In this paper, we introduce subspecifications as a mechanism to augment the synthesized implementation with explanatory notes of this form. In this model, the user may ask for explanations of different parts of the implementation; the subspecification generated in response is a logical formula that describes the constraints induced on that subexpression by the global specification and surrounding implementation. We develop algorithms to construct and verify subspecifications and investigate their theoretical properties. We perform an experimental evaluation of the subspecification generation procedure, and measure its effectiveness and running time. Finally, we conduct a user study to determine whether subspecifications are useful: we find that subspecifications greatly aid in understanding the global specification, in identifying alternative implementations, and in debugging faulty implementations.

Supplementary Material

Auxiliary Archive (oopslab23main-p769-p-archive.zip)

This appendix contains omitted details, proofs, and a listing of the tasks we used in our user study.

Download
421.13 KB

References

[1]

Agnar Aamodt and Enric Plaza. 2001. Case-Based Reasoning: Foundational Issues, Methodological Variations, and System Approaches. AI Communications, 7 (2001), 39–59. https://doi.org/10.3233/AIC-1994-7104

[2]

Amina Adadi and Mohammed Berrada. 2018. Peeking Inside the Black-Box: A Survey on Explainable Artificial Intelligence (XAI). IEEE Access, 6 (2018), 52138–52160. https://doi.org/10.1109/ACCESS.2018.2870052

[3]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo Martin, Mukund Raghothaman, Sanjit Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Formal Methods in Computer-Aided Design (FMCAD). IEEE, 1–8. https://doi.org/10.1109/FMCAD.2013.6679385

[4]

Rajeev Alur, Loris D’Antoni, Sumit Gulwani, Dileep Kini, and Mahesh Viswanathan. 2013. Automated Grading of DFA Constructions. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI). AAAI Press, 1976–1982. isbn:9781577356332

[5]

Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 319–336. isbn:978-3-662-54577-5

[6]

Solon Barocas, Moritz Hardt, and Arvind Narayanan. 2019. Fairness and Machine Learning: Limitations and Opportunities. fairmlbook.org. http://www.fairmlbook.org

[7]

Rafael Caballero, Adrián Riesco, and Josep Silva. 2017. A Survey of Algorithmic Debugging. Comput. Surveys, 50 (2017), 08, 1–35. https://doi.org/10.1145/3106740

Digital Library

[8]

Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith. 2003. Modular Verification of Software Components in C. In Proceedings of the 25th International Conference on Software Engineering (ICSE). IEEE Computer Society, 385–395. isbn:076951877X

[9]

Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba. 2021. Evaluating Large Language Models Trained on Code. arxiv:2107.03374.

[10]

Finale Doshi-Velez and Been Kim. 2017. Towards A Rigorous Science of Interpretable Machine Learning. https://doi.org/10.48550/ARXIV.1702.08608 arxiv:1702.08608.

[11]

Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, and Joshua Tenenbaum. 2021. DreamCoder: Bootstrapping Inductive Program Synthesis with Wake-Sleep Library Learning. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM, 835–850. isbn:9781450383912 https://doi.org/10.1145/3453483.3454080

Digital Library

[12]

Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. 2018. Program Synthesis Using Conflict-Driven Learning. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 420–435. isbn:9781450356985 https://doi.org/10.1145/3192366.3192382

Digital Library

[13]

Ashley Feniello, Hao Dang, and Stan Birchfield. 2014. Program Synthesis by Examples for Object Repositioning Tasks. In IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). 4428–4435. https://doi.org/10.1109/IROS.2014.6943189

[14]

Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg, Sorin Lerner, and Nadia Polikarpova. 2020. Small-Step Live Programming by Example. In Proceedings of the 33rd Annual ACM Symposium on User Interface Software and Technology (UIST). Association for Computing Machinery, 614–626. isbn:9781450375146 https://doi.org/10.1145/3379337.3415869

Digital Library

[15]

John Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, 229–239. isbn:9781450334686 https://doi.org/10.1145/2737924.2737977

Digital Library

[16]

Bernd Finkbeiner, Gideon Geier, and Noemi Passing. 2021. Specification Decomposition for Reactive Synthesis. In NASA Formal Methods. Springer, 113–130. isbn:978-3-030-76384-8

[17]

Orlena Gotel and Anthony Finkelstein. 1994. An Analysis of the Requirements Traceability Problem. In Proceedings of IEEE International Conference on Requirements Engineering. 94–101. https://doi.org/10.1109/ICRE.1994.292398

[18]

Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-Output Examples. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 317–330. isbn:9781450304900 https://doi.org/10.1145/1926385.1926423

Digital Library

[19]

Shivam Handa and Martin Rinard. 2020. Inductive Program Synthesis over Noisy Data. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC / FSE). ACM, 87–98. isbn:9781450370431

Digital Library

[20]

Susmit Jha, Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari. 2010. Oracle-Guided Component-Based Program Synthesis. In Proceedings of the 32nd International Conference on Software Engineering (ICSE). ACM, 215–224. https://doi.org/10.1145/1806799.1806833

Digital Library

[21]

Amy J. Ko and Brad A. Myers. 2004. Designing the Whyline: A Debugging Interface for Asking Questions About Program Behavior. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI). ACM, 151–158. isbn:1581137028 https://doi.org/10.1145/985692.985712

Digital Library

[22]

Robert Könighofer, Georg Hofferek, and Roderick Bloem. 2009. Debugging Formal Specifications Using Simple Counterstrategies. In 2009 Formal Methods in Computer-Aided Design. 152–159. https://doi.org/10.1109/FMCAD.2009.5351127

[23]

Manos Koukoutos, Etienne Kneuss, and Viktor Kuncak. 2016. An Update on Deductive Synthesis and Repair in the Leon Tool. In Proceedings Fifth Workshop on Synthesis (SYNT@CAV, Vol. 229). 100–111. https://doi.org/10.4204/EPTCS.229.9

[24]

Orna Kupferman and Moshe Vardi. 2003. Vacuity Detection in Temporal Model Checking. International Journal on Software Tools for Technology Transfer, 4, 2 (2003), Feb., 224–233. issn:1433-2779 https://doi.org/10.1007/s100090100062

[25]

Vu Le and Sumit Gulwani. 2014. FlashExtract: A Framework for Data Extraction by Examples. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 542–553. isbn:9781450327848 https://doi.org/10.1145/2594291.2594333

Digital Library

[26]

Mikaël Mayer, Gustavo Soares, Maxim Grechkin, Vu Le, Mark Marron, Oleksandr Polozov, Rishabh Singh, Benjamin Zorn, and Sumit Gulwani. 2015. User Interaction Models for Disambiguation in Programming by Example. In Proceedings of the 28th Annual ACM Symposium on User Interface Software and Technology (UIST). ACM, 291–301. isbn:9781450337793 https://doi.org/10.1145/2807442.2807459

Digital Library

[27]

Alex Mott, Daniel Zoran, Mike Chrzanowski, Daan Wierstra, and Danilo Rezende. 2019. Towards Interpretable Reinforcement Learning Using Attention Augmented Agents. In Proceedings of the 33rd International Conference on Neural Information Processing Systems (NeurIPS). Article 1107, 10 pages.

[28]

Steven Muchnick. 1998. Advanced Compiler Design and Implementation. Morgan Kaufmann. isbn:1558603204

[29]

Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, and Mukund Raghothaman. 2023. Explainable Program Synthesis by Localizing Specifications. https://doi.org/10.5281/zenodo.8331495

Digital Library

[30]

OpenAI. 2022. ChatGPT. https://openai.com/blog/chatgpt/

[31]

Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 619–630. isbn:9781450334686 https://doi.org/10.1145/2737924.2738007

Digital Library

[32]

Hila Peleg, Sharon Shoham, and Eran Yahav. 2018. Programming Not Only by Example. In Proceedings of the 40th International Conference on Software Engineering (ICSE). ACM, 1114–1124. isbn:9781450356381 https://doi.org/10.1145/3180155.3180189

Digital Library

[33]

Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 522–538. isbn:9781450342612 https://doi.org/10.1145/2908080.2908093

Digital Library

[34]

Nadia Polikarpova and Ilya Sergey. 2019. Structuring the Synthesis of Heap-Manipulating Programs. Proceedings of the ACM on Programming Languages, 3, POPL (2019), Article 72, Jan., 30 pages. https://doi.org/10.1145/3290385

Digital Library

[35]

Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In Computer Aided Verification (CAV). Springer, 198–216. isbn:978-3-319-21668-3

[36]

Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. 2016. Model-Agnostic Interpretability of Machine Learning. https://doi.org/10.48550/ARXIV.1606.05386

[37]

Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. 2016. “Why Should I Trust You?”: Explaining the Predictions of Any Classifier. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD). ACM, 1135–1144. isbn:9781450342322 https://doi.org/10.1145/2939672.2939778

Digital Library

[38]

Lei Shi, Yahui Li, Boon Thau Loo, and Rajeev Alur. 2021. Network Traffic Classification by Program Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 430–448. isbn:978-3-030-72016-2

[39]

Rishabh Singh. 2016. BlinkFill: Semi-Supervised Programming by Example for Syntactic String Transformations. Proceedings of the VLDB Endowment, 9, 10 (2016), June, 816–827. issn:2150-8097 https://doi.org/10.14778/2977797.2977807

Digital Library

[40]

Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama. 2013. Automated Feedback Generation for Introductory Programming Assignments. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 15–26. isbn:9781450320146 https://doi.org/10.1145/2491956.2462195

Digital Library

[41]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM, 404–415. isbn:1595934510 https://doi.org/10.1145/1168857.1168907

Digital Library

[42]

Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani, and Daniel Perelman. 2020. Information-theoretic User Interaction: Significant Inputs for Program Synthesis. CoRR, abs/2006.12638 (2020), arXiv:2006.12638. arxiv:2006.12638

[43]

Chenglong Wang, Yu Feng, Rastislav Bodik, Isil Dillig, Alvin Cheung, and Amy Ko. 2021. Falx: Synthesis-Powered Visualization Authoring. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems (CHI). ACM, Article 106, 15 pages. isbn:9781450380966 https://doi.org/10.1145/3411764.3445249

Digital Library

[44]

Zijie Wang, Robert Turko, Omar Shaikh, Haekyu Park, Nilaksh Das, Fred Hohman, Minsuk Kahng, and Duen Horng Polo Chau. 2021. CNN Explainer: Learning Convolutional Neural Networks with Interactive Visualization. IEEE Transactions on Visualization and Computer Graphics, 27, 2 (2021), Feb., 1396–1406. issn:2160-9306 https://doi.org/10.1109/tvcg.2020.3030418

[45]

Mark Weiser. 1981. Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE). IEEE Press, 439–449. isbn:0897911466

[46]

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and Extensible Equality Saturation. Proceedings of the ACM on Programming Languages, 5, POPL (2021), Article 23, Jan., 29 pages. https://doi.org/10.1145/3434304

Digital Library

[47]

Andreas Zeller. 1999. Yesterday, My Program Worked. Today, It Does Not. Why? In Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE). Springer, 253–267. isbn:3540665382

[48]

Tianyi Zhang, Zhiyang Chen, Yuanli Zhu, Priyan Vaithilingam, Xinyu Wang, and Elena Glassman. 2021. Interpretable Program Synthesis. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems. ACM, 16 pages. isbn:9781450380966

Digital Library

[49]

Tianyi Zhang, London Lowmanstone, Xinyu Wang, and Elena Glassman. 2020. Interactive Program Synthesis by Augmented Examples. In Proceedings of the 33rd Annual ACM Symposium on User Interface Software and Technology (UIST). 627–648. isbn:9781450375146 https://doi.org/10.1145/3379337.3415900

Digital Library

[50]

Bolei Zhou, Aditya Khosla, Àgata Lapedriza, Aude Oliva, and Antonio Torralba. 2016. Learning Deep Features for Discriminative Localization. In 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR). IEEE Computer Society, 2921–2929. issn:1063-6919 https://doi.org/10.1109/CVPR.2016.319

Cited By

Nazari AZhang YRaghothaman MChen H(2024)Localized Explanations for Automatically Synthesized Network ConfigurationsProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696888(52-59)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696888
Chen H(2024)Interpretable Network Synthesis via Localized SpecificationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673889(51-53)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673889
Naghiaei MDehghan MRahmani HAzizi JAliannejadi MOosterhuis HBast HXiong C(2024)Personalized Beyond-accuracy Calibration in RecommendationProceedings of the 2024 ACM SIGIR International Conference on Theory of Information Retrieval10.1145/3664190.3672507(107-116)Online publication date: 2-Aug-2024
https://dl.acm.org/doi/10.1145/3664190.3672507
Show More Cited By

Index Terms

Explainable Program Synthesis by Localizing Specifications
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
  2. Software notations and tools
    1. General programming languages
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Algorithmic program synthesis: introduction

Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of ...
Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...
Program synthesis by model finding

Program synthesis aims to automate the task of programming. In this paper, we present a clear and elegant formulation of program synthesis as an Alloy* specification by applying its model finder to search for a program that satisfies a contract in terms ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue OOPSLA2

October 2023

2250 pages

EISSN:2475-1421

DOI:10.1145/3554312

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 October 2023

Published in PACMPL Volume 7, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
679
Total Downloads

Downloads (Last 12 months)517
Downloads (Last 6 weeks)79

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nazari AZhang YRaghothaman MChen H(2024)Localized Explanations for Automatically Synthesized Network ConfigurationsProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696888(52-59)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696888
Chen H(2024)Interpretable Network Synthesis via Localized SpecificationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673889(51-53)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673889
Naghiaei MDehghan MRahmani HAzizi JAliannejadi MOosterhuis HBast HXiong C(2024)Personalized Beyond-accuracy Calibration in RecommendationProceedings of the 2024 ACM SIGIR International Conference on Theory of Information Retrieval10.1145/3664190.3672507(107-116)Online publication date: 2-Aug-2024
https://dl.acm.org/doi/10.1145/3664190.3672507
Nazari ASwayamdipta SChattopadhyay SRaghothaman M(2024)Generating Function Names to Improve Comprehension of Synthesized Programs2024 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)10.1109/VL/HCC60511.2024.00035(248-259)Online publication date: 2-Sep-2024
https://doi.org/10.1109/VL/HCC60511.2024.00035
Wang SBulitko VYeoh W(2024)Explaining Synthesized Pathfinding Heuristics via Iterative Visualization and Modification2024 IEEE Conference on Games (CoG)10.1109/CoG60054.2024.10645663(1-4)Online publication date: 5-Aug-2024
https://doi.org/10.1109/CoG60054.2024.10645663

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents