Technische Samenvatting: Waarom een Agentic Theorema-bewijzer Werkt

Probleemstelling

Recente agentic theorema-bewijzers, die grote taalmodellen (LLMs) combineren met ophaalmechanismen, zoekfuncties en verifikatoren van bewijshulpmiddelen, hebben empirisch succes getoond in het genereren van geverifieerde wiskundige bewijzen. Echter, bestaande theoretische kaders worstelen om dit succes te verklaren. Klassieke bewijstheorie behandelt het bestaan van bewijzen, terwijl complexiteitstheorie zich richt op worst-case moeilijkheid. Geen van beide verklaart adequaat waarom een specifiek algoritme met hoge waarschijnlijkheid slaagt binnen een vast rekentijd-budget voor de specifieke, vertekende verdelingen van theorema's die in de praktijk worden aangetroffen (bijvoorbeeld bibliotheektheorema's, benchmark-families).

Het artikel adresseert de vraag: Wat is de waarschijnlijkheid dat een specifieke agentic bewijzer een door de verifikator geaccepteerd bewijs genereert binnen een vast budget op een gespecificeerde stroom van theorema-instanties? De auteurs betogen dat het begrijpen van deze "statistische bewijsbaarheid" essentieel is om te verklaren waarom componenten zoals ophalen, feedback van de verifikator en decompositie de prestaties verbeteren zonder in strijd te zijn met klassieke onbeslisbaarheid of worst-case ondergrenzen.

Methodologie

1. Formalisering als een Bereikbaarheids-MDP

De auteurs modelleren het formele bewijzen zoeken als een reachability Markov Decision Process (MDP) met een eindige horizon met deterministische dynamiek:

• Toestand ($X$): De huidige bewijsplicht (bijvoorbeeld een lijst met open doelen in Lean) plus feedback van de verifikator.
• Actie ($A$): Bewijzer-bewegingen zoals tactieken, inferentieregels of ophaalcommando's.
• Overgang ($F$): Een deterministische verifikator-update-map $F: X \times A \to X$. Ongeldige acties leiden naar falings-toestanden; geldige acties leiden naar nieuwe bewijstoestanden.
• Doel ($G$): De verzameling opgeloste toestanden (lege lijsten met doelen).

Deze formulering behandelt de operationele semantiek van de verifikator als de overgangskern. De auteurs bewijzen dat onder een trouwe toestandsabstractie de optimale MDP-succeskans exact overeenkomt met gewone syntactische bewijsbaarheid binnen hetzelfde budget, waarbij de logische integriteit behouden blijft terwijl statistische analyse mogelijk wordt.

2. Definitie van Statistische Bewijsbaarheid

De kernmetriek is Statistische Bewijsbaarheid ($SP^\pi_B(q_0)$), gedefinieerd als de waarschijnlijkheid dat een bewijzerbeleid $\pi$ een geverifieerd bewijs bereikt binnen $B$ verifikatoroproepen, gemiddeld over een initiële theorema-verdeling $q_0$ en de interne randomisatie van de bewijzer. Dit wordt gecontrasteerd met de optimale succeswaarschijnlijkheid $SP^*_B(q_0)$.

De auteurs houden ook de gemiddelde getrimde bewijslengte ($Len^\pi_B(q_0)$) bij, gedefinieerd als het verwachte aantal verifikatoroproepen voor succes of uitputting van het budget. Deze metriek dient als een kritische interpretatiehandle in hun grenzen.

3. Analyse van de Leerpijplijn

Het artikel analyseert een pijplijn die is afgestemd op huidige praktijk:

1. Offline Actie-Waarde Regressie: Het leren van dieptewijze actie-waardefuncties ($Q^*_t$) uit door de verifikator ondersteunde rollouts (gesimuleerde bewijzen) op een trainingsverdeling.
2. Gretig Bewijzen tijdens Testtijd: Het gebruik van de geleerde scores om de beste actie gretig te selecteren tijdens de testfase.

De analyse steunt op Aanname 3.1, die postuleert:

• Compacte concentratieverzamelingen ($C_t$) waar training en testen plaatsvinden.
• Lipschitz-continuïteit van de optimale waardenfunctie en de hypotheseklasse.
• Voldoende dekking van de toestands-actie-ruimte door de exploratieverdeling.
• Beschikbaarheid van meerdere onafhankelijke rollout-labels per query om ruis te verminderen.

