Machine Learning and Formal Verification for Acquisition of Knowledge in Heuristic Program Synthesis
[ 1 ] Instytut Informatyki, Wydział Informatyki i Telekomunikacji, Politechnika Poznańska | [ P ] pracownik
[ 1 ] Instytut Informatyki, Wydział Informatyki i Telekomunikacji, Politechnika Poznańska | [ P ] pracownik
PL Uczenie maszynowe i formalna weryfikacja dla pozyskiwania wiedzy w heurystycznej syntezie programów
angielski
- genetic programming
- formal verification of software
- machine learning
- program synthesis
- programowanie genetyczne
- formalna weryfikacja oprogramowania
- uczenie maszynowe
- synteza programów
EN In this thesis, 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.
PL W rozprawie przedstawiamy i analizujemy opracowane przez nas techniki efektywnej heurystycznej syntezy programów opartej o programowanie genetyczne (GP). Wspólną cechą tych technik jest zdobywanie różnych rodzajów informacji w trakcie działania algorytmu lub odrębnej fazie uczenia. Trzy z opisanych podejść, Evolutionary Program Sketching, Counterexample-Driven GP i Counterexample-Driven Symbolic Regression, korzystają z formalnej weryfikacji/syntezy w celu znajdowania lokalnie optymalnych fragmentów kodu lub odkrywania kontrprzykładów prezentujących niepoprawne działanie generowanych programów. Czwarte podejście, Neuro-Guided GP, korzysta z technik uczenia maszynowego w celu odkrycia rozkładu prawdopodobieństwa instrukcji na podstawie przykładów wejście-wyjście, a następnie wykorzystuje go do ukierunkowania operatorów przeszukiwania w GP. Eksperymenty obliczeniowe wykazały, że prezentowane metody są konkurencyjne i oferują wiele zalet w porównaniu do rozwiązań dostępnych w literaturze.
157
nauki o komputerach i informatyka
informatyka
DrOIN 2191
publiczny
Wojciech Jamroga
Gdańsk, Polska
04.04.2022
polski
publiczny
Robert Schaefer
Kraków, Polska
17.03.2022
polski
publiczny
rozprawa doktorska
Poznań, Polska
20.05.2022
Rada Dyscypliny Informatyka Techniczna i Telekomunikacja Politechniki Poznańskiej
doktor nauk inżynieryjno-technicznych w dyscyplinie: informatyka techniczna i telekomunikacja