Sammanfattning Formell syntes är processen att generera ett program som uppfyller en formell specifikation på hög nivå. På senare tid har effektiva formella syntesmetoder föreslagits på grundval av användningen av induktivt lärande. Vi hänvisar till denna klass av metoder som lär sig program från exempel som formell induktiv syntes. I detta dokument presenterar vi en teoretisk ram för formell induktiv syntes. Vi diskuterar hur formell induktiv syntes skiljer sig från traditionell maskininlärning. Vi beskriver sedan orakelstyrd induktiv syntes (OGIS), ett ramverk som fångar en familj av synthesizers som fungerar genom att iterativt fråga ett orakel. Ett exempel på OGIS som har haft stor praktisk inverkan är kontraexempelstyrd induktiv syntes (CEGIS). Vi presenterar en teoretisk karakterisering av CEGIS för att lära sig något program som beräknar ett rekursivt språk. I synnerhet analyserar vi den relativa effekten av CEGIS varianter där de typer av motexempel som genereras av orakel varierar. Vi överväger också effekten av avgränsade kontra obundna minnen tillgängliga för inlärningsalgoritmen. I det speciella fallet där kandidatprogrammens universum är ändligt relaterar vi konvergenshastigheten till begreppet undervisningsdimension som studeras i maskininlärningsteori. Sammantaget tar dokumentets resultat ett första steg mot en teoretisk grund för det framväxande området för formell induktiv syntes.
Oracle-Guided Inductive Synthesis Jha och Seshia utvecklade nyligen en ny formalism för induktiv syntes kallad oracleled inductive syntes (OGIS) REF.
A theory of formal synthesis via inductive learning
{'venue': 'Acta Informatica', 'journal': 'Acta Informatica', 'mag_field_of_study': ['Computer Science']}