Maskinstøttet bevis

Maskinstøttet korrektur (eller mere tvetydigt: automatisk korrektur; en gren af automatisk fradrag ) er baseret på brugen af ​​computerprogrammer til at generere og teste matematiske beviser for logiske sætninger . I modsætning til et computersikkert forsøg er at konstruere hele det formelle bevis bestående af trin og mellemresultater.

Computerbevis

metode

Udtrykket bruges især til bevis, der har følgende skema: Først vises det, at det generelle problem P holder, hvis en anden egenskab E har, dvs. hvis P kan reduceres til E. Den afgørende faktor her er, at E kan afgøres ved at opregne en endelig mange (for det meste meget mange) sager. Reduktionen fra P til E er normalt et helt normalt, uformelt matematisk bevis. Først i næste trin kommer computeren i spil: Du skriver et program, der tæller alle sager ( genererer ) og kontrollerer derefter i hvert tilfælde, om E faktisk gælder for dem ( test ). Grundlæggende bestemmes E ved en brute force-metode . Proposition P følger af begge dele .

Indvendinger mod computerbevis

Computerbevis er f.eks. Delvis kontroversiel blandt matematikere. Ud over psykologiske og tekniske indvendinger er der også metodologiske.

  • En psykologisk indsigelse er idealet for en kort, logisk begrundelse, som enhver let kan forstå. Imidlertid bliver sådanne beviser stadig sjældnere i matematisk praksis. Den monster bevis på nuværende matematiske forskning ikke længere kan forstås af en enkelt person i alle dele (herunder de ekstra sætninger brugt).
  • En teknisk indvending er, at compileren eller hardwaren kan have fejl. Baseret på tidligere praktisk erfaring klassificeres denne indsigelse imidlertid som temmelig hypotetisk, fordi fejlene i hardware eller compilere, der hidtil er blevet kendt, for det meste ikke vedrørte heltalfunktioner eller logiske funktioner, men var mere aktive inden for området flydende aritmetik, f.eks. B. den velkendte Pentium FDIV-bug fra Intel Pentium-processoren. Imidlertid bruges hovedsagelig kun logiske og diskrete mekanismer til computerbevis. Denne risiko kan også minimeres ved gentagelser på forskellige computere og i forskellige implementeringer.
  • Metodisk problematisk er spørgsmålet om, hvorvidt programmet korrekt implementerer den underliggende algoritme, hvorvidt algoritmen opregner alle tilfælde i generere fase, og hvorvidt den test fase faktisk garanterer ejendom E for denne sag. Så der er et programbekræftelsesproblem her .

Maskinstøttet bevis

metode

Et matematisk bevis er formaliseret , dvs. H. opdelt i en sekvens af individuelle logiske trin, så de kan gengives af et computerprogram. Bevisprøvning er et universelt, eneste logikafhængigt problem, mens "generer-og-test" -algoritmer er problemspecifikke. Så der er gode grunde til, at maskinverificerede formelle beviser skal have tillid til mere end computerbevis.

Problemer og teoretiske grænser

Spørgsmålet om, hvorvidt et formelt bevis for en sætning kan konstrueres i en given logik, kaldes et beslutningsproblem . Afhængigt af den underliggende logik kan beslutningsproblemet variere fra trivielt til uløseligt. I tilfælde af propositionelogik kan problemet afgøres (dvs. et bevis kan altid genereres, hvis sætningen er logisk gyldig, ellers findes ugyldigheden), men NP-komplet . I modsætning hertil er prædikatlogik på første niveau kun halvbestemmelig, dvs. en gyldig sætning kan bevises ved hjælp af ubegrænset tid og hukommelsesressourcer, men en ugyldig sætning kan ikke altid anerkendes som sådan. Højere logik (HOL) er hverken bestemmelig eller komplet (med hensyn til såkaldte standardmodeller ).

Automatiske sætningsproverser

