Student World

(pokračování včerejšího úryvku)

Patrně nejznámějším automaticky dokázaným matematickým výsledkem (oznámeným například i v New York Times) je již uvedený důkaz Robbinsovy domněnky. Automatické dokazovače jsou často používány skupinou matematiků pracujících v teorii kvazigrup, která je soustředěna kolem dokazovače Prover9 (následník systémů Otter a také EQP, vyvíjený Williamem McCunem). Této skupině (William McCune, Ken Kunen, Michael Kinyon, Bob Veroff, J. D. Phillips a také David Stanovský z University Karlovy) se již podařilo automaticky dokázat řadu nových významných tvrzení v teorii kvazigrup (Phillips, Stanovský, 2010). William McCune spolu s kolegy použil svůj systém Otter k hledání minimálních axiomatik, nových jednoprvkových axiomatizací a řešení dalších zajímavých problémů v řadě algebraických struktur3. Výkonný rovnostní dokazovač Waldmeister byl nedávno (2007) integrován do komerčního programu Mathematica používaného patrně na většině univerzit na světě.

Použití v rámci interaktivních dokazovačů
V nedávné době se také začalo rozvíjet použití ATP v rámci větších interaktivních dokazovačů. První formálně ověřený důkaz Jordanovy věty („Rovinná uzavřená křivka, která sama sebe nikde neprotíná, rozděluje rovinu na dvě části – vnitřek a vnějšek křivky.“) byl sestrojen teprve v roce 2005 matematikem Thomasem Halesem v interaktivním systému HOL Light vyvíjeným Johnem Harrisonem z Intelu. Tento velký interaktivně vytvořený formální důkaz z rovinné topologie má zhruba 60 000 řádek a obsahuje zhruba 3000 volání automatického dokazovače zabudovaného do systému HOL Light. Bez možnosti použití ATP by dokazování takového počtu lemmat zabralo mnohem více úsilí a podstatně prodloužilo tento významný projekt, který už i tak trval špičkovému matematikovi (Hales v roce 1998 dokázal Keplerovu domněnku) deset měsíců. Automatické
dokazovače SPASS, E a Vampire byly v roce 2006 Larry Paulsonem integrovány také s dalším významným interaktivním dokazovačem Isabelle a toto propojení se stalo od té doby jednou z nejpoužívanějších dokazovacích metod v Isabelle. Patrně největší současná formální matematická knihovna vyvíjená systémem Mizar byla Josefem Urbanem převedena do logiky prvního řádu a systémy ATP byly použity k nezávislému ověření formálních Mizarových důkazů (Urban, Sutcliffe, 2007) a asistenci při jejich tvorbě a zjednodušování (Urban, 2006a), (Urban, 2006b).

Tvorba a verifikace softwaru
Tvorba a verifikace softwaru jsou ekonomicky významné aplikace automatického dokazování, které se pomalu stávají více a více používanými. V roce 2005 zveřejnil Tony Hoare (jeden ze zakladatelů formálního uvažování o programech a tvůrce tzv. Hoarovy logiky) „velkou výzvu“ (Grand Challenge, obdoba například úspěšné dřívější výzvy k prozkoumání lidského genomu) softwarové verifikace. V ní vyzývá k nahrazení současných počítačových programů programy, jejichž správnost je formálně ověřena a kterou zdůvodňuje mimo jiné i ekonomickými argumenty. V roce 1999 mezinárodní standardizační organizace (ISO a IEC) vytvořily Obecná kritéria pro bezpečnost informačních technologií (Common Criteria for Information Technology Security Evaluation – standard ISO/IEC 15408), která v sobě obsahují popis sedmi úrovní hodnocení bezpečnosti softwaru podle těchto kritérií, tzv. Evaluation Assurance Levels. Tři nejvyšší úrovně (EAL5, EAL6 a EAL7) vyžadují částečnou nebo úplnou formální verifikaci.
V říjnu 2008 byl americkou firmou Praxis dokončen a volně zveřejněn jeden z prvních projektů (Tokeneer4) plně splňujících podmínky EAL5, který si u dotyčné firmy (pro demonstraci těchto postupů) objednala americká Národní bezpečnostní agentura (NSA). Tento projekt využívá jazyk SPARK, což je verze jazyka ADA zjednodušená a upravená pro účely formální verifikace. Takové formální ověření správnosti programu je velmi podobné formálnímu ověření matematických vět (jako je například zmíněná Jordanova věta), a tedy i v tomto případě mohou automatické dokazovače podstatně usnadnit práci.
Vedle firmy Praxis a jejích projektů existuje řada dalších firem a projektů zabývajících se dnes formální verifikací softwaru. Například v Microsoftu je vyvíjený programovací systém Spec#5, který rozšiřuje jazyk C# o konstrukce potřebné k formální specifikaci a verifikaci. Tento systém je propojen s automatickým dokazovačem, který verifikační podmínky analyzuje a snaží se dokázat korektnost popsaného programu, nebo v něm najít chyby.
V americkém Národním úřadu pro letectví a kosmonautiku (NASA) je kromě verifikace softwaru také několik projektů zabývajících se přímou automatickou konstrukcí softwaru. Projekt Amphion6 používá automatické dokazovače k deduktivní konstrukci programů ze softwarových komponent. Tento projekt (a vývojové paradigma) lze použít pro řadu aplikací, jednou z nich byla například konstrukce softwaru potřebného pro planetární mise prováděné v NASA. Projekt „Certifikovatelná syntéza“ (Certifiable Synthesis) jde v tomto směru v NASA ještě dál a generuje kód navíc s anotacemi, které lze použít pro automatické dokazování různých (obvykle bezpečnostních) vlastností generovaných programů.

Verifikace hardwaru
Verifikace hardwaru je dnes patrně největší průmyslovou aplikací ATP. Firmy jako Intel, AMD, IBM a Motorola používají technologii ATP pro formální verifikaci. Například zmíněný systém HOL Light je v Intelu používán Johnem Harrisonem k verifikaci různých hardwarových řešení, třeba floating-point aritmetiky procesorů (Harrison, 2007). Nemalým impulsem k rozvoji použití formálních metod ve velkých hardwarových firmách byla právě chyba v aritmetice floating-point procesoru Intel Pentium nalezená v roce 1994, která nakonec donutila Intel k (potenciálně velmi drahé) nabídce výměny všech postižených procesorů. Obdobně jako systém HOL Light byl systém ACL2 použit k verifikaci aritmetiky floating-point procesorů AMD a k verifikaci různých vlastností procesorů ARM. Systém PVS byl použit k verifikaci procesorů sloužících k řízení letu letadel a systém Nqthm ke kompletnímu verifikovanému návrhu procesoru FM9001.

Tento text je úryvkem z knihy:
Vladimír Mařík a kolektiv: Umělá inteligence 6, Academia 2013
O knize na stránkách vydavatele

autor