Technische Samenvatting: Iteris: Agentic Research Loops voor Computationele Wiskunde

1. Probleemstelling

Het paper behandelt de uitdaging van het toepassen van AI op open problemen in de computationele wiskunde. In tegenstelling tot competitieproblemen of taken met een enkel doel (single-objective optimization), vereist onderzoek in dit domein een complexe wisselwerking tussen numerieke experimentatie, adversariële constructie en formele bewijsvoering. Huidige AI-systemen hebben vaak moeite met het coördineren van deze verschillende onderzoeksmodi of met het handhaven van langetermijn-onderzoekstrajecten waarbij feiten gescheiden, gecontroleerd en geherorganiseerd moeten worden.

De auteurs passen hun voorgestelde systeem, Iteris, toe op twee specifieke open problemen uit de Simons Workshop collectie [3]:

1. Probleem 2.4: Een asymptotische vergelijking tussen Conjugate Gradient (CG) en Randomized Coordinate Descent (RCD) op lineaire systemen met power-law spectra. Het doel is om een fasediagram te bepalen voor de genormaliseerde kostenratio tussen de twee methoden.
2. Probleem 4.3: Een vraag over de vraag of QR-factorisatie met kolompivoting (QRCP) betrouwbaar goed geconditioneerde submatrices selecteert uit een matrix met orthonormale rijen, specifiek onder condities van lage coherentie.

2. Methodologie: Het Iteris-systeem

Iteris is een agentic research system dat is georganiseerd als een explore–plan–execute loop. Het coördineert verschillende onderzoeksmodi via een file-gebaseerd geheugensysteem dat dient als zowel opslag voor de lange termijn als gestructureerde berichtgeving tussen agenten.

2.1 Het Agentic Protocol

Elke iteratie van het systeem volgt drie afzonderlijke fasen:

1. Explore: Een Exploration Agent voert "lichte repository-niveau probing" uit. Het leest projectbestanden, inspecteert recente iteraties en stelt ruwe redeneringen op over plausibele routes. Cruciaal is dat het niet het officiële plan schrijft, maar een adviserende registratie produceert die aanbevolen taakvormen, controles op lokale minima en risico-inschattingen bevat om te voorkomen dat het systeem zich te veel vastlegt op een stagnante tak.
2. Plan: Een Plan Agent leest de globale projectstatus (probleemstelling, roadmap, geheugen, routestatus) en het exploratieadvies. Het bepaalt de task pool voor de volgende iteratie en produceert een gestructureerde TASK_POOL.json die taalcategorieën, doelen, inputs en verificatie-eisen definieert.
3. Execute: Gespecialiseerde Execution Agents ontvangen toegewezen taken en voeren specifieke onderzoeksacties uit, waarbij zij gestructureerde resultatenbestanden terugschrijven naar het projectgeheugen.

2.2 Execution Agents

Het systeem maakt gebruik van vier categorieën execution agents, elk met taakspecifieke vaardigheden gedefinieerd door Markdown-gebaseerde capaciteitsspecificaties:

• Foundation Agent: Controleert bronnen, bevriest definities, stelt conjecture cards op en handhaaft de claim-discipline.
• Experiment Agent: Voert numeriek werk uit (test harnesses, diagnostiek, zoektochten naar tegenvoorbeelden). Bewijs wordt behandeld als richtinggevend, niet als bewijs.
• Proof Agent: Construeert en controleert bewijs-artefacten voor stabiele stellingen, speciale gevallen of lemma's.
• Review Agent: Evalueert bewijs, hiaten in bewijsvoering en de waarde van een route, en adviseert of een onderzoeksarm moet worden verdiept, geherformuleerd of ingetrokken.

2.3 Scheiding van Belangen

Een cruciaal ontwerpkenmerk is de scheiding van de Exploration Agent van de Plan Agent. Terwijl de Plan Agent de globale coherentie bewaakt, voert de Exploration Agent agressieve probes uit om "lokale inertie" (bijv. incrementele vervolgwerkzaamheden) te detecten en alternatieve richtingen voor te stellen voordat een taak officieel wordt toegezegd. Dit stelt het systeem in staat om verder te zoeken dan het huidige pad, terwijl de planning globaal coherent blijft.

3. Belangrijkste Bijdragen en Resultaten

3.1 Resultaat I: CG vs. RCD Fasediagram

Iteris werd toegepast op de vergelijking van CG en RCD op power-law spectra ($A_n = U_n \text{diag}(1^{-p}, \dots, n^{-p})U_n^*$).

