Technische Samenvatting: In kaart brengen van onverkende symmetrieën via machineontdekking in combinatoriek

Probleemformulering

Het artikel behandelt een specifieke klasse van wiskundige ontdekkingsproblemen die worden geformuleerd als functieontdekking: gegeven twee verzamelingen $X$ en $Y$, vind een functie $f: X \to Y$ die rigide, exacte constraints voldoet en tegelijkertijd een eenvoudige, symbolische beschrijving toelaat. De auteurs formaliseren deze setting als Simple Learning Under Rigid Proportions (SLURP).

Bij SLURP wordt het domein $X$ gepartitioneerd in "zakken" $B_i$, en elke zak is gekoppeld aan een doeldistributie $D_i$ op de codomein $Y$. Het doel is een functie $f$ te ontdekken zodat:

1. Rigide Proportie Constraint: De uitvoer van $f$ op elke zak $B_i$ voldoet exact aan de doeldistributie $D_i$. Benaderende voldoening is onvoldoende; elke afwijking impliceert dat het probleem niet is opgelost.
2. Eenvoudseis: De functie moet worden verstrekt als een beknopte symbolische beschrijving (gesloten formule of algoritme) die binnen een redelijke tijdsbound (bijvoorbeeld polynoom) evalueerbaar is. Deze eis is fundamenteel om ervoor te zorgen dat de oplossing wiskundige structuur onthult in plaats van een triviale, willekeurige toewijzing van waarden te zijn.

De auteurs passen dit raamwerk toe op algebraïsche combinatoriek, specifiek het bestuderen van $q,t$-Narayana-polynomen $N_{n,k}(q,t)$. De kernuitdaging is om paren van eenvoudige statistieken (functies) op combinatorische objecten (niet-kruisende partities) te vinden die gezamenlijk deze polynomen genereren en om expliciete bjecties te construeren die hun symmetrie $N_{n,k}(q,t) = N_{n,k}(t,q)$ bewijzen.

Methodologie

Het artikel introduceert twee verschillende machinelearning-methoden om SLURP-instanties op te lossen:

1. MapSeek-Functional (Zelftrainende Benadering)

Deze methode modelleert de gewenste functie met een neurale netwerk (specifiek een Transformer-encoder) en wisselt af tussen twee stappen:

• Constraint-projectie: Gegeven het huidige model $f_\theta$, vindt het algoritme de dichtstbijzijnde functie $\hat{f}$ die exact voldoet aan de rigide proportieconstraints. Dit behelst het oplossen van een optimalisatieprobleem om de afstand tussen $f_\theta$ en de constraint-voldoende functie te minimaliseren.
• Supervised Update: De geprojecteerde functie $\hat{f}$ genereert pseudo-labels, die worden gebruikt om $f_\theta$ bij te werken via supervised training (SGD).
• Validatie: Een strijd stopcriterium wordt afgedwongen: een run is alleen succesvol als het model perfect voldoet aan de constraints op een validatieset. De grootte van de validatieset fungeert als hyperparameter om complexe of niet-interpreteerbare oplossingen te filteren.
• Distillatie: Na convergentie wordt het gedrag van het neurale netwerk handmatig of automatisch gedistilleerd tot een symbolische formule.

2. MapSeek-Symbolic (Zoekbenadering)

Deze methode zoekt direct naar symbolische formules binnen een gedefinieerde formele taal $\mathcal{L}$.

• Zoekruimte: Formules worden geconstrueerd uit een alfabet van primitieve symbolen (variabelen, rekenkundige operatoren, logische operatoren).
• Optimalisatie: Het zoekproces maakt gebruik van een Deep Cross-Entropy Method (CEM) met een generatieve Transformer-decoder. Het steekt iteratief een populatie formules, evalueert hun "afstand" (schending van constraints) en selecteert een elite subset om het generatieve model opnieuw te trainen.
• Afstandsmetriek: De afstandfunctie $\delta$ meet het $L_1$-verschil tussen de uitvoerdistributie van een kandidaatformule en de doeldistributie. De auteurs ontdekten dat het behandelen van het probleem als een classificatietaken (met een triviale metriek) effectiever was dan een regressiebenadering (met gesorteerde $L_1$-afstand).
• Stabiliteit: De auteurs merkten op dat expliciete structurele scheidingstekens (witruimte en haakjes) in de formulenotatie cruciaal waren voor trainingsstabiliteit, waardoor het voorkomen werd dat het model syntactisch geldige maar semantisch overbodige expressies genereerde.

Belangrijkste Bijdragen en Resultaten

