research-article

Counterexample-driven genetic programming

Authors:

Krzysztof Krawiec,

Jerry SwanAuthors Info & Claims

GECCO '17: Proceedings of the Genetic and Evolutionary Computation Conference

Pages 953 - 960

https://doi.org/10.1145/3071178.3071224

Published: 01 July 2017 Publication History

Abstract

Genetic programming is an effective technique for inductive synthesis of programs from training examples of desired input-output behavior (tests). Programs synthesized in this way are not guaranteed to generalize beyond the training set, which is unacceptable in many applications. We present Counterexample-Driven Genetic Programming (CDGP) that employs evolutionary search to synthesize provably correct programs from formal specifications. CDGP employs a Satisfiability Modulo Theories (SMT) solver to formally verify programs in the evaluation phase. A failed verification produces counterexamples that are in turn used to calculate fitness and so drive the search process. When compared against a range of approaches on a suite of state-of-the-art specification-based synthesis benchmarks, CDGP systematically outperforms them, typically synthesizing correct programs faster and using fewer tests.

References

[1]

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. 2011. An Overview of Formal Methods Tools and Techniques. Springer London, London, 15--44.

[2]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit Seshia, Rajdeep Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013. IEEE, 1--8.

[3]

Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. 2015. Results and Analysis of SyGuS-Comp'15. In Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015. 3--26.

[4]