• Stelling 1: Het systeem stelde een fixed-parameter fasediagram vast voor het asymptotische gedrag van de ratio $\rho_n(\epsilon, p)$ (RCD epochs vs. CG stappen) als $n \to \infty$.
• Belangrijkste Bevindingen:
  • Voor $p > 1$ (sommeerbaar spectrum) convergeert RCD in $O(1)$ epochs, terwijl CG $O(n)$ stappen nodig heeft, dus $\rho_n \to 0$.
  • Voor $p = 1$, $\rho_n \to 0$ met een logaritmische grens.
  • Voor $0 < p < 1$, wordt het gedrag bepaald door een limiterende CG-vloer $F(p)$, afgeleid van een einddimensionaal momentprobleem met betrekking tot de tail measure $\nu_p$.
  • Als de foutdrempel $\epsilon < F(p)$, vereist CG groeiende graden om te convergeren, terwijl RCD begrensd blijft, wat zorgt voor $\rho_n \to 0$.
  • Als $\epsilon > F(p)$, convergeert CG in $O(1)$ stappen terwijl RCD een positief deel van een epoch vereist, waardoor $\rho_n$ niet naar nul convergeert.
• Mens-AI Interactie: Het systeem identificeerde de fasestructuur en het "Hankel floor"-mechanisme. Echter, een initiële bewijsontwerp vertrouwde op een onterecht sterkere aanname voor de rate-analyse in het $p < 1$ regime. Menselijke experts ontdekten dit gat, en het argument werd hersteld door interactie om conservatieve, geverifieerde rate-bounds te bieden.

3.2 Resultaat II: QRCP Tegenvoorbeeld

Iteris behandelde de vraag of QRCP gegarandeerd goed geconditioneerde submatrices selecteert voor matrices met orthonormale rijen en begrensde coherentie.

• Stelling 2: Het systeem construeerde een low-coherence tegenvoorbeeldfamilie die aantoont dat QRCP kan falen in het selecteren van goed geconditioneerde submatrices, zelfs wanneer de energie van de rijen uniform gecontroleerd is.
• Belangrijkste Bevindingen: Voor elke $H^* > 1$ (coherentie-grens) en $B > 0$, bestaat er een matrix $Q$ met orthonormale rijen en coherentie $\mu(Q) < H^*$ zodanig dat de conditiegetal van de geselecteerde submatrix groter is dan $B k^e$.
• Mechanisme: Het tegenvoorbeeld maakt gebruik van een "triangular back-substitution" druk. Het systeem ontwierp een geselecteerde kernblok die voldoet aan lokale pivot-condities maar een grote inverse norm creëert. Aanvullende kolommen werden toegevoegd om de globale orthonormality te herstellen zonder door de pivoting-regel te worden geselecteerd.
• Mens-AI Interactie: Iteris identificeerde de obstructie en genereerde de constructie. Het bewijstraject was aanvankelijk omwegen; menselijke experts herorganiseerden het argument tot een leesbaar bewijs en stemden het informele theorem af met een formele Lean 4 verificatie.

4. Betekenis en Claims

Het paper beweert dat agentic AI-systemen betekenisvol kunnen deelnemen aan onderzoeksworkflows voor open problemen in de computationele wiskunde, maar benadrukt dat menselijke validatie essentieel blijft.

• Voorbij Benchmarks: Iteris laat zien dat AI verder kan gaan dan het oplossen van geïsoleerde oefeningen om deel te nemen aan echt onderzoek, door langdurige exploratieve artefacten en bewijsontwerpen te genereren.
• Workflow Integratie: Het systeem coördineert succesvol numerieke experimentatie (om structurele kenmerken zoals de Hankel floor of back-substitution pressure te identificeren) met formele bewijsconstructie.
• Rol van Menselijke Interventie: De auteurs stellen expliciet dat Iteris de menselijke inspanning verplaatst in plaats van verwijdert:
  • In het CG-geval vond het systeem de structuur, maar herstelden mensen de rate-analyse.
  • In het QRCP-geval vond het systeem het tegenvoorbeeld, maar herorganiseerden mensen het bewijs en verifieerden zij de semantische consistentie.
• Vergelijking met Directe LLM's: Directe queries aan geavanceerde modellen (bijv. GPT-Pro) produceerden plausibele heuristieken of hoog-niveau schetsen, maar faalden in het sluiten van bewijzen; ze vervaagden vaak het onderscheid tussen verwachte en waarschijnlijke bounds of behandelden plausibele stappen als voldane verplichtingen. Iteris daarentegen deelt heuristieken op in controleerbare bewijsvorderingen en gebruikt review agents om ongegronde shortcuts te blokkeren.

Het paper concludeert dat hoewel AI de zoekruimte kan vergroten en conceptuele argumenten kan produceren, het uiteindelijke wiskundige oordeel, de verificatie van aannames, de detectie van hiaten en de expositie kritische menselijke verantwoordelijkheden blijven.