- author = "Iwo Bladek",
- title = "Machine Learning and Formal Verification for Acquisition of Knowledge in Heuristic Program Synthesis",
- school = "Politechnika Poznanska",
- year = "2022",
- address = "Poznan, Poland",
- keywords = "genetic algorithms, genetic programming, Counterexample-Driven Genetic Programming, CDGP, Counterexample Driven Symbolic Regression, CDSR, Neuro-Guided Genetic Programming, ANN, Evolutionary Program Sketching, EPS, SMT, formal verification of software, machine learning, program synthesis, programowanie genetyczne, formalna weryfikacja oprogramowania, uczenie maszynowe, synteza programow",
- language = "en",
-
URL = "
https://sin.put.poznan.pl/dissertations/details/d2987",
-
URL = "
http://www.cs.put.poznan.pl/ibladek/publications/phdthesis.pdf",
- size = "159 pages",
- abstract = "we present and evaluate our techniques for efficient heuristic program synthesis based on genetic programming (GP). The common theme among our approaches is that various kinds of information (knowledge) are collected during runtime or a separate training phase, and then are used to guide GP search. Three of the described techniques, i.e., Evolutionary Program Sketching, Counterexample-Driven GP, and Counterexample-Driven Symbolic Regression, use formal verification/synthesis to either find locally optimal code fragments, or discover counterexamples exposing incorrect behavior of candidate programs. The fourth approach, Neuro-Guided GP, uses machine learning to learn the probability distribution of program instructions given input-output examples, and then uses it to bias variation operators of GP. The computational experiments show that all presented methods outperform or provide some advantages over existing state of the art methods.",
- abstract_pl = "W rozprawie przedstawiamy i analizujemy opracowane przez nas techniki efektywnej heurystycznej syntezy programow opartej o programowanie genetyczne (GP). Wspolna cecha tych technik jest zdobywanie roznych rodzajow informacji w trakcie dzialania algorytmu lub odrebnej fazie uczenia. Trzy z opisanych podejsc, Evolutionary Program Sketching, Counterexample-Driven GP i Counterexample-Driven Symbolic Regression, korzystaja z formalnej weryfikacji/syntezy w celu znajdowania lokalnie optymalnych fragmentow kodu lub odkrywania kontrprzykladow prezentujacych niepoprawne dzialanie generowanych programow. Czwarte podejscie, Neuro-Guided GP, korzysta z technik uczenia maszynowego w celu odkrycia rozkladu prawdopodobienstwa instrukcji na podstawie przykladow wejscie-wyjscie, a nastepnie wykorzystuje go do ukierunkowania operatorow przeszukiwania w GP. Eksperymenty obliczeniowe wykazaly, ze prezentowane metody sa konkurencyjne i oferuja wiele zalet w porownaniu do rozwiazan dostepnych w literaturze.",
-
notes = "Also known as \cite{Bladek2022:d2987}
On-line catalog to2022000422
Supervisor: Krzysztof Krawiec",