På trods af disse teoretiske grænser er der implementeret praktiske automatiske teoriprovere (ATP'er), der kan løse mange vanskelige problemer i disse logikker.

Der er en række vellykkede systemer, især inden for prædikatlogik på første niveau. Næsten alle disse metoder skaber beviser ved modsigelse og er teoretisk baseret på en variant af Herbrands sætning . De tilfælde, der er nødvendige for modsigelsen, genereres via forening . En første beregning af denne art er opløsningsregningen, der blev introduceret af John Alan Robinson i 1965 . Selv dagens bevis er stort set baseret på udvidelser og forbedringer af denne idé. B. superposition-beregningen . I disse beregninger udledes nye konsekvenser successivt fra et indledende sæt klausuler ved at anvende inferensregler (dvs. sættet er mættet ), indtil modsigelsen bliver eksplicit ved at udlede den åbenlyst utilfredsstillende tomme klausul.

Mens sætning bevis for sætninger fra aksiomer om inferens trin afledt og reproducere i enhver form, er matematiske bevis i modeltesten ( model kontrol ) for det meste raffinerede implementerede teknikker, der anvendes evidens stater brute-force opregne og systematisk søge i søgerum af evidens stater. Nogle systemer er også hybrider, der bruger både interaktivt bevis og modeltest.

Interaktive sætningsproverser

Et enklere, men beslægtet problem er beviskontrol , hvor et givet formelt bevis kontrolleres for at se, om det faktisk beviser en given sætning. Alt, hvad der kræves, er at kontrollere hvert eneste trin i beviset, hvilket normalt er muligt ved hjælp af enkle funktioner.

Interaktive sætningen provers , også kendt som beviser assistenter , kræver ledetråde til søgen efter beviser , der skal gives til det bevismateriale systemet ved en menneskelig bruger. Afhængig af graden af ​​automatisering kan en sætningsprover i det væsentlige reduceres til en beviskontrol eller uafhængigt udføre væsentlige dele af bevis søgningen automatisk. Interaktive bevis bruges nu til en række opgaver, hvis omfang spænder fra ren matematik til teoretisk datalogi til praktiske problemer i programverifikation .

Videnskabelige og industrielle anvendelser

Væsentlige matematiske beviser kontrolleret af interaktive sætningsprovere er beviset for firefarvet sætning af Georges Gonthier (som erstattede den ældre computersikkerhed med Appel og Haken) og det formaliserede bevis for Keplers formodning fra Flyspeck-projektet (2014). Men også automatiske sætningsprovere har i mellemtiden været i stand til at løse nogle interessante og vanskelige problemer, hvis løsning i lang tid var ukendt i matematik. Sådanne succeser har imidlertid tendens til at være sporadiske, og behandlingen af ​​vanskelige problemer kræver normalt interaktive sætningsproverser.

Den industrielle anvendelse af sætningsproverser eller modelchecks er i øjeblikket stadig primært fokuseret på verifikation af integrerede kredsløb og processorer . Da bugs med alvorlige økonomiske virkninger i kommercielle processorer blev kendt (se Pentium FDIV bug ), er deres behandlingsenheder for det meste verificeret. Sætningsproverser og modelbrikker er blevet anvendt i de nyeste processorversioner fra AMD , Intel og andre for at bevise mange kritiske operationer i dem. For nylig er sætningsprovere også i stigende grad blevet brugt til softwareverifikation; store projekter inkluderer delvis verifikation af Microsofts Hyper-V eller omfattende verifikation af L4 (microkernel) .

Tilgængelige implementeringer

Tilgængelige implementeringer til automatiske sætningsproverser er f.eks. B. Forenkle eller Alt-Ergo. Ligesom de nyere systemer Z3 eller CVC-4, de viser den (manglende) fulfillability af fremstillet på basis af afgørbare baggrund teorier (opfyldelighed modulo teorier ).

De velkendte bevis SPASS, E og Vampire er baseret på klassisk predikatlogik. Lean er et nyere system baseret på typeteori (CoC).

Eksempler på interaktive sætningsproverser er Isabelle og Coq , der bruger logik på højere niveau (henholdsvis HOL og CC).

Theorem Prover Museum er et initiativ til at bevare beviserne som vigtige kulturelle og videnskabelige artefakter til videnskabelig og historisk forskning. Det gør mange af de ovennævnte systemer tilgængelige i kildekoden.

Eksempler på bevisteknikker

litteratur

  • Thomas C. Hales Formal Proof (PDF; 524 kB), 55:11, Notices of the American Mathematical Society, 1370-1382, 2008.
  • Georges Gonthier: Formal Proof - The Four-Color Theorem , 55:11, Notices of the American Mathematical Society, 1384-1393, 2008.
  • Dirk Leinenbach, Thomas Santen: Bekræftelse af Microsoft Hyper-V Hypervisor med VCC , i: FM 2009: Formelle metoder, forelæsningsnotater i datalogi bind 5850 (2009), 806-809, 2009. doi : 10.1007 / 978-3-642 -05089-3_51 .
  • Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij, Gernot Heiser: Forbedret pålidelighed af enhedsdrivere gennem genbrug af hardwareverifikation (PDF; 225 kB).
  • M. Nakao, M. Plum, Y. Watanabe (2019) Numeriske verifikationsmetoder og computerassisterede bevis for delvis differentialligninger (Springer Series in Computational Mathematics).

Individuelle beviser

  1. ↑ a b Se gennemgangsartikel af T. Hales (2008), Formal Proof (PDF; 524 kB).
  2. ↑ John Alan Robinson: En maskinorienteret logik baseret på opløsningsprincippet . I: Journal of the ACM . Bind 12, nr. 1 , 1965.
  3. ↑ Se formel bevis - firefarvet sætning
  4. ^ Et formelt bevis på Kepler-formodningen .
  5. ↑ Dirk Leinenbach, Thomas Santen: Bekræftelse af Microsoft Hyper-V Hypervisor med VCC , i: FM 2009: Formal Methods, Lecture Notes in Computer Science Volume 5850 (2009), 806–809, 2009. doi : 10.1007 / 978-3- 642-05089-3_51 .
  6. ↑ Forbedret enhedsdriver Pålidelighed Gennem Hardware Verification Genbrug ( Memento af den originale fra 20 februar 2011 i Internet Archive ) Info: Den arkiv link blev indsat automatisk, og er endnu ikke blevet kontrolleret. Kontroller original- og arkivlinket i henhold til instruktionerne, og fjern derefter denne meddelelse. (PDF; 225 kB) @ 1@ 2Skabelon: Webachiv / IABot / ertos.nicta.com.au
  7. ^ Theorem Proving in Lean
  8. ^ Lean (fork) webredaktør
  9. ^ Theorem Prover Museum

Weblinks

Oversigtsrepræsentationer