[PDF] Faster Smarter Proof by Induction in Isabelle/HOL

View - Download Faster Smarter Proof by Induction in Isabelle/HOL

Previous PDF

Next PDF

FasterSmarter Proof byInductioninIsabelle/HOL

YutakaNagashima

Yale-NUSColle ge,NationalUniv ersityof Singapore

UniversityofInnsbruck

Czech Instituteof Informatics,Robotics, andCybernetics, CzechT echnicalUni versity inPrague yutaka@yale-nus.edu.sg

Abstract

Wepresent semind, arecommendation toolfor

proof byinduction inIsabelle/HOL. Giv enan in- ductiveproblem,semindproduces candidatear - guments forproof byinduction, andselects promis- ing onesusing heuristics.Our ev aluationbased on 1,095inducti veproblemsfrom22source files showsthat semindimprovestheaccurac yof rec- ommendation from20.1% to38.2% forthe most promising candidateswithin 5.0s econdsof time- out comparedto itspredecessor whiledecreasing the medianv alueofex ecutiontime from2.79sec- onds to1.06 seconds.

1 Introduction

As oursociety grew reliantonsoftware systems, thetrustw or- thiness ofsuch systemsbecame essential.One approachto developtrustworth ysystemsiscompleteformalv erification using proofassistants. Ina completeformal verification, we specify thedesired propertiesof oursystems andpro ve that our implementationsare correctin termsof thespecifications using softwaretools,called proofassistants . In manyverification projects,proofbyinduction playsa critical role.T ofacilitateproof byinduction,modernproof assistants offersub-tools,called tactics. Forexample, Is- abelle [Nipkowet al., 2002]comes withthe inducttac- tic. Usingthe inducttactic, humanproof authorscan apply proof byinduction simplyby passingappropriate arguments instead ofmanually dev elopinginductionprinciples.When choosing suchar guments,proofengineersha ve toanswer the followingthree questions: • Onwhich termsdo they applyinduction? • Whichv ariablesdothey passto thearbitraryfield to generalisethem? • Whichinduction ruledo they passto therulefield?

