Twitch: Learning Abstractions for Equational Theorem Proving

Dit paper introduceert Twitch, een tool die automatisch abstraheringen ontdekt uit mislukte of succesvolle bewijzen om de prestaties en snelheid van de equationale bewijzer Twee aanzienlijk te verbeteren.

De kern

Het Grote Raadsel: Hoe een computer wiskunde oplost

Stel je voor dat een wiskundige bewijsvoerder (zoals de computerprogramma's die in dit artikel worden besproken) een enorm labyrint moet doorkruisen om een antwoord te vinden. Dit labyrint is de "zoekruimte". Er zijn miljoenen mogelijke paden, maar slechts een paar leiden naar de uitkomst.

De meeste computers zijn erg snel, maar ze zijn ook een beetje dom. Ze kijken naar elk pad en zeggen: "Dit pad is kort, dat is lang." Ze kiezen het kortste pad. Soms werkt dit perfect, maar bij heel moeilijke problemen raken ze verdwaald in een doolhof van onbelangrijke details. Ze zien niet het grote plaatje.

Mensen kunnen dit beter. Een mens kijkt naar een bewijs en zegt: "Ah, ik zie hier een patroon! Deze vorm komt steeds terug." Dit noemen we een abstractie. Het is alsof je in plaats van elke losse steen in een muur te bekijken, zegt: "Dit is een 'vensterblok'."

Wat doet Twitch?

De auteurs van dit paper hebben een nieuw programma gemaakt, genaamd Twitch. De naam is een grapje: het is een combinatie van Twee (het bewijsprogramma) en Stitch (een ander programma dat patronen herkent).

De missie van Twitch is simpel: Leer van fouten en successen om slimme patronen te vinden.

Stel je voor dat Twitch een detective is die twee manieren heeft om te werken:

1. De "Bekende Vriend" Methode (Domain Abstractions)

Stel, je wilt een heel moeilijk wiskundig probleem oplossen over "Gordelkringen" (een soort wiskundige structuur). Je hebt geen idee hoe je moet beginnen.

• Wat doet Twitch? Het kijkt eerst naar eenvoudige problemen over Gordelkringen die al zijn opgelost.
• De Analogie: Het is alsof je een meesterkok bent die een nieuwe, ingewikkelde saus wilt maken. Je kijkt eerst naar de recepten voor de simpele soepen die je al kunt maken. Je ziet dat in al die soepen vaak "ui en knoflook" samen voorkomen. Je besluit: "Oké, ui en knoflook is een basispatroon."
• Het resultaat: Twitch pakt deze patronen (de "ui en knoflook") en zegt tegen het bewijsprogramma: "Als je een stap ziet die op dit patroon lijkt, kies die dan! Dat is waarschijnlijk belangrijk." Hierdoor vindt het programma het antwoord veel sneller.

2. De "Leer van je Fouten" Methode (Partial Proof Abstractions)

Soms heb je geen simpele voorbeelden om van te leren. Je moet het moeilijke probleem direct oplossen, en het lukt niet.

• Wat doet Twitch? Het laat het programma een tijdje proberen, ook al weet je dat het gaat falen. Het kijkt naar de "dode hoek" waar het programma vastliep.
• De Analogie: Stel je probeert een zware koffer te tillen en je valt. Je kijkt naar hoe je viel. Je ziet dat je altijd op je linkervoet struikelde als je een zware koffer vasthield. Je concludeert: "Ah, 'zware koffer + linkervoet' is een gevaarlijk patroon."
• Het resultaat: Twitch pakt dit patroon uit de mislukte poging en zegt: "Let op bij dit soort situaties!" Hierdoor kan het programma de volgende keer sneller zien waar het moet zoeken, zelfs zonder dat het het probleem al heeft opgelost.

Hoe werkt het technisch? (De "Stitch" Magie)

Het geheimzinnige onderdeel heet Stitch. Stel je voor dat je een heel lang verhaal hebt geschreven waarin je steeds dezelfde lange zin gebruikt, bijvoorbeeld: "De man met de rode hoed die naar de maan keek".

• Stitch zegt: "Wacht, dit komt 50 keer voor. Laten we dit korten tot 'Roodhoed'."
• In de wiskunde doet Stitch hetzelfde. Het kijkt naar een bewijs en zegt: "Deze ingewikkelde formule komt steeds terug. Laten we die een naam geven, bijvoorbeeld g(x)."
• Dit maakt het bewijs korter en overzichtelijker. Het bewijsprogramma (Twee) krijgt dan een "bonus" als het een stap maakt die op g(x) lijkt. Het gaat sneller.

Wat is het resultaat?

De auteurs hebben Twitch getest op een grote lijst van wiskundige puzzels (de TPTP-database).

• Snelheid: Het programma werd veel sneller. Voor sommige problemen werd de tijd gehalveerd.
• Succes: Het lukte om 12 zeer moeilijke problemen op te lossen die het programma voorheen nooit kon oplossen.
• Slimmer zoeken: In plaats van blindelings alle mogelijke paden te verkennen, weet het programma nu waar het moet kijken, omdat het de "veilige patronen" kent.

Samenvatting in één zin

Twitch is een slimme assistent die leert van eerdere (mis)lukte pogingen om patronen te vinden, en deze patronen gebruikt om een wiskundig computerprogramma te helpen sneller en slimmer de juiste weg te vinden in een doolhof van miljoenen mogelijke antwoorden.

Het is alsof je een GPS hebt die niet alleen naar de kaart kijkt, maar ook onthoudt: "Afgelopen week liep ik vast bij dit kruispunt, dus vandaag kies ik een andere route."

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Twitch: Learning Abstractions for Equational Theorem Proving" in het Nederlands.

Titel: Twitch: Het Leren van Abstrakties voor Equational Theorem Proving

Auteurs: Guy Axelrod, Moa Johansson, en Nicholas Smallbone (Chalmers University of Technology & Universiteit van Göteborg).

---

1. Het Probleem

Automatische bewijsgevers (ATP-systemen) moeten navigeren door een enorm zoekruimte van mogelijke inferenties. In bewijzen gebaseerd op saturatie (zoals in de equational theorem prover Twee) kunnen honderden miljoenen kritieke paren (critical pairs) worden gegenereerd, waarvan er slechts een klein aantal daadwerkelijk in het uiteindelijke bewijs wordt gebruikt.

• Huidige uitdaging: De heuristieken om te bepalen welke kritieke paren "interessant" zijn, zijn vaak te simpel (bijvoorbeeld gebaseerd op de grootte van de term).
• Menselijke input: Traditioneel gebruiken systemen zoals Otter menselijke richtlijnen (weighting, resonance, hint strategies) om te specificeren welke termvormen belangrijk zijn. Dit vereist echter handmatige expertise.
• Doel: Het automatisch ontdekken van interessante termvormen (abstrakties) die vaak voorkomen in relevante bewijzen, zonder menselijke tussenkomst, om de zoekrichting te sturen.

2. Methodologie

De auteurs introduceren Twitch, een systeem dat abstrakties leert door bestaande bewijzen te comprimeren. Het systeem gebruikt een bestaand hulpmiddel genaamd Stitch (oorspronkelijk ontwikkeld voor programmasynthese) om herhalende patronen te identificeren.

Kernconcept: Abstraktie als Compressie

Het idee is dat een bewijs kan worden "gecomprimeerd" door nieuwe functiedefinities in te voeren die veelvoorkomende termstructuren vervangen door kortere symbolen.

• Voorbeeld: Als de term $f(x, x)$ vaak voorkomt, kan een abstraktie $g(x) := f(x, x)$ worden gedefinieerd.
• Stitch: Dit tool zoekt naar de meest comprimerende set van functiedefinities voor een gegeven verzameling termen. Het maximaliseert de product van de grootte van de functie en het aantal keren dat deze kan worden gebruikt.

Twee Modi van Twitch

Twitch leert abstrakties op twee manieren:

1. Abstrakties uit Partiele Bewijzen (Partial Proof Abstractions):

   • Wordt gebruikt wanneer er geen andere bewijzen in hetzelfde domein beschikbaar zijn.
   • Twee probeert een moeilijk probleem $P_h$ te bewijzen totdat het time-outt.
   • Uit de gefaalde zoektocht worden "interessante" lemmata geselecteerd (gebaseerd op een score: grootte van het bewijs gedeeld door het kwadraat van de lengte van de lemma-statement).
   • Stitch wordt toegepast op de termen uit de bewijzen van deze lemmata om patronen te vinden.

2. Domein-Abstrakties (Domain Abstractions):

   • Gebaseerd op het principe van curriculum learning.
   • Het systeem analyseert een corpus van succesvolle bewijzen van "makkelijke" problemen binnen een bepaald domein (bijv. Groepstheorie).
   • Voor elk makkelijk probleem worden lokale abstrakties gegenereerd en getest op snelheidswinst.
   • De "goede" lokale abstrakties worden vervolgens samengevoegd en opnieuw door Stitch gestuurd om hogere niveau domein-abstrakties te vinden die universeel toepasbaar zijn binnen dat domein.

Implementatie in Twee

De auteurs hebben Twee uitgebreid om abstrakties natiu te ondersteunen (in plaats van ze als nieuwe axioma's toe te voegen).

• Mechanisme: Abstrakties beïnvloeden de heuristiek voor het rangschikken van kritieke paren.
• Gewichtsberekening: Als een term in een kritiek paar overeenkomt met een abstraktie, wordt het gewicht van die term verlaagd. Dit maakt de inferentie "goedkoper" en dus waarschijnlijker om geselecteerd te worden.
• Voordeel: In tegenstelling tot het toevoegen van axioma's (wat de zoekruimte kan vergroten en leiden tot meer inferenties), verandert het gebruik van abstrakties als heuristiek de zoekruimte niet, maar sturen het zoekproces alleen. Dit staat toe om veel meer abstrakties te gebruiken zonder de prestaties te schaden.

3. Belangrijkste Bijdragen

1. Automatische Generatie: Een methode om abstrakties automatisch te genereren uit zowel gefaalde bewijspogingen als succesvolle bewijzen van gerelateerde problemen.
2. Integratie met Stitch: Het toepassen van een tool voor programmasynthese (Stitch) op formele bewijzen om herbruikbare patronen te extraheren.
3. Twee Extensie: Een implementatie in de equational theorem prover Twee die abstrakties gebruikt om de zoekheuristiek te sturen zonder de zoekruimte te vergroten.
4. Validatie: Uitgebreide experimenten op de TPTP-benchmarks die aantonen dat deze aanpak zowel de snelheid verbetert als de oplossingscapaciteit vergroot.

4. Resultaten

De auteurs hebben Twitch geëvalueerd op een set van 1041 onbevredigbare unit equality (UEQ) problemen uit TPTP v9.2.1.

• Snelheidswinst:
  • Het gebruik van domein-abstrakties in combinatie met de "goal flattening" strategie van Twee leidde tot een aanzienlijke snelheidswinst. Ongeveer 25 extra problemen werden binnen 300 seconden opgelost.
  • Voor problemen die al binnen 300 seconden opgelost konden worden, werd de runtime ongeveer gehalveerd.
• Oplossen van Moeilijke Problemen:
  • Twitch slaagde erin om 12 problemen met een rating van 1 (de moeilijkste categorie, waarbij 90% van de ATP-systemen faalt) op te lossen.
  • In totaal werden 18 moeilijke problemen opgelost die Twee zonder abstrakties niet kon bewijzen binnen 1000 seconden.
  • Een specifiek voorbeeld is het probleem LAT075-1 (over de axiomatisatie van modulaire ortholattices met de Sheffer-stroke), dat van ~250s runtime teruggebracht werd tot ~32s.
• Vergelijking met Axioma's:
  • Het toevoegen van abstrakties als axioma's (definities) leidde vaak tot meer time-outs en langzamere prestaties omdat de zoekruimte te groot werd.
  • Het gebruik van abstrakties als heuristiek (zoals geïmplementeerd in Twitch) was robuuster en liet toe om meer patronen te gebruiken zonder negatieve effecten.

5. Betekenis en Toekomstperspectief

• Automatisering van Menselijke Intuïtie: Het paper toont aan dat het mogelijk is om de menselijke strategie van het identificeren van "interessante termvormen" te automatiseren. Dit vermindert de afhankelijkheid van handmatige tuning.
• Interpreteerbaarheid: In tegenstelling tot sommige machine learning-benaderingen die als "black box" werken, zijn de gevonden abstrakties expliciete, menselijk leesbare termstructuren (bijv. $f(x,x)$ als negatie). Dit maakt de bewijzen beter begrijpbaar voor wiskundigen.
• Potentieel: Hoewel het huidige systeem nog eenvoudige heuristieken gebruikt voor het selecteren van lemmata, toont het aan dat zelfs een simpele pijplijn voor het ontdekken van structuur aanzienlijke verbeteringen kan brengen in het oplossen van complexe algebraïsche problemen.
• Toekomst: De auteurs zien potentie in het verfijnen van de lemma-score, het combineren van domein- en partiele abstrakties, en het verkennen van het genereren van "hints" (sleutelschakels in een bewijs) naast abstrakties.

Conclusie: Twitch demonstreert dat het automatisch leren van abstrakties uit bewijzen een veelbelovende strategie is om de efficiëntie en kracht van equational theorem provers te verhogen, waardoor moeilijke wiskundige problemen opgelost kunnen worden die eerder onbereikbaar waren.