Formally Solving Answer-Construction Problems in Lean

Technische Samenvatting: Formeel oplossen van problemen met antwoordconstructie in Lean

Probleemdefinitie
Wiskundige competitieproblemen vallen over het algemeen in twee categorieën: stellingbewijzen (het verifiëren van een gegeven bewering) en antwoordconstructie (het construeren van een specifiek object dat aan een eigenschap voldoet). Hoewel recente vooruitgang in Large Language Models (LLM's) de formele stellingbewijzing aanzienlijk heeft verbeteren, blijft formele antwoordconstructie onderbelicht. Er bestaat een kritieke kloof tussen informele redeneersystemen, die sterk zijn in het vermoeden van conjecturen maar zwak in formele verificatie, en formele bewijs-LLM's, die geoptimaliseerd zijn voor bewijzen maar moeite hebben met het ontdekken van de noodzakelijke getuigen (witnesses) om existentiële kwantoren te elimineren.

Een specifieke uitdaging bij het formaliseren van antwoordconstructie is admissibiliteit (toelaatbaarheid). Standaard Lean-bewijscontroleurs verifiëren dat een bewijsterm het juiste type heeft, maar dwingen niet inherent af dat de geconstrueerde getuige een canoniek, gesloten antwoord is. Bijvoorbeeld, een bewijs kan een existentiële bewering $\exists x, P(x)$ bevredigen door een niet-canonieke term terug te geven zoals sInf PropertySet (het infimum van de gedefinieerde verzameling) in plaats van een expliciet natuurlijk getal (bijv. 245). Dergelijke "circulaire" of niet-gesloten getuigen zijn wiskundig geldig binnen de logica, maar zijn niet-admissibel als wedstrijdantwoorden.

Methodologie: Enumerate-Conjecture-Prove (ECP)
Om deze uitdagingen aan te pakken, introduceren de auteurs Enumerate-Conjecture-Prove (ECP), een neuro-symbolisch framework ontworpen voor end-to-end antwoordconstructie met formele bewijzen in Lean 4. ECP scheidt het proces in afzonderlijke stadia terwijl een formele verificatielus behouden blijft:

1. Probleemformalisering & Admissibiliteitscontrole:

   • Problemen worden geformaliseerd als functiesynthesetaken: het vinden van een functie $\Psi$ zodanig dat $\forall X, P(X) \to Q(X, \Psi(X))$.
   • Een admissibiliteitschecker is geïmplementeerd om te garanderen dat de gesynthetiseerde antwoorden alleen een vooraf gedefinieerde "admissibele vocabulaire" gebruiken (bijv. specifieke constanten, rekenkundige operatoren en standaard constructoren). Het extraheert structureel semantische constanten uit de Lean-term en filtert administratieve constanten (zoals typeclass-instanties of compiler-gegenereerde artefacten) en niet-canonieke definities (zoals sInf) eruit.

2. Enumerate Stage (Tool-Assisted Exploration):

   • Een algemeen doel-LLM (bijv. GPT-5.4) wordt uitgerust met Python-tool execution-mogelijkheden.
   • De LLM schrijft en voert Python-code uit om een begrensde enumeratie over kleine domeinen uit te voeren om tuples te vinden die aan de probleembeperkingen voldoen.
   • Deze uitvoeringstraces dienen als empirisch bewijs om patronen, invarianten en functionele vormen te identificeren.

3. Conjecture Stage (Answer Synthesis):

   • Gebruikmakend van het bewijs uit de Enumerate-fase synthetiseert dezelfde algemene LLM een kandidaat-antwoordfunctie $\Psi'$.
   • De kandidaat ondergaat twee filters voordat deze verder gaat:
     • Syntactische Verificatie: De term moet compileren in Lean met het juiste type.
     • Admissibiliteitsverificatie: De term mag alleen constanten uit de toegestane vocabulaire gebruiken.
   • Als een kandidaat faalt, iterreert het systeem met de foutmelding opgenomen in de prompt.

4. Prove Stage (Formal Verification):

   • Zodra een geldige kandidaat $\Psi'$ is geconstrueerd, probeert het systeem de geïnstantieerde stelling $Stmt(T)|_{\Psi=\Psi'}$ te bewijzen.
   • Refutatie-loop: Voordat er een bewijs wordt geprobeerd, probeert het systeem de kandidaat te weerleggen door de negatie te bewijzen. Als de weerlegging slaagt, wordt de kandidaat verworpen en keert het systeem terug naar de Conjecture-fase.
   • Bewijsgeneratie: Als de weerlegging mislukt, probeert het systeem de positieve bewering te bewijzen met een combinatie van de ingebouwde automatisering van Lean (tactieken zoals simp, aesop, ring, norm_num) en een gespecialiseerde prover LLM (bijv. Goedel-Prover-V2). Als automatisering faalt, wordt de prover LLM aangeroepen met een reparatieloop om het bewijs te genereren of te herstellen.

