Kan vi vara säkra på att datorn har rätt?
Visste du att du troligtvis konstant använder en dator för att lösa optimeringsproblem? Det gör du till exempel då du kollar upp snabbaste vägen in till stan på din mobil. Men kan du lita på att förslaget är det bästa möjliga? Den här artikeln beskriver en forskningsprocess där en algoritm, som bevisar kvaliteten på sina resultat, utvecklades.
Introduktion
Har du någonsin fått en automatisk rekommendation för den för dig mest intressanta filmen att se på en streamingtjänst? Har du någonsin kollat upp snabbaste vägen in till stan på din mobil? Då har du använt en dator för att lösa ett optimeringsproblem. Optimeringsproblem är vanliga inom många branscher. Förmågan att effektivt lösa dem kan spara tid, pengar, eller andra resurser i många tillämpningar. Detta motiverar utvecklingen av effektiva optimeringsalgoritmer för att lösa dem. Den främsta utmaningen inom forskningen i optimeringsalgoritmer kommer från att de flesta av de optimeringsproblem vi är intresserade av att lösa är väldigt svåra. En enkel algoritm, som bara prövar alla möjligheter, skulle ta en dator miljontals år att köra. Därmed består de flesta optimeringsalgoritmer som används i praktiken av otaliga, komplexa delar.
Vårt arbete motiveras av komplexiteten av de optimeringsalgoritmer som används i praktiken, samt de betydande konsekvenser som deras resultat kan ha för många individer. Många firmor använder optimeringsalgoritmer i sin rekrytering för att bestämma vem av arbetssökandena som borde anställas. Optimeringsalgoritmer används också av många banker för att bestämma vem som får bostadslån. I USA används optimeringsalgoritmer för att bestämma vilka fångar som skall bli villkorligt frigivna1 och i många länder (inkl. Norden) används de för att hitta lämpliga mottagare för organdonationer.2
Den främsta forskningsfrågan i vårt arbete är: Hur kan vi veta att ett datorprogram som löser optimeringsproblem faktiskt hittar den bästa möjliga lösningen? Fastän det kan vara frestande att alltid lita på datorer, är det viktigt att inse att för att omvandla en optimeringsalgoritm till ett datorprogram som kan köras, måste en människa implementera den. Även om algoritmen i sig är bevisad att vara korrekt, dvs. alltid beräkna den bästa möjliga lösningen, kan dess höga komplexitet enkelt leda till att människan som implementerar den gör ett misstag och introducerar fel, som kallas för buggar. Dessa buggar kan t.ex. leda till att datorprogrammet felaktigt påstår att en arbetssökande inte borde bli anställd, fastän hen vore perfekt för jobbet. I de flesta fall är sådana buggar svåra, rentav omöjliga att märka i efterhand, speciellt för en användare som inte är bekant med optimerinsalgoritmer och hur de funkar.
Inom forskningen har det utvecklats tre huvudsakliga metoder för att öka pålitligheten av datorprogrammen som löser optimeringsproblem. Den första är testning. Om vi vet om någon person som vore en bra kandidat för jobbet, kan vi köra vårt program på den personen. Om programmet också tycker att personen passar för jobbet kan vi vara (lite) säkrare på att programmet är rätt implementerat. Dock kan vi aldrig vara helt säkra; fastän programmet ger rätt svar om person A, behöver den inte ge rätt svar om person B. Den andra metoden är formell verifiering, där vi matematiskt analyserar själva programmet för att bevisa att den inte innehåller buggar. Detta är ett kraftigt verktyg, som tyvärr endast går att använda på mycket simpla program. För tillfället vet inte forskarna hur man borde gå tillväga för att formellt verifiera de komplexa datorprogram som löser optimeringsalgoritmer i praktiken.
Den tredje metoden för att öka pålitligheten av datorprogram som löser optimeringsproblem, och den vi fokuserar på i vårt arbete, är att utöka algoritmen som programmet använder med en förmåga att producera ett matematiskt bevis för att resultatet den beräknar är den bästa möjliga.
Detta bevis kan sedan checkas skillt av en verifieringsalgoritm, som är tillräckligt simpel för att formellt verifieras. Notera att detta inte bevisar att programmet i sig inte skulle ha några buggar. Fastän beviset vi producerar för att en specifik person är en bra kandidat är rätt, kan algoritmen ändå fungera fel för andra kandidater. Poängen är, att alltid då optimeringsalgoritmen funkar fel, kommer beviset också att vara fel och den mycket simplare verifieringsalgoritmen märker det.
Hur gjordes forskningen?
Vårt arbete bestod av att utöka en existerande optimeringsalgoritm med förmågan att producera bevis för sina beräkningar. Vårt arbete bestod av både teori och praktik. Först måste vi klura ut hur man i teorin kan utöka algoritmen med bevis. Detta arbete liknade lösningen av matematikproblem i skolan, med den skillnaden att det inte fanns ett facit för oss att titta i. Vi diskuterade i grupp och tänkte oss fram till ett möjligt sätt.
Efter att teoridelen var klar började praktiken. Vi implementerade vår bevisproducerande algoritm och testade hur mycket långsammare bevisproduceringen gjorde programmet. Algoritmer som producerar bevis måste ju nämligen göra mer arbete än de som inte producerar bevis. Eftersom det för tillfället inte finns någon teori som berättar hur mycket långsammare en bevisproducerande algoritm är, måste vi helt enkelt pröva det experimentellt. Vi använde vårt program för att lösa många olika optimeringsproblem för att utvärdera hur mycket långsammare det är med bevisproducering. Dessutom testade vi hur länge det tar för en verifieringsalgoritm att checka de bevis vi producerade.
Vad hittades i forskningen?
Vi lyckades utforma teorin som behövs för att utöka en existerande optimeringsalgoritm med bevisföring. Med hjälp av vår nya bevisproduktion lyckades vi även upptäcka och fixa en bugg i ett existerande program med algoritmen, som har använts i många sammanhang.
Våra experiment visar att tilläggning av bevisproduktionen gjorde optimeringsalgoritmen 8,5 procent långsammare i medeltal. Det betyder att om ett optimeringsproblem tar 100 sekunder att lösa utan bevisproduktion, så kan vi producera både resultatet och beviset för korrekthet på 108 sekunder. Att kontrollera bevisen tog i medeltal tre gånger så länge som att producera dem. Alltså: om det tar 108 sekunder att producera ett bevis, tar det 324 sekunder att verifiera att beviset är rätt. Det är viktigt att inse att bevisproduktion är menad att användas endast i samband med optimeringsproblem, vars lösningar har betydande konsekvenser. En streamingtjänst, som snabbt vill rekommendera en film åt dig, har inte tid att vänta tre gånger längre för att få ett bevis för att rekommendationen är den bästa möjliga. Å andra sidan kan det definitivt vara värt att vänta tre gånger längre för att garanterat kunna vara säker på att man anställer den bästa möjliga personen – att vara tvungen att rekrytera på nytt senare blir nämligen mycket dyrare.
Till slut
I dagens värld används datorer och andra smarta enheter i allt fler tillämpningar. Ofta är det ganska enkelt att bara blint tro på att resultaten de producerar är korrekta, även om algoritmerna som används i moderna datasystem är mycket komplicerade och enkla att implementera fel. I vår artikel studerar vi optimeringsalgoritmer som kan producera både lösningar och bevis för sina resultat. Forskningen krävde både teoretiska och praktiska studier. För det första måste vi komma på hur man överhuvudtaget kan utvidga optimeringsalgoritmen med bevisproduktion. Sedan studerade vi ännu hurdan effekt bevisproduktion har på effektiviteten av datorprogrammet. Även om våra studier inte ännu ledde till ett datasystem som kan användas i industriella tillämpningar, är det viktigt att inse att vi presenterar en av de första sätten att ens i teorin göra bevis för optimeringsalgoritmer. Därmed hoppas vi på att teknikerna vi beskriver utvecklas vidare, blir snabbare, och förhoppningsvis mer allmänt använda i framtiden.