Fore xample,Program1defines theappend function(

and tworev ersefunctions( rev1andrev2) andpresents twow aystoprov etheir equivalencebyapplyingthe induct tactic. Notethat [],#, and[x]represent theempty list,the list constructor,andthe syntacticsug arfor x #[] , respec- tively.Program1 Equivalenceoftw ore versefunctions@ ::list)list)list [] @ys =ys | (x# xs)@ ys= x# (xs@ ys) rev1 ::list)list rev1 []= [] | rev1(x #xs) =rev1 xs@ [x] rev2 ::list)list)list rev2 []ys =ys | rev2(x #xs) ys= rev2xs (x# ys) theorem rev2xs ys= rev1xs @ys apply(induct xsys rule:rev2.induct) by auto theorem rev2xs ys= rev1xs @ys apply(induct xsarbitrary: ys)by autoThe firstproof scriptapplies computationinduction by passingrev2.inductto therulefield.rev2.induct is acustomised inductionrule, whichIsabelle automatically derivesfromthe definitionof rev2. Thesubsequent appli- cation ofautodischargesall sub-goalsproduced bythis in- duction. The secondproof scriptapplies structuralinduction onxs while generalisingys. Thisapplicationof structuralinduc- tion resultsin thefollo wingbase caseandinductionstep: base case:rev2 []ys =rev1 []@ ys induction step: 8 ys. rev2xs ys= rev1xs @ys) ! rev2 (a# xs)ys =rev1 (a# xs)@ ys where8and!represent theuni versalquantifierandim- plication, respectively.Usingtheassociativ eproperty of@, the subsequentapplication ofautofirstly transformedthe induction stepto thefollo wingintermediate goalinternally: 8 ys. rev2xs ys= rev1xs @ys) ! rev2 xs(a #ys) =rev1 xs@ (a# ys) Sinceyswasgeneralis edintheinduction hypothesis, auto

provedrev2 xs(a #ys) =rev1 (xs@ (a# ys))Proceedingsofthe Thirtieth Inter nationalJointC onferenceonArtificialI ntelligence(IJCAI-21)

1981
by consideringit asa concretecase ofthe inductionh ypoth- esis. Ifwe remov eysfrom thearbitraryfield, thesub- sequent applicationof autoleavestheinduction stepas fol- lows: rev2 xsys =rev1 xs@ ys! rev2 xs(a #ys) =rev1 xs@ (a# ys) In otherw ords,autocannot makeuseof thei nduc tionh y- pothesis sincethe conclusionof inductionstep sharethe same ys . Experiencedhuman researcherscan judgethat thisappli- cation ofthe inducttactic wasnotappropriate. Howe ver , it isals otruethatthis inductionstep isstill prov able.F orthis reason, counter-examplefinders,suchas Nitpick [Blanchette and Nipkow,2010 ]and Quickcheck[Bulwahn,2012], cannot detect thatthis inducttactic withoutgeneralisation isnot appropriate forthis problem.This iswh yengineers stillha ve to carefullye xamineinductive problemstoanswertheafore- mentioned threequestions whenusing theinducttactic. This issueis notspecific toIsa be lle:other proofassis- tants, suchas Coq [The Coqde velopmentteam,2021], HOL4 [Slind andNorrish, 2008], andHOL Light[Harrison, 1996], offersimilar tacticsfor inductiv etheorem proving,anditis human engineerswho hav etospecifythearguments forsuch tactics. Thisissue isnot triv ial either:inasummarypa- per from2005, Gramlichlisted generalisationas oneof the main problemsandc hallenges of inductivetheoremproving while predictingthat substantial progressininductivetheo- rempr ovingwilltaketime due tothe enormouspr oblemsand the inherentdifficulty ofinductivetheorem pro ving [Gram- lich, 2005

Previously,web uiltsmartinduct, whichsuggests ar-

guments ofthe inducttactic inIsabel le/HOL.Ourev alu- ation showedthatsmartinductpredicts onwhich vari- ables Isabellee xpertsapplytheinducttactic forsome in- ductiveproblems.Unfortunately ,smartinducthas the followinglimitations: L1. Ittends totak etoo longtoproducerecommendations. L2. Itcannot recommendinduction oncompound termsor induction onmultiple occurrencesof thesame variable. L3. Itis badat predictingv ariablegeneralisations. L4. Itse valuationisbasedona smalldataset with109 induc- tiveproblems.

Weo vercametheseproblemswithsemind, ane wrec-

ommendation toolfor theinducttactic. Similarlyto smartinduct,semindsuggests whatar gumentstopass to thethe inducttactic fora giv eninductiveproblem.Our overallcontribution isthat we builtasystem thatpredicts how oneshould apply proofby inductionin Isabelle/HOLboth quickly andaccurately .

Event houghwebuiltsemindfor Isabelle/HOL,ourap-

proach istransferable toother proofassistants basedon tac- tics: nomatterwhatproofassistantsweuse,weneedanarchi- tecture thataggressi velyremovesless promisingcandidates to addressL1 (presentedin Section2), aprocedure tocon- manygood onesto address L2(presented inSection3),and goal

Step 1: syntax-directed candidate construction

Step 2: filtering out unpromising tactics

Step 3: rank tactics using SeLFiE heuristics

18

18181817

20 20

1818182018

18 202018

2022
2426
28
Step 5: rank tactics using SeLFiE heuristics for generalisation

Step 4: construct generalisation variables

20201918Proceedingsofthe Thirtieth Inter nationalJointC onferenceonArtificialI ntelligence(IJCAI-21)

1982

Figure 1:The ov erviewofsemind.

domain-agnostic heuristicsthat analysenot onlythe syntactic constants toaddress L3(pr esentedin Section4).Finally, Sec- tion 5justifies ourclaims throughe xtensiv ee valuationsbased on 1095inducti veproblems,addressingL4.

2 TheOv erallArchitecture

Figure 1illustrates theo verall architectureofsemind, con- sisting of5 stepst oproduce andselectcandidatetactics as follows.

Step 1.semindproduces aset ofsequences ofinduc-

tion termsand inductionrules forthe inducttactic from a giveninductive problem.Theaimofthisstep isto produce a smallnumber ofcandidates intelligently, sothat itcovers most promisingsequences ofinduction termsand induction rules whilea voidingacombinatorialblowup. We expound the algorithmto achiev ethisgoalinSection3.

Step 2.semindapplies theinducttactic withthe se-

quences ofar gumentsproducedinStep 1to discardless promising candidates.seminddecides asequence ofar - guments isunpromising ifthe sequencesatisfies any ofthe followingconditions: • theinducttactic failswithan errormessage, or • oneof theresulting intermediategoals isidentical tothe original goalitself. Step 3.semindapplies 36pre-defined heuristicswritten in SeLFiE [Nagashima,2020a ], whichwe explain inSection

4 usingour runninge xample.These heuristicsjudgethev a-

lidity ofinduction termsand inductionrules withrespect to the proofgoal andthe relev antdefinitions. Eachheuristicis implemented asan assertionon inductiv eproblems andar- guments ofthe inducttactic, andeach assertionis tagged with av alue.Ifanassertion returnsTruefor asequence of arguments,semindgivesthetagged value tothe sequence. semindsums upsuch pointsfrom the36 heuristicsto com-

pute thescore foreach sequence.Based onthese scores,Proceedingsofthe Thirtieth Inter nationalJointC onferenceonArtificialI ntelligence(IJCAI-21)

1982

Figure 2:The user-interf aceofsemind.

semindsorts sequencesof arguments fromStep2and se- lects thefi vemostpromisingsequencesfor furtherprocess- ing. Step 4.After decidinginduction termsand inductionrules for theinducttactic inStep 3,semindadds arguments for thearbitrary fieldto thesequences ofar gumentspassed from Step3.Firstly ,semindcollects freev ariablesinthe proof goalthat arenot inductionterms foreach sequence from Step3. Then,it constructsthe powerset ofsuch free thearbitraryfield ofthe inducttactic. Forexample, if semindreceives(induct xs)from Step3 forour run- ning exampleoflist rev ersal,it produces{{}, {ys}}as the powersetbecausexsandysare theonly freev ariablesin the goaland xsappears asthe inductiont erm.This powerset leads tothe following twoinducttactics:(induct xs), and(induct xsarbitrary:ys) .

Step 5.Foreach remainingsequence, semindapplies 8

isation. Again,eachheuristic istagged witha value, whichis used tocompute thefinal scorefor eachcandidate: foreach sequence,semindadds thescore fromthe generalisation heuristics tothe scorefrom Step3 todecide thefinal scorefor each sequence.Based onthese finalscores, semindsorts sequences ofar gumentsfromStep5 andpresents the10 most promising sequencesin theOutput panelof Isabelle/jEdit,the defaultproof editorfor Isabelle/HOL [Wenzel,2012 ].

Wede velopedsemindentirely withinthe Isabelle

ecosystem withoutan ydependencyto externaltools.This allowsfor theeasy installationprocess ofsemind: touse semind, usersonly hav etodownloadtherele vant Isabelle files fromour publicGitHub repository

1and installsemind

using thestandard Isabellecommand. Theseamless integra- tion intothe Isabelleproof language,Isar [Wenzel,2002 ], lets users invokesemindwithin theirongoing proofde velop- ment andcop yarecommendedinducttactic tothe right location withone clickas shown inFigure 2.quotesdbs_dbs49.pdfusesText_49

[PDF] auto induction exercice corrigé

[PDF] auto induction formule

[PDF] auto induction pdf

[PDF] pour communiquer en français 4aep

[PDF] auto train narbonne

[PDF] auto train nice

[PDF] auto train questions

[PDF] auto train sncf

[PDF] autocad 2014 tutorial francais pdf

[PDF] autocad 2017 serial number and product key

[PDF] autodesk product key 2014

[PDF] automate easy moeller

[PDF] autonomie électrique d une maison passive

[PDF] autonomie électrique d'une maison

[PDF] autoportrait léonard de vinci