Technische Samenvatting: Schalen van Testtijd-Berekening voor Natuurlijke Taal-Gebaseerde Grafen voor Geautomatiseerd Bewijzen van Stellingen

Probleemstelling

Hoewel Large Language Models (LLM's) vaardigheden hebben aangetoond in meerstaps logisch redeneren, blijft geautomatiseerd bewijzen van stellingen een uitdaging. Specifieke hindernissen zijn de accurate identificatie van sleutelwiskundige concepten, het begrijpen van hun onderlinge relaties en het correct formaliseren van bewijzen binnen natuurlijke taal of formele systemen. Bestaande benaderingen vertrouwen vaak op intensieve fine-tuning, expertiteratie of training op grote hoeveelheden formele data (bijv. Lean), wat resource-intensief kan zijn en de mogelijkheid van het model beperkt om bredere, informele wiskundige kennis te benutten. Bovendien kunnen puur formele benaderingen moeite hebben met de flexibiliteit van natuurlijk redeneren, terwijl puur natuurlijke taalbenaderingen te maken krijgen met ambiguïteit bij de vertaling naar formele verificatiesystemen.

Methodologie: KG-Prover

De auteurs introduceren KG-Prover, een nieuw raamwerk dat algemene LLM's verrijkt met een kennisgrafiek (KG) die is gewonnen uit betrouwbare wiskundige teksten (specifiek ProofWiki) om bewijzen te construeren en te formaliseren. Het systeem werkt zonder aanvullende fine-tuning van de basis-LLM, maar vertrouwt in plaats daarvan op schaling van testtijd-berekening en retrieval-augmented generation.

Kerncomponenten

1. Constructie van de Kennisgrafiek:

   • Bron: De grafiek wordt gebouwd door ProofWiki te parseren, waarbij knopen worden geëxtraheerd uit naamruimten zoals "Definition", "Axiom" en "Proof".
   • Structuur: Elke knoop vertegenwoordigt een zelfstandige wiskundige bewering (bijv. een stellingpropositie of definitie). Randen vertegenwoordigen hyperlinks die in de tekst worden aangetroffen, en vangen afhankelijkheden en conceptuele relaties op.
   • Schaal: De resulterende grafiek bevat meer dan 60.000 knopen en 300.000 randen.
   • Embeddings: Knopen worden verrijkt met vooraf berekende embeddingvectoren (met text-embedding-3-large) om semantische retrieval te faciliteren.

2. Inferentiepijplijn:

   • Retrieval & Traversie: Gegeven een propositie $P$, berekent het systeem de embedding en haalt de $k$ meest vergelijkbare knopen op. Als de eerste bewijspoging faalt, breidt het systeem de context iteratief uit door de grafiek te traverseren tot diepte $d$, waarbij de $k$ beste buren van eerder bezochte knopen worden geselecteerd.
   • Generatie van Informele Bewijzen: De LLM genereert een informeel, natuurlijk taalbewijs met behulp van de opgehaalde context. Dit maakt gebruik van de emergente redeneervermogens van het model en het brede corpus aan informele bewijzen dat beschikbaar is in de KG.
   • Autoformalisatie: Een apart model (DeepSeek-Prover-V1.5) vertaalt het informele bewijs naar Lean 4-code.
   • Verificatie & Verfijning: De gegenereerde Lean-code wordt geverifieerd met de Lean 4-stellingbewijzer. Als verificatie faalt, worden foutberichten teruggekoppeld naar de autoformalizer voor verfijning. Als het bewijs nog steeds faalt, kan het systeem de traversiediepte van de grafiek verhogen of zoekstrategieën toepassen.

3. Schalingsstrategieën (Testtijd-Berekening):

   • Best-of-N: Het systeem genereert $n$ onafhankelijke informele bewijzen, formaliseert deze automatisch en gebruikt een dedicated "judge"-model om ze te scoren op basis van correctheid en duidelijkheid, waarbij de kandidaat met de hoogste score wordt geselecteerd.
   • Beam Search: Bewijskandidaten worden georganiseerd in een beam met breedte $w$. Bij elke stap worden kandidaten uitgebreid op basis van feedback van de verifiër, gescoord en worden de top-$k$ bewaard voor de volgende iteratie. Dit balanceert exploratie van diverse bewijspaden met verificatie-gedreven verfijning.

Belangrijkste Bijdragen

• KG-Prover Raamwerk: Een systeem dat generatie van informele bewijzen in natuurlijke taal integreert met iteratieve, kennisgrafiek-gebaseerde traversie en een LLM-as-a-judge-mechanisme, waardoor de behoefte aan gespecialiseerde training of expertiteratie wordt geëlimineerd.
• Grootschalige Wiskundige KG: De constructie van een kennisgrafiek uit ProofWiki met meer dan 60.000 knopen en 300.000 randen, die complexe relaties tussen wiskundige concepten modelleert.
• Iteratief Verfijningssysteem: Een heuristische evaluatie en beam search-mechanisme dat de prestaties verbetert met tot 26,4% ten opzichte van baselines en 21,8% ten opzichte van niet-schalende KG-Prover-configuraties.
• Demonstratie van Testtijd-Schaling: Bewijs dat het moduleren van de traversiediepte van de grafiek en het toepassen van zoekstrategieën (Best-of-N, Beam Search) de prestaties aanzienlijk verhoogt zonder de onderliggende modellen opnieuw te trainen.

Experimentele Resultaten

Het raamwerk werd geëvalueerd op drie benchmarks: miniF2F-test, ProofNet en MUSTARDSAUCE.

• Prestatiewinst:

  • KG-Prover presteerde consistent beter dan baselinesystemen en standaard Retrieval-Augmented Generation (RAG) over alle datasets.
  • Verbeteringen varieerden van 2% tot 11% ten opzichte van baselines over meerdere modellen (Llama 3.1 8B, GPT-4o, o1-mini, enz.).
  • Op miniF2F-test verbeterden algemene LLM's met tot 21% wanneer ze werden gecombineerd met KG-Prover.
  • De configuratie van KG-Prover met o4-mini behaalde een 50% slaagkans op miniF2F-test.
  • In de hoogste schalingsconfiguratie reikten de verbeteringen tot 26,4% ten opzichte van baselines.

• Schalingseffecten:

  • Traversiediepte: De nauwkeurigheid nam toe met een grotere traversiediepte ($r$), vooral voor kleinere parametermodellen zoals Llama 3.1 8B. De eerste paar toenames in diepte leverden de meest significante winsten op.
  • Zoekstrategieën: Het combineren van de KG met Beam Search en Best-of-N-sampling verbeterde de nauwkeurigheid verder, met resultaten tot 10,75% op ProofNet en 50,40% op MUSTARDSAUCE.
  • Finetuned Modellen: Zelfs wanneer toegepast op modellen die al zijn gefinetuned voor Lean (bijv. TheoremLlama, DeepSeek-Prover-V1.5), bood KG-Prover extra prestatiewinst (bijv. +1,85% ten opzichte van een gefinetuned baseline op miniF2F).

Betekenis en Claims

Het artikel stelt dat KG-Prover een veelbelovende, schaalbare aanpak biedt voor geautomatiseerd bewijzen van stellingen die geen aanvullende fine-tuning of intensieve expertiteratie vereist. Door gebruik te maken van de ingebouwde redeneervermogens in natuurlijke taal van algemene LLM's en deze te verrijken met gestructureerde, via grafiek opgehaalde informatie, overbrugt het raamwerk effectief de kloof tussen informeel redeneren en formele verificatie.

De auteurs benadrukken dat deze methode bestaande foundation-modellen in staat stelt prestaties te bereiken die vergelijkbaar zijn met of zelfs beter zijn dan die van gespecialiseerde, gefinetunde systemen, simpelweg door gerelateerde concepten tijdens inferentie in te brengen. Het werk onderstreept het potentieel van testtijd-berekeningsschaling – het moduleren van de traversiediepte van de grafiek en het toepassen van zoekstrategieën – als een haalbaar alternatief voor het schalen van modelparameters voor complexe redeneertaken. Hoewel de aanpak uitdagingen introduceert in de stap van informeel naar formeel vertalen, mitigeert het twee-agentensysteem (generatie + autoformalisatie), ondersteund door grafiekretrieval, deze problemen succesvol en biedt het interpreteerbare redeneersporen en nieuwe strategieën voor bewijsgeneratie.