Technische Samenvatting: Verzadigende Schaalwetten voor Equatie-ontdekking

Probleemstelling

Het artikel onderzoekt of deterministische symbolische ontdekingssystemen—specifiek die welke groeien door het toevoegen van equationale herschrijvingsregels—empirische schaalwetten gehoorzamen die analoog zijn aan die welke worden aangetroffen bij grote taalmodellen (LLM's). Hoewel schaalwetten voor neurale modellen (Kaplan et al., 2020; Hoffmann et al., 2022) goed gevestigd zijn, blijft het een open vraag of deterministische substraten, zoals die worden gebruikt in inductieve logische programmering, gelijkheidsverzadiging en programmasynthese, vergelijkbare groeidynamieken volgen. De auteurs beogen de fenomenologie van groei in deze systemen te karakteriseren, door te toetsen of een eenvoudige machtswet of een complexere verzadigende functie de accumulatie van ontdekte regels in de tijd beter beschrijft.

Methodologie

De studie hanteert een gecontroleerd experimenteel kader dat drie "toy" deterministische substraten van toenemende typecomplexiteit omvat:

1. Rekenkunde (arith): Equationale identiteiten over een getypeerde grammatica met optelling, vermenigvuldiging en vrije variabelen.
2. Booleaans (bool): Identiteiten over logische operatoren (en, of, niet).
3. Hoogste-orde Lijst (list): Een door DreamCoder geïnspireerd domein met primitieven zoals map, fold en cons.

De Ontdekkingslus:
Het systeem laat een substraat $S$ (een verzameling herschrijvingsregels) groeien over discrete stappen $t$. Bij elke stap:

• Genereert een generator kandidaat-equaties op basis van de huidige staat van $S$ (met strategieën zoals willekeurig, compositieel, frequentie-gewogen of MDL-gierig).
• Worden kandidaten getoetst op semantische geldigheid via willekeurige instantiatie.
• Worden geaccepteerde paren gegeneraliseerd (vrije variabelen worden vervangen door patroonvariabelen).
• Bepaalt een configureerbaar acceptatiefilter (ofwel "elke" of "noviteit") of de regel aan $S$ wordt toegevoegd.

Dataverzameling:
De auteurs genereerden 592 onafhankelijke ontdekkings-trajecten over deze substraten, waarbij vijf architecturale kenmerken varieerden: type generator, filterstrengheid, recursiediepte, batchgrootte en willekeurige seed. Zij maten het totale aantal regels $|S(t)|$ in de loop van de tijd.

Modelleerbenadering:
De auteurs stellen een heuristisch gemiddeld-veld-sluitingsmodel voor, afgeleid van aannames van uniforme dekking en benaderende onafhankelijkheid. Dit levert een differentiaalvergelijking voor groei op:
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
waarbij $N$ de substraatgrootte is, $k$ gerelateerd is aan de recombinatiediepte van de generator, en $\mu$ het dekkingspercentage van de kandidatenruimte voorstelt.

• Korte afstand ($\mu N \ll 1$): De vergelijking benadert een pure machtswet $N(t) \propto t^b$, waarbij $b = 1/(1-k)$.
• Lange afstand ($\mu N \gtrsim 1$): De exponentiële term induceert verzadiging, gemodelleerd door een logistisch-machtswet-vorm.

De studie past drie kandidaatmodellen (pure machtswet, uitgerekt-exponentieel, verzadigende machtswet) aan op de data met behulp van AIC voor modelselectie en gradient-boosted regressie om de exponent $b$ te voorspellen uit architecturale kenmerken.

Belangrijkste Bijdragen en Resultaten

1. Korte-afstand Machtswet-dynamiek

Over 592 trajecten heen past de groei van de substraatgrootte $|S(t)|$ op korte afstanden (tot 30 epoch) consequent een machtswet-vorm $t^b$. De exponent $b$ varieert continu tussen 0 en 1,15, afhankelijk van het domein en de architectuur.

• Architectuur-gevoeligheid: Binnen een enkel substraat is de exponent $b$ zeer gevoelig voor architecturale keuzes. Een gradient-boosted regressor die vijf architecturale kenmerken gebruikt, voorspelt $b$ met een cross-gevalideerde $R^2 \approx 0,82$ voor zowel rekenkundige/booleaanse als lijst-domeinen.
• Mislukte overdracht tussen substraten: Een model dat is getraind om $b$ te voorspellen op rekenkundige en booleaanse data, faalt volledig wanneer het wordt toegepast op het lijst-domein ($R^2 \approx -0,84$). De optimale architectuur voor samengestelde groei in plat-getypeerde substraten (bijv. noviteitsfilters) onderdrukt groei in hoger-orde getypeerde substraten. Dit geeft aan dat groeidynamieken substraat-voorwaardelijk zijn, niet universeel.

2. Lange-afstand Verzadigingshypothese

De auteurs toetsten of de groei uiteindelijk verzadigt zoals voorspeld door hun sluitingsmodel.

• Toy-data (Lijst-domein): Bij het uitbreiden van vijf lijst-domein trajecten naar 500 epoch wint het verzadigende machtswet-model in-sample AIC-vergelijkingen voor trajecten langer dan 200 epoch. Echter, out-of-sample forecasting (fitting op de eerste 100 epoch en voorspelling van de volgende 400) wordt in alle 5 gevallen gewonnen door de pure machtswet. De auteurs concluderen dat de toy-trajecten binnen 500 epoch feitelijk het verzadigingsregime niet bereiken; de voorkeur voor het verzadigende model in-sample is waarschijnlijk een fit-arteefact dat slecht extrapoleert.
• Real-world data (Mathlib4): Analyse van maandelijkse nieuwe .lean-bestands toevoegingen in de Mathlib4-bibliotheek (60 maanden, 9.701 bestanden) ondersteunt de verzadigende vorm. Het verzadigende model presteert beter dan de pure machtswet in out-of-sample forecasting met een factor van $\sim 7\times$ (RMSE 3.279 vs 23.896), wat suggereert dat Mathlib4 een verzadigingsregime heeft bereikt.
• Real-world data (Coq Mathcomp): Analyse van maandelijkse commits in de Coq Mathcomp-bibliotheek (129 maanden) geeft de voorkeur aan de pure machtswet. De verzadigingsparameter $\mu$ stort in tot nul, en de pure machtswet presteert beter dan het verzadigende model in out-of-sample forecasting met $\sim 67\times$. Dit suggereert dat Mathcomp nog geen verzadigingsregime heeft bereikt.

3. Fenomenologische Kaderstelling

Het artikel stelt een werkend kader voor: "Verzadigende machtswet-groei met substraat-voorwaardelijke $(k, \mu)$, waarneembaar wanneer het substraat zijn verzadigingsregime heeft bereikt." De dynamiek is voorwaardelijk op twee niveaus:

1. Architecturale parameters die de groe exponent voorspellen, worden niet overgedragen tussen verschillende substraattypen.
2. De functionele familie die groei beschrijft (pure versus verzadigende machtswet) hangt af van het specifieke levenscyclusstadium van het substraat.

Betekenis en Claims

Het artikel positioneert zichzelf als een eerste empirisch en theoretisch onderzoek naar de schaalwetten van deterministische equatie-ontdekking, en biedt een fenomenologie in plaats van een definitieve theorie.

• Bescheiden Scope: De auteurs stellen expliciet dat het bewijs beperkt is tot drie toy-substraten en twee real-world proxies (die grof zijn, gebaseerd op commit-/bestandsaantallen). Zij erkennen dat de lange-afstand toy-resultaten "consistent met, niet bevestigd" zijn vanwege het falen van out-of-sample forecasting op de toy-data.
• Kerninzicht: De primaire bevinding is dat symbolische ontdekkingsdynamieken substraat-voorwaardelijk zijn. In tegenstelling tot neurale schaalwetten die vaak universaliteit over architecturen veronderstellen, hangt het groeigedrag hier zwaar af van de specifieke "sluitingsgeometrie" (dekkingparameter $\mu$) van het type-systeem van het substraat.
• Toekomstige Richtingen: De auteurs identificeren drie concrete upgrades die nodig zijn om dit werk te tillen van "toy-fenomenologie" naar een "echt fenomeen":
  1. Replicatie op een non-toy substraat met traject-niveau granulariteit (niet alleen commit-aantallen).
  2. Succesvolle out-of-sample voorspellende forecasting voor het verzadigende model.
  3. Een theoretische afleiding van de verzadigingsparameter $\mu$ uit substraat-combinatoriek (bijv. type-entropie) om overdracht tussen substraten falsifieerbaar te maken.

Het artikel concludeert dat hoewel het kader van de verzadigende machtswet consistent is met de waargenomen data in regimes waar verzadiging aannemelijk is, het geen universele wet is voor alle symbolische ontdekingssystemen. Het werk dient als startpunt voor een potentiële "statistische mechanica van symbolische ontdekking".