Formal Inductive Synthesis -- Theory And Applications
Formal Inductive Synthesis-- Theory and ApplicationsSanjit A. SeshiaProfessorEECS DepartmentUC BerkeleyAcknowledgments to several Ph.D. students, postdoctoralresearchers, and collaborators, and tothe students of EECS 219C, Spring 2015/16, UC BerkeleySAT/SMT Winter School @ TIFRDecember 8, 2016
Connections in this LectureSAT/SMT SolvingFormalSynthesisMachine Learning–2–
Examples of Synthesis–3–
Program Synthesis: Example 1Compute the MAX of two 32‐bit integers without usingconditional statements!int max(int x, int y) {if (x y)return x;elsereturn y;}int max no cond(int x, int y) {t1 x y;t2 - (x y);t3 t1 & t2;return t3 x;}
Program Synthesis: Example 2Turn off rightmost contiguous 1 bits10110 10000, 11010 11000Naïve implementation:i length(x) – 1;while( x[i] 0 ){i--; if (i 0) return x;}x[i] 0; i--;while( x[i] 1 ){x[i] 0; i--; if (i 0) return x;}return x;Bit-wise implementation:t1 x - 1;t2 x t1;t3 t2 1;return t3 & x;
Program Synthesis problem Given a reference implementation R, and arestricted program space S, find a program P in Sthat is equivalent to the reference R. Reference: S. Jha et al., Oracle‐GuidedComponent‐Based Program Synthesis, ICSE 2010.S. A. Seshia6
Example Verification Problem Transition System– Init: Ix 1 y 1– Transition Relation: x’ x y y’ y xx, y Z Temporal Logic Property: G (y 1)– “always, y 1” Attempted Proof by Induction:– Base Case: x 1 y 1 y 1– Inductive Step:y 1 x’ x y y’ y x y’ 1
Example Verification Problem Transition System– Init: Ix 1 y 1– Transition Relation: x’ x y y’ y x Property: G (y 1) Attempted Proof by Induction Fails:y 1 x’ x y y’ y x y’ 1 Need to Strengthen Invariant: Find s.t. y 1 x’ x y y’ y x ’ y’ 1 Safety Verification Invariant Synthesis
Safety Verification as Invariant Synthesis Transition System– Init: Ix 1 y 1– Transition Relation: x’ x y y’ y x Property: G (y 1) Following Strengthened Invariant works: x 1x 1 y 1 x’ x y y’ y x x’ 1 y’ 1 How can we automate this process?
Another (Fun) Synthesis Problem: Inventing Card[S. Jha, V. Raman, and S. A. Seshia, FMCAD 2016]TricksTransformations such asMoving card to front/back,Flipping card over,Cutting the deck (withaudience choice),Repeating some numberof times (audience chosen)J – audience cardConfiguration where onlyfront‐facing card is the onechosen initially by audience sequence of transformations audience choices(we reach the desired final configuration)Similar format for problems in AI planningS. A. Seshia10
Formal Synthesis andMachine Learning– 11 –
Formal Synthesis Given:– Class of Artifacts C– Formal (mathematical) Specification Find f C that satisfies Example:– C: all affine functions f of x R– : x. f(x) x 42– 12 –
Induction vs. Deduction Induction: Inferring general rules (functions)from specific examples (observations)– Generalization Deduction: Applying general rules to deriveconclusions about specific instances– (generally) Specialization Learning/Synthesis can be Inductive orDeductive or a combination of the two– 13 –
Inductive Synthesis Given– Class of Artifacts C– Set of (labeled) Examples E (or source of E)– A stopping criterion May or may not be formally described Find, using only E, an f C that meets Example:– C: all affine functions f of x R– E {(0,42), (1, 43), (2, 44)}– -- find consistent f– 14 –
Inductive Synthesis Given– Class of Artifacts C– Set of Examples E (or source of E)– A stopping criterion Find using only E an f C that meets Example:– C: all affine functions f of x R– E {(0,42), (1, 43), (2, 45)}– -- find consistent f– 15 –
Inductive Synthesis Example:– C: all predicates of the form ax by c– E {(0,42), (1, 43), (2, 45)}– -- find consistent f One such: -x y 42 Another: -x y 0 Which one to pick: need to augment ?– 16 –
Machine Learning "A computer program is said tolearn from experience E withrespect to some class of tasks Tand performance measure P, ifits performance at tasks in T, asmeasured by P, improves withexperience E.”- Tom Mitchell [1998]– 17 –
Machine Learning: Typical SetupGiven: Domain of Examples D Concept class C– Concept is a subset of D– C is set of all concepts Criterion (“performance measure”)Find using only examples from D, f C meeting – 18 –
Inductive Bias in Machine Learning“Inductive bias is the set ofassumptions required todeductively infer a conceptfrom the inputs to the learningalgorithm.”Example:C: all predicates of the form ax by cE {(0,42), (1, 43), (2, 45)} -- find consistent fWhich one to pick: -x y 42 or -x y 0Inductive Bias resolves this choice E.g., pick the “simplest one” (Occam’s razor)– 19 –
Formal Inductive Synthesis(Initial Defn) Given:– Class of Artifacts C– Formal specification – Domain of examples D Find f C that satisfies using only elements of D– i.e. no direct access to , only to elements of Drepresenting Example:– C: all affine functions f of x R– D R2– : x. f(x) x 42– 20 –
ImportanceFormal Inductive Synthesis is Everywhere!– Many problems can be solved effectivelywhen viewed as synthesisParticularly effective in various tasks inFormal MethodsFor the rest of this lecture series, for brevity we willoften use “Inductive Synthesis” to mean “FormalInductive Synthesis”– 21 –
Formal Methods Computational ProofMethods Formal Methods is about Provable Guarantees– Specification/Modeling Statement ofConjecture/Theorem– Verification Proving/Disproving the Conjecture– Synthesis Generating (parts of) Conjecture/Proof Formal Methods Computational Proof methods– Temporal logic / Assertions– Boolean reasoning: SAT solving & Binary DecisionDiagrams– Equivalence checking– Model checking– Automated theorem proving, SMT solving– – 22 –2
Inductive Synthesis for FormalMethods Modeling / Specification– Generating environment/component models– Inferring (likely) specifications/requirements Verification– Synthesizing verification/proof artifacts such asinductive invariants, abstractions, interpolants,environment assumptions, etc. Synthesis (of course)– 23 –
Questions of Interest for this Tutorial How can inductive synthesis be used to solveother (non-synthesis) problems? What is a core computational problem for formalsynthesis (aka SAT or SMT)? Is there a theory of formal inductive synthesisdistinct from (traditional) machine learning? Is there a complexity/computability theory forformal inductive synthesis?– 24 –
Questions of Interest for this Tutorial How can inductive synthesis be used to solveother (non-synthesis) problems? Reducing a Problem to Synthesis What is a core computational problem for formalsynthesis (aka SAT or SMT)? Syntax-Guided Synthesis (SyGuS) Is there a theory of formal inductive synthesisdistinct from (traditional) machine learning? Oracle-Guided Inductive Synthesis (OGIS) Is there a complexity/computability theory forformal inductive synthesis? Yes! Can compare different oracles/learners– 25 –
Outline for this Lecture Sequence Examples of Reduction to Synthesis– Specification– Verification Demo: Requirement Mining for Cyber-PhysicalSystems Differences between Inductive Synthesis andMachine Learning Oracle-Guided Inductive Synthesis– Examples, CEGIS Theoretical Analysis of CEGIS– Properties of Learner– Properties of Verifier– 26 –
Further Reading S. A. Seshia, “Combining Induction, Deduction,and Structure for Verification and Synthesis.”,Proc. IEEE 2015, DAC 2012http://www.eecs.berkeley.edu/ berkeley.edu/ sseshia/pubs/b2hd-seshiapieee15.html S. Jha and S. A. Seshia, “A Theory of FormalSynthesis via Inductive Learning”http://www.eecs.berkeley.edu/ sseshia/pubs/b2hd-jhaarxiv15.html Lecture notes of EECS 219C: “Computer-AidedVerification” class at UC Berkeley, available at:http://www.eecs.berkeley.edu/ sseshia/219c/– 27 –
Reductions to Synthesis– 28 –
Artifacts Synthesized in Verification Inductive invariantsAbstraction functions / abstract modelsAuxiliary specifications (e.g., pre/post-conditions,function summaries)Environment assumptions / Env model / interfacespecificationsInterpolantsRanking functionsIntermediate lemmas for compositional proofsTheory lemma instances in SMT solvingPatterns for Quantifier Instantiation – 29 –
Recall: Example Verification Problem Transition System– Init: Ix 1 y 1– Transition Relation: x’ x y y’ y x Property: G (y 1) Attempted Proof by Induction:y 1 x’ x y y’ y x y’ 1 Fails. Need to Strengthen Invariant: Find s.t.x 1 y 1 x’ x y y’ y x x’ 1 y’ 1 Safety Verification Invariant Synthesis– 30 –
One Reduction from Verification toSynthesisNOTATIONTransition system M (I, )Safety property G( )VERIFICATION PROBLEMDoes M satisfy ?SYNTHESIS PROBLEMSynthesize s.t.I ’ ’– 31 –
Two Reductions from Verification toSynthesisNOTATIONTransition system M (I, ), S set of statesSafety property G( )VERIFICATION PROBLEMDoes M satisfy ?SYNTHESIS PROBLEM #1Synthesize s.t.I ’ ’SYNTHESIS PROBLEM #2Synthesize : S Ŝ whereˆ )ˆ (M) (I,s.t. (M) satisfies iffM satisfies – 32 –
Common Approach for both:Inductive SynthesisSynthesis of: Inductive Invariants– Choose templates for invariants– Infer likely invariants from tests (examples)– Check if any are true inductive invariants, possiblyiterate Abstraction Functions– Choose an abstract domain– Use Counter-Example Guided AbstractionRefinement (CEGAR)– 33 –
Counterexample-Guided AbstractionRefinement is Inductive Synthesis[Anubhav Gupta, ‘06]System heckerAbstract Model PropertyFailDoneCounterexampleNew Abstraction � 34 –
CEGAR Counterexample-GuidedInductive Synthesis (of Abstractions)INITIALIZEStructure Hypothesis (“Syntax-Guidance”),Initial ampleSynthesis FailsVerification Succeeds– 35 –
Lazy SMT Solving performsInductive Synthesis (of TIONSYNTHESISGenerateSATFormulaInvokeSATSolverSAT FormulaSAT(model)Blocking NSATDone(“Counterexample”)Invoke TheorySolverSATDone– 36 –
Reducing Specification to Synthesis Formal Specifications difficult for non-experts Tricky for even experts to get right! Yet we need them!“A design without specification cannot be right orwrong, it can only be surprising!”– paraphrased from [Young et al., 1985] Specifications are crucial for effective testing,verification, synthesis, – 37 –
Reduction of Specification toSynthesis VERIFICATION: Given (closed) system M, andspecification , does M satisfy ?Suppose we don’t have (a good enough) .SYNTHESIS PROBLEM: Given (closed) systemM, find specification such that M satisfies .– Is this enough?– 38 –
ExampleabLet a and b be atomic propositions.What linear temporal logic formulas does the above systemsatisfy?– 39 –
Reduction of Specification toSynthesis VERIFICATION: Given (closed) system M, andspecification , does M satisfy ? SYNTHESIS PROBLEM: Given (closed) system Mand class of specifications C, find specification in C such that M satisfies .– C can be defined syntactically (e.g. with atemplate)– E.g. G( X )– 40 –
Reduction of Specification toSynthesis VERIFICATION: Given (closed) system M, andspecification , does M satisfy ? SYNTHESIS PROBLEM: Given (closed) system M andclass of specifications C, find “tightest” specification in C such that M satisfies .– Industrial Tech. Transfer Story: Requirement Synthesis forAutomotive Control Systems [Jin, Donze, Deshmukh, Seshia,HSCC 2013, TCAD 2015]http://www.eecs.berkeley.edu/ sseshia/pubs/b2hd-jin-tcad15.html– Based on Counterexample-Guided Inductive Synthesis(CEGIS)– Implemented in Breach toolbox by A. Donze– An enabler for Toyota to apply formal verification to softwarein a cyber-physical system [see Yamaguchi et al., FMCAD 2016]– 41 –
Specification Mining Inductive Synthesis of Specifications See survey of the topic in recent Ph.D.dissertation by Wenchao Li: “SpecificationMining: New Formalisms, Algorithms s/TechRpts/2014/EECS-2014-20.html– Environment Assumptions for Reactive Synthesis(with application to planning in robotics)– 42 –
Summary of Part 1 Basic Terminology–––– Formal SynthesisInductive SynthesisFormal Inductive Synthesis (basic intro)Notions from Machine LearningReductions to Synthesis– Verification artifacts– Specifications– Industry tech transfer: requirement mining forclosed-loop automotive control systems– 43 –
Syntax-Guided Synthesis– 44 –
Formal Synthesis (recap) Given:– Formal Specification – Class of Artifacts C Find f C that satisfies – 45 –
Syntax-Guided Synthesis (SyGuS) Given:– An SMT formula in UF T (where T is somecombination of theories)– Typed uninterpreted function symbols f1,.,fk in – Grammars G, one for each function symbol fi Generate expressions e1,.,ek from G s.t. [f1,.,fk e1,.,ek]is valid in T– 46 –
SyGuS Example 1 Theory QF-LIA– Types: Integers and Booleans– Logical connectives, Conditionals, and Linear arithmetic– Quantifier-free formulas Function to be synthesized Specification:, GrammarLinExp :,, x y Const LinExp:, ,LinExp LinExp ‐ LinExpIs there a solution?– 47 –
SyGuS Example 2 Theory QF-LIA– Types: Integers and Booleans– Logical connectives, Conditionals, and Linear arithmetic– Quantifier-free formulas Function to be synthesized Specification:, Grammar,, :, ,Term : x y Const If-Then-Else (Cond, Term, Term)Cond : Term Term Cond & Cond Cond (Cond)Is there a solution?– 48 –
From SMT-LIB to SYNTH-LIB(set-logic LIA)(synth-fun max2 ((x Int) (y Int)) Int((Start Int (x y 0 1 ( Start Start)(- Start Start)(ite StartBool Start Start)))(StartBool Bool ((and StartBool StartBool)(or StartBool StartBool)(not StartBool)( Start Start)))))(declare-var x Int)(declare-var y Int)(constraint ( (max2 x y) x))(constraint ( (max2 x y) y))(constraint (or ( x (max2 x y)) ( y (max2 x y))))(check-synth)– 49 –
Invariant Synthesis via SyGuS Find s.t.x 1 y 1 y 1 y 1 x’ x y y’ y x ’ y’ 1 Syntax-Guidance: Grammar expressing simplelinear predicates of the form S 0 where S is anexpression defined as:S :: 0 1 x y S S S – S Homework: Try encoding this in SyGuS andsolve it using one of the reference solversavailable at sygus.org– 50 –
Recall Program Synthesis Example 2Turn off rightmost contiguous 1 bits10110 10000, 11010 11000Naïve implementation:i length(x) – 1;while( x[i] 0 ){i--; if (i 0) return x;}x[i] 0; i--;while( x[i] 1 ){x[i] 0; i--; if (i 0) return x;}return x;Bit-wise implementation:t1 x - 1;t2 x t1;t3 t2 1;return t3 & x;– 51 –
More Demos (time permitting) Impact of Grammar definition– Small changes to grammar can affect the run timein unpredictable ways! Visit http://www.sygus.org for publications,benchmarks and sample solvers– 52 –
SyGuS SMTExists-Forall SMT f x (f,x) SyGuS (abusing notation slightly) f G x (f,x) Sometimes SyGuS is solved by reductionto EF-SMT– 53 –
Other Considerations Let-Expressions (for common sub-expressions)– Example:S :: let [t : T] in t * tT :: x y 0 1 T T T - T Cost constraints/functions (for “optimality” ofsynthesized function)– 54 –
SyGuS vs. CEGIS SyGuS --- problem classes CEGIS --- solution classes– 55 –
Example: CEGIS for SyGuS Specification:, , , ,GrammarTerm : x y 0 1 If-Then-Else (Cond, Term, Term)Cond : Term Term Cond & Cond Cond (Cond)Examples: { }Candidatef(x,y) xSYNTHESIZEVERIFYCounterexample(x 0, y 1)– 56 –
Example: CEGIS for SyGuS Specification:, , , ,GrammarTerm : x y 0 1 If-Then-Else (Cond, Term, Term)Cond : Term Term Cond & Cond Cond (Cond)Examples: {(0,1)}Candidatef(x,y) ySYNTHESIZEVERIFYCounterexample(x 1, y 0)– 57 –
Example: CEGIS for SyGuS Specification:, , , ,GrammarTerm : x y 0 1 If-Then-Else (Cond, Term, Term)Cond : Term Term Cond & Cond Cond (Cond)Examples:{(0,1),(1,0)}Candidatef(x,y) 1SYNTHESIZEVERIFYCounterexample(x 0, y 0)– 58 –
Example: CEGIS for SyGuS Specification:, , , ,GrammarTerm : x y 0 1 If-Then-Else (Cond, Term, Term)Cond : Term Term Cond & Cond Cond (Cond)Examples:{(0,1),(1,0),(0,0)}Candidatef(x,y) ITE(x y, y, x)SYNTHESIZEVERIFYVerification Succeeds!– 59 –
Three Flavors of SyGuS Solvers All use CEGIS, differ in implementation of“Synthesis” step Enumerative [Udupa et al., PLDI 2013]– Enumerate expressions in increasing order of“syntactic simplicity” with heuristic optimizations Symbolic [Jha et al., ICSE 2010, PLDI 2011]– Encode search for expressions as SMT problem– Similar approach used in SKETCH [Solar-Lezama’08] Stochastic [Schkufza et al., ASPLOS 2013]– Markov Chain Monte Carlo search method overspace of expressions See [Alur et al., FMCAD 2013] paper for more details– 60 –
Decidability of SyGuS Problems[B. Caulfield, M. Rabe, S. A. Seshia, S. Tripakis,“What’s Decidable about Syntax-Guided Synthesis, 2016]– 61 –
An Industrial Application of InductiveSynthesis of SpecificationsRequirements Mining for Closed-Loop AutomotiveControl SystemsUsed internally by Toyota production groups– 62 –
Challenges for Verification of AutomotiveControl Systems Closed‐loop setting very complex software physical artifactsnonlinear dynamicslarge look‐up tableslarge amounts of switchingExperimental EngineControl ModelRequirements Incomplete/Informal Specifications often created concurrentlywith the design!Designers often only have informalintuition about what is “good behavior” “shape recognition”63
Solution: Requirements MiningRequirements Expressed in Signal Temporal Logic(STL) [Maler & Nickovic, ‘04]Value added by mining: It’s working, but I don’tunderstand why!Mined Requirements become usefuldocumentation Use for code maintenance and revision Use during tuning and testing64
Control Designer’s Viewpoint of the Method Tool extracts properties of closed‐loop designDesigner reviews mined requirements “Settling time is 6.25 ms” 100“Overshoot is 100 units”6.25msExpressed in SignalTemporal Logic [Maler & Nickovic, ‘04]65
Signal Temporal Logic (STL) Extension of Linear Temporal Logic (LTL) and Variantof Metric Temporal Logic (MTL)– Quantitative semantics: satisfaction of a property over atrace given real‐valued interpretation– Greater value more easily satisfied– Non‐negative satisfaction value Boolean satisfaction Example: “For all time points between 60 and 100,the absolute value of x is below 0.1”x1 0.1-0.1t60010066
CounterExample Guided Inductive Synthesis[Jin, Donze, Deshmukh, Seshia, HSCC 2013]Experimental EngineControl Model1.Find “Tightest”PropertiesAre there behaviorsthat do NOT satisfytheserequirements?Settling Time is 5 msOvershoot is 5 KPaUpper Bound on x is 3.6Settling Time is ?Overshoot is ?Upper Bound on x is ?67
CounterExample Guided Inductive SynthesisExperimental EngineControl Model1.Are there behaviorsthat do NOT satisfytheserequirements?CounterexamplesFind “Tightest”PropertiesSettling Time is 5.3msmsOvershoot is 5.1KPaKPaUpper Bound on x is 3.8Settling Time is ?Overshoot is ?Upper Bound on x is ?68
CounterExample Guided Inductive SynthesisOptimization‐basedFalsificationAre there behaviorsthat do NOT satisfytheserequirements?Experimental EngineParameterControl ModelSynthesis (exploits1.monotonicity)CounterexamplesFind "Tightest"PropertiesSettling Time is ?Overshoot is ?Upper Bound on x is ?Settling Time is 6.3 msOvershoot is 5.6 KPaUpper Bound on x is 4.1Parametric SignalTemporal Logic(PSTL)NOMinedRequirementSettling Time is 6.3 msOvershoot is 5.6 KPaUpper Bound on x is 4.169
Parameter Synthesis Find ‐tightvalues of params (for suitably small )1 000 000Find "Tightest"PropertiesToo loose32.90x100Want the value of corresponding to the “tightest”satisfaction over a set of traces70
Satisfaction MonotonicityFind "Tightest"Properties Satisfaction function monotonic in parameter value Example:43If upper bound of all signals is 3,any number 3 is also an upperbound050100 ( , x) inft ( ‐ x(t) ) For all x, ( , x) is a monotonic function of Advantage: If monotonic, use binary search overparam space, otherwise exhaustive search71
Deciding Satisfaction Monotonicity ‐‐use SMT solving!Find "Tightest"Properties Need to decide whether:For all x, ( , x) is a monotonic function of Theorem: Deciding monotonicity of a PSTL formula isundecidable Use an encoding to satisfiability modulo theories(SMT) solving– Quantified formulas involving uninterpreted functions,and arithmetic over reals linear arithmetic if predicatesare linear72
Experimental Results on Industrial Airpath[Jin, Donze, Deshmukh, Seshia, HSCC 2013]ControllerExperimental EngineControl Model Found max overshoot with 7000 simulations in 13 hours Attempt to mine maximum observed settling time:– stops after 4 iterations– gives answer tsettle simulation time horizon (shown in trace below)73
Mining can expose deep bugsExperimental EngineControl Model Uncovered a tricky bug– Discussion with control designer revealed it to be a real bug– Root cause identified as wrong value in a look‐up table, bugwas fixed Duality between spec mining and bug‐finding:– Synthesizing “tightest” spec could uncover corner‐case bugs– Looking for bugs Mine for negation of bug74
Toyota Unit’s Experience with Model Checking[FMCAD’16]Revising propertyMaking modelMaking propertyExecutingmodel checkingRevising modelTotalWork hour1 trial70min560min7 trailsMappingcounterexample40minMaking/revising property: 110 minMapping counterexample: 280 min for just 1 module75
Overview of FMCAD’16 methodologyBreach1. Pre-conditionminingPre-condition forsoftware moduleSLDV/CBMC2. Softwaremodel checkingModule levelcounterexample3. Simulation-BasedVerification BreachinoutSystem levelcounterexample76
Requirement Mining In Toyota Case Study [FMCAD’16] Founded false caseViolation area of post-conditionFind system level violationactuator output 15077
Demo: Requirement Mining for a HelicopterControl Model
An Example: Modeling Helicopter Dynamics(taken from textbook available athttp://LeeSeshia.org, Chapter 2)Go to Breach webpage for this example:http://www.eecs.berkeley.edu/ donze/mining example.html
Modeling Physical MotionSix degrees of freedom: Position: x, y, z Orientation: pitch, yaw, roll
Feedback Control ProblemA helicopter without a tail rotor, like the onebelow, will spin uncontrollably due to thetorque induced by friction in the rotor shaft.Control system problem:Apply torque using the tailrotor to counterbalancethe torque of the top rotor.
Model of the helicopterInput is the net torque ofthe tail rotor and the toprotor. Output is the angularvelocity around the y axis.Parameters of themodel are shown inthe box. The inputand output relation isgiven by the equationto the right.
Proportional ueHow long does it take for theta dot to reach desired psi?
Summary of Part 2 Syntax-Guided Synthesis–––– Problem DefinitionExamplesCEGISDecidabilityRequirement Mining for Closed-Loop ControlSystems– Use of CEGIS, but for synthesis of STL properties– SMT solving used to determine satisfactionmonotonicity– 84 –
Theoretical Aspects ofFormal Inductive Synthesis– 85 –
CEGIS Learning from Examples &CounterexamplesINITIALIZE“Concept Class”, Initial IONORACLECounterexampleLearning FailsLearning Succeeds– 86 –
How is Formal Inductive Synthesis differentfrom (traditional) Machine Learning?– 87 –
Comparison*Feature[see also, Jha & Seshia, 2015]Formal InductiveMachine e,ComplexFixed, rsSpecializedLearning CriteriaExact, w/ FormalSpecApproximate, w/Cost FunctionOracle-GuidanceCommon (canRare (black-boxselect/design Oracle)oracles)* Between typical inductive synthesizer and machine learning algo– 88 –
Formal Inductive Synthesis Given:– Class of Artifacts C -- Formal specification – Domain of examples D– Oracle Interface O Set of (query, response) typesFind using only O an f C that satisfies – i.e. no direct access to D or Example:– C: all affine functions f of x R– : x. f(x) x 42– O {(pos-witness, (x, f(x)) satisfying )}– 89 –
Oracle Interface Generalizes the simple model of samplingpositive/negative examples from a corpusof dataLEARNERORACLE Specifies WHAT the learner and oracle do Does not specify HOW the oracle/learneris implemented– 90 –
Common Oracle Query Types(for trace property )Positive Witnessx , if one exists, else Negative Witnessx , if one exists, else Membership: Is x ?Yes / NoEquivalence: Is f ?Yes / No x fSubsumption/Subset: Is f ?Yes / No x f \ Distinguishing Input: f, X fLEARNERf’ s.t. f’ f X f’, if it exists;o.w. ORACLE– 91 –
Formal Inductive Synthesis Given:– Class of Artifacts C -- Formal specification – Domain of examples D– Oracle Interface O Set of (query, response) typesFind using only O an f C that satisfies – i.e. no direct access to D or How do we solve this?Design/Select:– 92 –
Oracle-Guided Inductive Synthesis(OGIS) A dialogue is a sequence of (query, response)conforming to an oracle interface O An OGIS engine is a pair L, T where– L is a learner, a non-deterministic algorithmmapping a dialogue to a concept c and query q– T is an oracle/teacher, a non-deterministic algorithmmapping a dialogue and query to a response r An OGIS engine L,T solves an FIS problem ifthere exists a dialogue between L and T thatconverges in a concept f C that satisfies – 93 –
Language Learning in the Limit[E.M. Gold, 1967] Concept Formal Language Class of languages identifiablein the limit if there is a learningprocedure that, for eachlanguage in that class, given aninfinite stream of strings, willeventually generate arepresentation of the language. Results:– Cannot learn regular languages,CFLs, CSLs using just positivewitness queries– Can learn using both positive &negative witness queries (assumingall examples eventually enumerated)– 94 –
Query-Based Learning[Queries and Concept Learning, 1988][Queries Revisited, 2004] First work on learning based onquerying an oracle– Supports witness, equivalence, membership,subsumption/subset queries– Oracle is BLACK BOX– Oracle determines correctness: No separatecorrectness condition or formal specification– Focus on proving complexity results forspecific concept classesDana Angluin Sample results– Can learn DFAs in poly time frommembership and equivalence queries– Cannot learn DFAs or DNF formulas in polytime with just equivalence queries– 95 –
Examples of OGIS L* algorithm to learn DFAs: counterexample-guided– Membership Equivalence queries CEGARCEGIS used in Program Synthesis/SyGuS solvers– (positive) Witness Counterexample/Verificationqueries CEGIS for Hybrid Systems– Requirement Mining [HSCC 2013]– Reactive Model Predictive Control [HSCC 2015] Two different examples:– Learning Programs from Distinguishing Inputs [Jha etal., ICSE 2010]– Learning LTL Properties for Synthesis fromCounterstrategies [Li et al., MEMOCODE 2011]– 96 –
Revisiting the ComparisonFeatureFormal mplexSimpleClassesWhat can we prove poseSpecialized ive languages)Exact, w/ ofFormal Different properties“general-Approximate, w/Learning CriteriaSpecCost Functionpurpose” learners Different properties of (non blackRare (black-boxbox) oraclesCommon (canOracle-Guidancecontrol Oracle)oracles)– 97 –
Query Types for CEGISPositive WitnessLEARNERORACLEx , if one exists, else Counterexample to f?Yes counterexample x / Finite memory vsInfinite memory Type of counterexample givenConcept class: Any set of recursive languages– 98 –
Questions Convergence: How do properties of the learnerand oracle impact convergence of CEGIS?(learning in the limit for infinite-sized conceptclasses) Sample Complexity: For finite-sized conceptclasses, what upper/lower bounds can we deriveon the number of oracle queries, for variousCEGIS variants?– 99 –
Problem 1: Bounds onSample Complexity– 100 –
Teaching Dimension[Goldman & Kearns, ‘90, ‘95] The minimum number of (labeled) examples ateacher must reveal to uniquely identify anyconcept from a concept class– 101 –
Teaching a 2-dimensional Box -- What about N dimensions?– 102 –
Teaching Dimension The minimum number of (labeled) examples ateacher must reveal to uniquely identify anyconcept from a concept classTD(C) max c C min (c) whereC is a concept classc is a concept is a teaching sequence (uniquely identifies concept c) is the set of all teaching sequences– 103 –
Theoretical Results: Num. of Queries neededfor Finite Program Classes with CEGIS Thm 1: NP-hard to find minimum number of queriesfor CEGIS oracle interface– CEGIS int. {counterexample, positive witness} Thm 2: Teaching Dimension of Program Class islower bound on query complexity– TD: min number of queries needed to uniquelyidentify any program
Formal Inductive Synthesis is Everywhere! - Many problems can be solved effectively when viewed as synthesis Particularly effective in various tasks in Formal Methods For the rest of this lecture series, for brevity we will often use "Inductive Synthesis" to mean "Formal Inductive Synthesis"
equations. The resulting theory is an improvement over previous treat-ments of inductive-inductive and indexed inductive definitions in that it unifies and generalises these into a single framework. The framework can also be seen as a first approximation towards a theory of higher inductive types, but done in a set truncated setting.
We consider inductive inference of formal languages, as defined by Gold (1967), in the case of positive data, i.e., when the examples of a given formal language are successive elements of some arbitrary enumeration of the elements . The theory of inductive inference may be viewed as an attempt to use our .
2.1 Use Inductive Reasoning Obj.: Describe patterns and use inductive reasoning. Key Vocabulary Conjecture - A conjecture is an unproven statement that is based on observations. Inductive reasoning - You use inductive reasoning when you find a pattern in specific cases and then write a conjecture for the general case. Counterex
13th Prepare inductive lesson plan Inductive grammar lesson: Direct object, indirect object, and reflexive pronouns 14th Prepare inductive lesson plan Inductive grammar lesson: relative pronouns 15thth. Composition #2: "Historia de horror" Words: 300-350 Time: 50 min. No dictionary or translation devices allowed.
A formal system consists of a collection of inductive types of terms along with inductive and coinductive relations over terms. Examples of formal systems include proof systems, such as Gentzen's inference rules for first-order logic [50], the static and dynamic semantics of programming languages [57], and process calculi [82]. In
In this paper I have discussed about grammar teaching by using inductive method, and also compared between Inductive method and Deductive Method. Inductive method is an easy and interesting method for the teachers. It is the method where the teacher would give the examples of any grammatical rules, and students would practice the examples.
We further the research into inductive logic programming and inductive con- cept learning using equational logic that was begun by Hamel [1, 2, 3] and Shen [4], as well as the inductive processes used in the functional programming system
President Judy Harris president.sydneyu3a@gmail.com VP Education Anne Richardson vpeducation.sydneyu3a@gmail.com VP Public Relations TBA Treasurer Ivona Kadlec sydu3a.treasurer@gmail.com Secretary Pamela Frei secretary.sydneyu3a@gmail.com Admin Manager Lynda Cronshaw officemgr.sydneyu3a@gmail.com Course Listing Order Course Delivery Booking a Course Insurance Principal Officers . 5. REGIONAL .