1. Het SLURP-raamwerk en Benchmark

De auteurs formaliseren het SLURP-raamwerk en geven de skip-pairing benchmark vrij. Deze benchmark stelt de taak om statistieken op niet-kruisende partities te ontdekken die paren met de bekende "skip"-statistiek om $q,t$-Narayana-polynomen te interpreteren. De dataset bevat verfijnde constraints gebaseerd op het maximale element in niet-singuliere blokken.

2. Ontdekking van Nieuwe Statistieken

Door beide methoden toe te passen op het geval $k=3$ (partities met $n-2$ blokken), ontdekten de auteurs verschillende nieuwe, interpreteerbare statistieken:

• Mag (Magnitude): Ontdekt via MapSeek-Functional met warm-start constraints. Het paart met de skip-statistiek.
• Leap: Ontdekt via MapSeek-Functional met homogene constraints. Het paart met de skip-statistiek.
• Skew: Ontdekt via MapSeek-Symbolic. Het paart met de skip-statistiek.
• Mingarc (Min Gap Arc): Een door mensen gedefinieerde uitbreiding van de omgekeerde "skew"-statistiek, afgeleid van de ML-ontdekkingen.

3. Oplossen van een Open Probleem in Combinatoriek

Het meest significante wiskundige resultaat is de oplossing van Open Probleem 4.1 voor het geval $k=3$:

• Combinatorisch Bewijs van Symmetrie: De auteurs construeerden een expliciete uitwisselende bijectie die een partitie $\pi$ afbeeldt op $\psi(\pi)$ zodat het paar statistieken $(\text{skip}, \text{leap})$ wordt uitgewisseld: $(\text{skip}(\psi(\pi)), \text{leap}(\psi(\pi))) = (\text{leap}(\pi), \text{skip}(\pi))$.
• Dit levert het eerste combinatorische bewijs van de symmetrie $N_{n,3}(q,t) = N_{n,3}(t,q)$ via een expliciete bijectie, een probleem dat algemeen wordt beschouwd als uiterst moeilijk.
• Nieuwe Interpretatie: Het werk biedt de eerste combinatorische interpretatie van $N_{n,k}(q,t)$ voor alle $k$ in termen van niet-kruisende partities (specifiek via het $(\text{skip}, \text{mingarc})$-paar).

4. Formele Verificatie

Om reproduceerbaarheid en striktheid te waarborgen, formaliseerden de auteurs alle wiskundige ontdekkingen, inclusief de nieuwe statistieken, de bijecties en de symmetriebewijzen, in Lean 4. Zij maakten gebruik van het Aristotle-systeem om te assisteren bij autoformalisatie en bewijszoektocht, wat resulteerde in een volledig door de machine gecontroleerde verificatie van de kernresultaten.

Betekenis en Claims

Het artikel claimt de eerste te zijn die machinelearning gebruikt om voorheen onbekende combinatorische statistieken voor te stellen die vervolgens worden gebruikt om een uitwisselende bijectie te construeren die een open probleem in $q,t$-combinatoriek oplost.

• Methodologische Betekenis: De auteurs positioneren SLURP als een "bewijs-gedreven ontdekkingsraamwerk". In tegenstelling tot standaard machinelearning die benaderende generalisatie nastreeft, vereist SLURP exacte constraint-voldoening op eindige data, met als ultiem doel het vinden van eenvoudige symbolische beschrijvingen die wiskundig bewezen kunnen worden te gelden op oneindige domeinen.
• Wetenschappelijke Impact: Het werk demonstreert dat moderne ML zinvol kan bijdragen aan verifieerbare wiskundige ontdekkingen, specifiek bij het vinden van eenvoudige functies onder rigide distributieconstraints.
• Beperkingen en Toekomstig Werk: De auteurs merken bescheiden op dat terwijl het geval $k=3$ resulteerde in gesloten-formule-oplossingen, de experimenten voor $k=4$ momenteel falen tonen (bijvoorbeeld MapSeek-Functional die convergeert naar moeilijk te interpreteren oplossingen, MapSeek-Symbolic die niet de nul-afstand bereikt). Zij erkennen dat het begrijpen van de verkenning van de oplossingsruimte en het kwantificeren van "eenvoud" open methodologische uitdagingen blijven.

Het artikel concludeert dat deze tools, in handen van deskundige wiskundigen, menselijke intuïtie kunnen benutten om de reikwijdte van wiskundige ontdekking uit te breiden, met name op gebieden waar het construeren van expliciete bijecties een primaire bottleneck is.