Belangrijkste Bijdragen en Resultaten

1. Het Hoofdstelling (Grens voor Statistische Bewijsbaarheid)

Het centrale resultaat (Stelling 3.1) begrenst de kloof tussen de succeswaarschijnlijkheid van de geleerde bewijzer en die van de optimale bewijzer. De grens is een bezettingsgewogen som van uniforme actie-waardefouten:

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

Waarbij:

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ de waarschijnlijkheid is dat de geleerde bewijzer het probleem op stap $s$ nog niet heeft opgelost (de onopgeloste-massa-curve).
• $\epsilon_t$ de uniforme foutgrens is op de geleerde actie-waarde-schatter op diepte $t$.

Interpretatie van de Foutterm ($\epsilon_t$):
De fout decomposeert in drie componenten:

1. Benaderingsfout: Het onvermogen van de hypotheseklasse om de ware waardenfunctie weer te geven.
2. Dekkings/Geometriefout: Afhankelijk van de effectieve lokale dimensie ($d_t$) en de dekkingsconstante ($c_t$) van de trainingsverdeling.
3. Rollout-ruis: Variantie door het eindige aantal Monte Carlo-labels ($m_t$) gebruikt voor regressie.

2. De Rol van de Gemiddelde Bewijslengte

Een kerninzicht is dat de leidende complexiteitsvermenigvuldiger in de grens de gemiddelde getrimde bewijslengte van de geleerde bewijzer ($Len^{\hat{\pi}}_B(q_0)$) is.
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
Dit impliceert dat mechanismen die bewijzen verkorten (bijvoorbeeld effectieve decompositie, invoering van lemma's) de end-to-end-verlies direct verminderen, zelfs als de lokale schattingsfout van de waarde ($\bar{\epsilon}_B$) constant blijft.

3. Marginevoorwaarden en Snelle Rates

Onder een marginevoorwaarde (waarbij de kloof tussen de beste en de op één na beste actie-waarden met hoge waarschijnlijkheid voldoende groot is), verbetert de grens tot een snelle rate:
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
Dit suggereert dat het verbeteren van actie-kloven (het maken van correcte zetten duidelijk superieur aan incorrecte) convergentie significant versnelt.

4. Schalingswetten

Het artikel leidt sample-complexiteit heuristieken af. Logaritmische factoren negerend, schaalt de fout als $n^{-1/(d+2)}$, waarbij $n$ het budget voor verifikator-labels is en $d$ de effectieve lokale dimensie. Dit verduidelijkt dat winst door "schalen tijdens de testfase" kan voortkomen uit:

• Het verminderen van de effectieve horizon (kortere bewijzen).
• Het verminderen van de effectieve geometrische dimensie (better ophalen/representatie).
• Het vergroten van de actie-kloof marge.

Betekenis en Beweringen

Het artikel claimt een component-gevoelige account te bieden van waarom agentic theorema-bewijzers werken op vertekende werklasten. Het overbrugt de kloof tussen klassieke logica en statistisch leren door aan te tonen dat:

1. Feedback van de Verifikator: De bewijsbaarheid verbetert door de benaderingsfout te verminderen, de dekking te verbeteren en actie-kloven te vergroten.
2. Ophalen en Representatie: Helpt door de waardenfunctie te gladstrijken, de toestandsruimte te concentreren op lager-dimensionale regio's en slechte keuzes te snoeien om marges te vergroten.
3. Bewijsverkorting: Mechanismen zoals decompositie verminderen de "bezettingsgewichten" (gemiddelde bewijslengte), wat de primaire vermenigvuldiger van fouten in de grens is.

De auteurs benadrukken dat deze theorie niet in strijd is met worst-case moeilijkheid. In plaats daarvan verklaart het waarom agentic systemen slagen op de specifieke, gestructureerde verdelingen van theorema's die in de praktijk worden aangetroffen (bibliotheektheorema's, benchmarks), waar bewijzen kort zijn, kloven groot zijn en dekking goed is. Het kader behandelt de verifikator als een informatiekanaal en de bewijzer als een statistisch leerder die nuttige informatie extrahert onder een beperkt budget, en biedt een rigoureuze rechtvaardiging voor de engineeringkeuzes (ophalen, decompositie, verifikator-lussen) die wijdverbreid zijn in moderne agentic systemen.