Belangrijkste Bijdragen

• Framework voor Antwoordconstructie: ECP is het eerste framework dat antwoordconstructie expliciet scheidt van bewijsgeneratie, terwijl het admissibiliteitsbeperkingen afdwingt binnen een formele verificatielus.
• Handhaving van Admissibiliteit: Het paper introduceert een structurele methode om niet-canonieke getuigen (bijv. circulaire definities) eruit te filteren die standaard Lean-checkers anders zouden accepteren, waardoor wordt gegarandeerd dat de output overeenkomt met de wedstrijdvereisten.
• Neuro-Symbolische Integratie: Het framework combineert effectief de exploratieve redenering van algemene LLM's met Python-tools en de rigoureuze bewijskracht van gespecialiseerde prover LLM's.
• Autoformalizatie: De auteurs hebben 75 problemen uit de 2026 MathArena Final Answer Comps (AIME, HMMT, APEX) geautoformaliseerd en 346 antwoordconstructieproblemen van PutnamBench, waarmee ze een nieuwe evaluatiestandaard voor dit type probleem hebben gecreëerd.

Experimentele Resultaten
Het systeem werd geëvalueerd op MathArena 2026 (75 problemen) en PutnamBench (346 problemen) tegenover baselines bestaande uit directe bewijsgenererende LLM's (GPT-5.4, Goedel-Prover-V2).

• End-to-End Prestaties: ECP presteerde beter dan directe bewijsgenererende baselines.
  • MathArena: ECP loste 18/75 problemen op (Pass@32), vergeleken met 13/75 voor de beste LLM-only baseline (GPT-5.4).
  • PutnamBench: ECP loste 17/346 problemen op (Pass@32), vergeleken met 8/346 voor GPT-5.4 en 7/346 voor Goedel-Prover-V2-32B.
• Antwoord-Alleen Nauwkeurigheid: Tool-ondersteunde antwoordconstructie verbeterde de nauwkeurigheid van de algemene LLM's bij het genereren van correcte kandidaten aanzienlijk. Voor GPT-5.4 verhoogde het gebruik van tools de correcte antwoordconstructie op PutnamBench van 290/346 naar 303/346.
• Impact van Admissibiliteit: Analyse toonde aan dat veel door baselines gegenereerde bewijzen Lean-compileerbaar waren, maar onadmissibele antwoorden bevatten (bijv. circulaire getuigen). De expliciete admissibiliteitscheck van ECP was cruciaal om deze eruit te filteren.
• Ablatie-studies:
  • Het verwijderen van de prover LLM-correctiestap verminderde de prestaties op MathArena (18 $\to$ 16) en PutnamBench (17 $\to$ 16).
  • Het verwijderen van Lean-automatisering had een zware impact op MathArena (18 $\to$ 11) maar minder op PutnamBench in de specifieke run, wat suggereert dat MathArena-problemen meer leunen op automatiseringstactieken terwijl PutnamBench meer leunt op de capaciteit van de prover.
  • Het gebruik van een kleinere prover (8B) behield de MathArena-prestaties maar deed de PutnamBench-resultaten aanzienlijk dalen (17 $\to$ 7), wat aangeeft dat Putnam-problemen meer beperkt zijn door de zoektocht naar bewijzen (proof-search).

Betekenis en Claims
Het paper claimt dat ECP er succesvol in is geslaagd de kloof te overbruggen tussen informele antwoordgeneratie en formele stellingbewijzing. Door expliciet de "antwoordconstructiefase" te behandelen en admissibiliteit af te dwingen, lost ECP instanties op die momenteel onbereikbaar zijn voor directe bewijsgenererende benaderingen. De auteurs benadrukken dat hun aanpak bijzonder effectief is voor problemen die de constructie van een specifieke getuige vereisen (existentiële kwantificatie) in plaats van alleen het verifiëren van een vaste conclusie.

Het werk benadrukt dat huidige formele benchmarks vaak de moeilijkheid van antwoordconstructie weglaten, door te focussen op "met-antwoord"-versies van problemen. ECP demonstreert dat het combineren van algemene LLM's met tool execution voor enumeratie, gevolgd door gespecialiseerde prover LLM's voor verificatie, een levensvatbare weg is naar het oplossen van complexe, open eindige wiskundige problemen in formele systemen. De auteurs merken beperkingen op met betrekking tot het heuristische karakter van de labeling van de admissibele vocabulaire en de potentiële combinatorische explosie in de enumeratiefase voor zeer complexe combinatoriekproblemen.