Andrea Arcuri and Xin Yao. 2007. Coevolving Programs and Unit Tests from Their Specification. In Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering (ASE '07). ACM, New York, NY, USA, 397--400.

Digital Library

[5]

Andrea Arcuri and Xin Yao. 2014. Co-evolutionary Automatic Programming for Software Development. Inf. Sci. 259 (Feb. 2014), 412--432.

Digital Library

[6]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2015. The SMT-LIB Standard: Version 2.5. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.

[7]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. (2016).

[8]

Dines Bjørner and Cliff B. Jones (Eds.). 1978. The Vienna Development Method: The Meta-Language. Springer-Verlag, London, UK, UK.

[9]

Paul P. Boca, Jonathan P. Bowen, and Jawed I Siddiqi. 2009. Formal Methods: State of the Art and New Directions (1st ed.). Springer Publishing Company, Incorporated.

Digital Library

[10]

Nathan Buries, Edward Bowles, Alexander E. I. Brownlee, Zoltan A. Kocsis, Jerry Swan, and Nadarajen Veerapen. 2015. Search-Based Software Engineering: 7th International Symposium, SSBSE 2015, Bergamo, Italy, September 5--7, 2015, Proceedings. Springer International Publishing, Cham, Chapter Object-Oriented Genetic Improvement for Improved Energy Consumption in Google Guava, 255--261.

[11]

Iwo Błądek and Krzysztof Krawiec. 2017. Evolutionary Program Sketching. Springer International Publishing, Cham, 3--18.

[12]

A. Cavalcanti, A. Sampaio, and J. Woodcock. 2006. Refinement Techniques in Software Engineering: First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures. Springer Berlin Heidelberg, https://books.google.co.in/books?id=aa1qCQAAQBAJ

Digital Library

[13]

B Cohen. 1994. A Brief History of Formal Methods. Formal Aspects of Computing 1, 3 (1994).

[14]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. Ramakrishnan and Jakob Rehof (Eds.). Lecture Notes in Computer Science, Vol. 4963. Springer Berlin / Heidelberg, Berlin, Heidelberg, Chapter 24, 337--340.

Digital Library

[15]

Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2010. Component Based Synthesis Applied to Bitvector Programs. Technical Report MSR-TR-2010-12. http://research.microsoft.com/apps/pubs/default.aspx?id=119146

[16]

John V. Guttag and James J. Horning. 1993. Larch: Languages and Tools for Formal Specification. Springer-Verlag New York, Inc., New York, NY, USA.

Digital Library

[17]

Mark Harman, Yue Jia, and William B. Langdon. 2014. Babel Pidgin: SBSE Can Grow and Graft Entirely New Functionality into a Real World System. Springer International Publishing, Cham, 247--252.

[18]

Thomas Helmuth, Lee Spector, and James Matheson. 2015. Solving Uncompromising Problems with Lexicase Selection. IEEE Transactions on Evolutionary Computation 19, 5 (Oct. 2015), 630--643.

Digital Library

[19]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (Oct. 1969), 576--580.

Digital Library

[20]

Martin Hofmann. 2010. Igor II - an analytical inductive functional programming system. In In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. 29--32.

Digital Library

[21]

Martin Hofmann, Emanuel Kitzelmann, and Ute Schmid. 2008. Analysis and Evaluation of Inductive Programming Systems in a Higher-Order Framework. In Proceedings of the 31st Annual German Conference on Advances in Artificial Intelligence (KI '08). Springer-Verlag, Berlin, Heidelberg, 78--86.

Digital Library

[22]

Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. 2010. Oracle-guided component-based program synthesis. In 29th International Conference on Software Engineering (ICSE '10). 215--224.

Digital Library

[23]

Colin Johnson. 2007. Genetic Programming with Fitness based on Model Checking. In Proceedings of the 10th European Conference on Genetic Programming (Lecture Notes in Computer Science), Marc Ebner, Michael O'Neill, Anikó Ekárt, Leonardo Vanneschi, and Anna Isabel Esparcia-Alcázar (Eds.), Vol. 4445. Springer, Valencia, Spain, 114--124.

Digital Library

[24]

Susumu Katayama. 2012. An Analytical Inductive Functional Programming System That Avoids Unintended Programs. In Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM '12). ACM, New York, NY, USA, 43--52.

Digital Library

[25]

Gal Katz and Doron Peled. 2008. Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms. Springer Berlin Heidelberg, Berlin, Heidelberg, 33--47.

Digital Library

[26]

Gal Katz and Doron Peled. 2010. MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming. In 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010 (Lecture Notes in Computer Science), Ahmed Bouajjani and Wei-Ngan Chin (Eds.), Vol. 6252. Springer, Singapore, 359--364.

Digital Library

[27]

Gal Katz and Doron Peled. 2016. Synthesizing, correcting and improving code, using model checking-based genetic programming. International Journal on Software Tools for Technology Transfer (2016), 1--16.

[28]

Zoltan Kocsis and Jerry Swan. 2014. Asymptotic Genetic Improvement Programming with Type Functors and Catamorphisms. In Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature, Ljubljana, Slovenia.

[29]

Zoltan A. Kocsis, John H. Drake, Douglas Carson, and Jerry Swan. 2016. Automatic Improvement of Apache Spark Queries using Semantics-preserving Program Reduction. In Genetic Improvement 2016 Workshop, Justyna Petke, David R. White, and Westley Weimer (Eds.). ACM, Denver, 1141--1146.

Digital Library

[30]

Zoltan A. Kocsis and Jerry Swan. 2017 (to appear). Genetic Programming + Proof Search = Automatic Improvement. Journal of Automated Reasoning (2017 (to appear)).

[31]

Krzysztof Krawiec. 2015. Behavioral Program Synthesis with Genetic Programming. Studies in Computational Intelligence, Vol. 618. Springer International Publishing.

Digital Library

[32]

Lech Madeyski. 2010. Test-Driven Development: An Empirical Evaluation of Agile Practice (1st ed.). Springer Publishing Company, Incorporated.

Digital Library

[33]

Bertrand Meyer. 1986. Design by Contract. Technical Report TR-EI-12/CO. Interactive Software Engineering Inc.

[34]

Stephen Muggleton. 1994. Inductive Logic Programming: Derivations, Successes and Shortcomings. SIGART Bull. 5, 1 (Jan. 1994), 5--11.

Digital Library

[35]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. SIGPLAN Not. 41, 11 (Oct. 2006), 404--415.

Digital Library

[36]

Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From Program Verification to Program Synthesis. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10). ACM, New York, NY, USA, 313--326.

Digital Library

[37]

L. G. Valiant. 1984. A Theory of the Learnable. Commun. ACM 27, 11 (Nov. 1984), 1134--1142.

Digital Library

[38]

Jim Woodcock and Jim Davies. 1996. Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.

Digital Library

Cited By

Helmuth TPantridge EFrazier JSpector L(2024)Generational Computation Reduction in Informal Counterexample-Driven Genetic ProgrammingGenetic Programming10.1007/978-3-031-56957-9_2(21-37)Online publication date: 3-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-56957-9_2
Helmuth TFrazier JShi YAbdelrehim ASilva SPaquete L(2023)Human-Driven Genetic Programming for Program Synthesis: A PrototypeProceedings of the Companion Conference on Genetic and Evolutionary Computation10.1145/3583133.3596373(1981-1989)Online publication date: 15-Jul-2023
https://dl.acm.org/doi/10.1145/3583133.3596373
Fonseca APoças DSilva SPaquete L(2023)Comparing the expressive power of Strongly-Typed and Grammar-Guided Genetic ProgrammingProceedings of the Genetic and Evolutionary Computation Conference10.1145/3583131.3590507(1100-1108)Online publication date: 15-Jul-2023
https://dl.acm.org/doi/10.1145/3583131.3590507
Show More Cited By

Index Terms

Counterexample-driven genetic programming
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
        Genetic programming
2. Theory of computation
  1. Design and analysis of algorithms
    1. Mathematical optimization
      1. Discrete optimization
        Optimization with randomized search heuristics
        Evolutionary algorithms
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Counterexample-driven genetic programming without formal specifications
GECCO '20: Proceedings of the 2020 Genetic and Evolutionary Computation Conference Companion

Counterexample-driven genetic programming (CDGP) uses specifications provided as formal constraints in order to generate the training cases used to evaluate the evolving programs. It has also been extended to combine formal constraints and user-provided ...
Counterexample-driven genetic programming: Heuristic program synthesis from formal specifications

Conventional genetic programming GP can guarantee only that synthesized programs pass tests given by the provided input-output examples. The alternative to such a test-based approach is synthesizing programs by formal specification, typically realized ...
Counterexample-driven genetic programming: stochastic synthesis of provably correct programs
IJCAI'18: Proceedings of the 27th International Joint Conference on Artificial Intelligence

Genetic programming is an effective technique for inductive synthesis of programs from tests, i.e. training examples of desired input-output behavior. Programs synthesized in this way are not guaranteed to generalize beyond the training set, which is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

GECCO '17: Proceedings of the Genetic and Evolutionary Computation Conference

July 2017

1427 pages

ISBN:9781450349208

DOI:10.1145/3071178

General Chair:
Peter A. N. Bosman
Centrum Wiskunde & Informatica (CWI)

Copyright © 2017 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

SIGEVO: ACM Special Interest Group on Genetic and Evolutionary Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Centre, Poland

Conference

GECCO '17

Sponsor:

SIGEVO

GECCO '17: Genetic and Evolutionary Computation Conference

July 15 - 19, 2017

Berlin, Germany

Acceptance Rates

GECCO '17 Paper Acceptance Rate 178 of 462 submissions, 39%;

Overall Acceptance Rate 1,669 of 4,410 submissions, 38%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
276
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)1

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Helmuth TPantridge EFrazier JSpector L(2024)Generational Computation Reduction in Informal Counterexample-Driven Genetic ProgrammingGenetic Programming10.1007/978-3-031-56957-9_2(21-37)Online publication date: 3-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-56957-9_2
Helmuth TFrazier JShi YAbdelrehim ASilva SPaquete L(2023)Human-Driven Genetic Programming for Program Synthesis: A PrototypeProceedings of the Companion Conference on Genetic and Evolutionary Computation10.1145/3583133.3596373(1981-1989)Online publication date: 15-Jul-2023
https://dl.acm.org/doi/10.1145/3583133.3596373
Fonseca APoças DSilva SPaquete L(2023)Comparing the expressive power of Strongly-Typed and Grammar-Guided Genetic ProgrammingProceedings of the Genetic and Evolutionary Computation Conference10.1145/3583131.3590507(1100-1108)Online publication date: 15-Jul-2023
https://dl.acm.org/doi/10.1145/3583131.3590507
Błądek IKrawiec K(2023)Counterexample-Driven Genetic Programming for Symbolic Regression With Formal ConstraintsIEEE Transactions on Evolutionary Computation10.1109/TEVC.2022.320528627:5(1327-1339)Online publication date: Oct-2023
https://doi.org/10.1109/TEVC.2022.3205286
Kubalík JDerner EBabuška R(2023)Toward Physically Plausible Data-Driven Models: A Novel Neural Network Approach to Symbolic RegressionIEEE Access10.1109/ACCESS.2023.328739711(61481-61501)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3287397
Garrow FLones MStewart RWagner M(2022)Why functional program synthesis matters (in the realm of genetic programming)Proceedings of the Genetic and Evolutionary Computation Conference Companion10.1145/3520304.3534045(1844-1853)Online publication date: 9-Jul-2022
https://dl.acm.org/doi/10.1145/3520304.3534045
Kubalík JDerner EBabuška R(2021)Multi-objective symbolic regression for physics-aware dynamic modelingExpert Systems with Applications: An International Journal10.1016/j.eswa.2021.115210182:COnline publication date: 15-Nov-2021
https://dl.acm.org/doi/10.1016/j.eswa.2021.115210
Welsch TKurlin VCoello Coello C(2020)Synthesis through unification genetic programmingProceedings of the 2020 Genetic and Evolutionary Computation Conference10.1145/3377930.3390208(1029-1036)Online publication date: 25-Jun-2020
https://dl.acm.org/doi/10.1145/3377930.3390208
Kubalík JDerner EBabuška RCoello Coello C(2020)Symbolic regression driven by training data and prior knowledgeProceedings of the 2020 Genetic and Evolutionary Computation Conference10.1145/3377930.3390152(958-966)Online publication date: 25-Jun-2020
https://dl.acm.org/doi/10.1145/3377930.3390152
Helmuth TSpector LPantridge ECoello Coello C(2020)Counterexample-driven genetic programming without formal specificationsProceedings of the 2020 Genetic and Evolutionary Computation Conference Companion10.1145/3377929.3389983(239-240)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3377929.3389983
Show More Cited By

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