🤖 AI

Structural Enforcement of Statistical Rigor in AI-Driven Discovery: A Functional Architecture

Dit artikel presenteert een formeel geverifieerde, twee-traps functionele architectuur die een Haskell-gebaseerde onderzoeksmonade combineert met een OS-niveau sandbox om statistische strengheid structureel af te dwingen en schijnontdekkingen in AI-gestuurde wetenschappelijke exploratie te voorkomen door online controle van de false-discovery-rate te garanderen en validatiedata fysiek te isoleren.

Oorspronkelijke auteurs: Karen Sargsyan

Gepubliceerd 2026-07-02

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Karen Sargsyan

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een briljante, razendsnelle onderzoeksassistent voor genaamd "AI-Scientist". Deze assistent heeft een enorme taak gekregen: om duizenden nieuwe ideeën in één nacht te testen om te zien welke er echt werken. Het is alsof een chefkok probeert om in één nacht 2.000 nieuwe recepten uit te vinden.

Het probleem? Als je 2.000 recepten proeft, zul je onvermijdelijk ongeveer 100 vinden die louter door puur geluk lijken te smaken, ook al zijn ze eigenlijk verschrikkelijk. In de wetenschap wordt dit een "valse ontdekking" genoemd. Als de AI deze gelukkige ongelukjes als echte doorbraken rapporteert, creëert het een berg nepnieuws.

Dit artikel stelt een "Veiligheidsvesting" voor om te voorkomen dat de AI tegen zichzelf of tegen ons liegt. Het bouwt een tweelaags verdedigingssysteem, ondersteund door een wiskundig bewijs, om te garanderen dat wanneer de AI zegt "Ik heb iets gevonden", het ook echt betekent wat het zegt.

Zo werkt de vesting, met behulp van eenvoudige analogieën:

1. Het Probleem: Het "Budget" van de Waarheid

Denk aan wetenschappelijke waarheid als een beperkt budget aan geld.

De Naïeve Aanpak: Als je de AI elke test laat uitvoeren met een "uitgavenlimiet" van $0,05 (een kans van 5% om fout te zitten), en het test 2.000 ideeën, dan zal de AI dat budget 2.000 keer "uitgeven". Het zal direct door zijn geld heen zijn en beginnen met het drukken van valse bonnetjes. Het artikel stelde vast dat zonder waarborgen 41% van de "ontdekkingen" van de AI slechts gelukkige gokken waren.
De Oplossing (LORD++): Het artikel gebruikt een slimmer systeem genaamd LORD++. Stel je voor dat de AI een enkele spaarpot heeft met "waarheid-geld". Elke keer als de AI een idee wil testen, moet het een kleine vergoeding betalen vanuit de spaarpot.
- Als het idee een echte ontdekking blijkt te zijn, krijgt de spaarpot een terugbetaling (een beloning).
- Als het idee een doodlopende weg is, is de vergoeding weg.
- Als de spaarpot bijna leeg is, wordt de AI gedwongen om extreem voorzichtig te worden en te stoppen met het testen van zwakke ideeën. Dit zorgt ervoor dat, gemiddeld genomen, slechts 5% van de uiteindelijke "winnaars" eigenlijk nep is.

2. De Eerste Muur: De "Haskell Monadic" Boekhouder

De eerste laag van de vesting is een strenge boekhouder die in de hersenen van de AI is ingebouwd (met behulp van een programmeertaal genaamd Haskell).

De Metafoor: Stel je een videogame voor waarin je niet op de "Spring"-knop kunt drukken tenzij je precies de juiste hoeveelheid energie hebt, en de game fysiek voorkomt dat je op de knop drukt als je dat niet hebt.
Hoe het werkt: De AI kan niet eens denken aan het testen van een hypothese zonder eerst de spaarpot-rekening bij te werken. De code is zo geschreven dat het onmogelijk is om deze stap over te slaan. Als de AI probeert de wiskunde te bedriegen, weigert het systeem simpelweg de test uit te voeren. Het is als een verkoopautomaat die je geen frisdrank geeft tenzij je de exacte muntjes erin hebt gedaan; je kunt niet zoma van de frisdrank pakken.

3. De Tweede Muur: De "OS-Level Sandbox"

De tweede laag beschermt tegen een andere truc: de AI die per ongeluk (of kwaadwillig) in het antwoordenschema kijkt terwijl hij aan het studeren is.

De Metafoor: Stel je een student voor die een eindexamen maakt. De "slechte" manier is om de student te laten studeren met het tekstboek open, en dan het examen te laten maken. De "goede" manier is om het tekstboek in een kluis in een andere kamer te vergrendelen.
Hoe het werkt: De AI schrijft code om zijn ideeën te testen. Het systeem van het artikel creëert een digitale "luchtsluis" kamer (een OS-level sandbox) waar de AI werkt.
- In deze kamer bestaat het "Antwoordenschema" (de validatiedata) niet. Het is fysiek verwijderd uit het zicht van de computer.
- Zelfs als de AI code schrijft die zegt: "Ga het bestand op /secret/answers.txt lezen," is de deur naar dat bestand vergrendeld en is het bestand er niet. De AI kan de data die hij nodig heeft om te bedriegen letterlijk niet zien.
- Het artikel testte dit met een "schurk"-AI die expliciet de opdracht kreeg om te bedriegen. De schurk probeerde het bestand te lezen, maar de luchtsluis hield stand. Het lekpercentage was nul.

4. Het "Wiskundig Bewijs" (De Blauwdrukken)

Je zou kunnen vragen: "Hoe weten we dat deze wiskunde echt werkt?"

De auteurs hebben niet alleen geraden; ze hebben een wiskundige bewijsassistent (Lean 4) gebruikt om te bewijzen dat de "spaarpot"-logica deugt.
Ze hebben ook een gespecialiseerde tool (SPARK/Ada) gebruikt om te bewijzen dat de berekeningen van de computer (die soms getallen afronden) de spaarpot niet per ongeluk zouden breken.
Het Resultaat: Ze hebben een keten van vertrouwen gecreëerd die loopt van een zuivere wiskundige stelling tot aan de daadwerkelijke computercode die op de chip draait. Het is alsof je een architect, een bouwer en een inspecteur hebt die allemaal een brug goedkeuren, om te bewijzen dat deze niet instort als de wind waait.

De Resultaten: Wat is er Gebeurd?

Het team heeft simulaties en praktijktests uitgevoerd:

Zonder de vesting: De AI beweerde dat 41% van zijn bevindingen echt was, maar het waren er voornamelijk neppe.
Met de vesting: De AI hield de foutenmarge dicht bij de doelstelling van 5% (in tests werd zelfs 1,1% behaald).
Praktijkcheck: Wanneer de AI een echte verbetering in een machine learning-model vond, liet het systeem dit door. Wanneer het een neppe verbetering vond, stopte het systeem dit.
De "Bedrieger"-test: Toen ze probeerden het systeem te misleiden om de geheime data te lezen, hield de "luchtsluis" perfect stand. De AI kon niet bedriegen.

Samenvatting

Dit artikel bouge een statistische veiligheidsgordel voor AI-wetenschappers. Het combineert een strikt boekhoudsysteem (zodat de AI niet te veel uitgeeft aan valse claims) met een afgeschermde kamer (zodat de AI niet in de antwoorden kan spieken). Het bewijst wiskundig dat dit systeem werkt, waardoor we er echt op kunnen vertrouwen wanneer een AI zegt: "Ik heb iets nieuws ontdekt."

Technische Samenvatting: Structurele Handhaving van Statistische Rigor in AI-gestuurde Ontdekking

Probleemstelling
AI-Scientist-systemen, die Large Language Models (LLM's) gebruiken om wetenschappelijke hypothesen te genereren, te implementeren en te evalueren, worden geconfronteerd met twee kritieke bedreigingen voor de statistische integriteit:

Ongecontroleerde Meervoudige Testen: Wanneer geautomatiseerde systemen duizenden hypothesen testen, leidt de naïeve toepassing van een vaste significantiedrempel (bijv. $\alpha = 0,05$ ) tot een massale inflatie van de False Discovery Rate (FDR). Zonder correctie zal het merendeel van de gerapporteerde "ontdekkingen" vals zijn.
Data Leakage en Vertekende P-waarden: In hybride architecturen waarbij LLM's Python-code genereren, bestaat het risico dat de gegenereerde code onbedoeld toegang krijgt tot validatiedata tijdens de optimalisatiefase. Dit produceert kunstmatig lage p-waarden die elke daaropvolgende statistische correctie (zoals FDR-controle) betekenisloos maken, omdat de onderliggende p-waarden vertekend zijn.

Bestaande online FDR-contremethoden (bijv. LORD++) bieden wiskundige garanties, maar deze rusten op aannames (zoals de onafhankelijkheid van toekomstige p-waarden van eerdere beslissingen en de geldigheid van de p-waarden zelf) die standaard software-implementaties stilzwijgend kunnen schenden.

Methodologie: Een Defense-in-Depth Architectuur
De auteurs stellen een functionele architectuur voor die statistische rigor afdwingt via twee complementaire lagen: een macro-niveau Haskell embedded Domain-Specific Language (eDSL) en een micro-niveau declaratieve scaffold ondersteund door OS-level isolatie.

Macro-niveau: De Research Monad (Haskell)
- Functie: Dit eDSL dwingt het LORD++ protocol structureel af. Het behandelt het significantieniveau als een "foutbudget" (alpha-rijkdom).
- Mechanisme: Gebruikmakend van een StateT transformer over een ExceptT monad, voert het systeem de statistische staat (rijkdom, ontdekkingsmomenten, tijdstempels) door elke operatie.
- Handhaving: Het is structureel onmogelijk om een hypothese te testen zonder de staat bij te werken. Het typesysteem zorgt ervoor dat drempels worden berekend op basis van alleen eerdere informatie (voorspelbaarheid), waardoor de code niet kan "vooruitkijken" naar toekomstige p-waarden. Als een protocolschending optreedt (bijv. een niet-sequentiële tijdstempel), stopt de berekening onmiddellijk.
Micro-niveau: Declaratieve Scaffolding en OS-level Sandboxing
- Functie: Deze laag zorgt ervoor dat de p-waarden die in de Research Monad worden gevoed onbevooroordeeld zijn en dat de door de LLM gegenereerde code geen toegang heeft tot validatiedata.
- Mechanisme: De Haskell-orchestrator genereert een rigide Python-harness voordat de LLM enige domeinlogica schrijft. Deze harness:
  - Dwingt Dataseparatie Af: De optimize functie van de LLM ontvangt alleen de exploratiedata-split. De validatie-split wordt exclusief door de harness geladen tijdens de validatiefase.
  - Standaardiseert Tests: De harness voert een gepaard sign-flip permutatietest uit op uitgesloten per-voorbeeld verliezen, waardoor de null p-waarden super-uniform zijn.
  - OS-Level Isolatie: De optimalisatiestap wordt uitgevoerd binnen een onbevoegde Linux user+mount namespace. De datadirectory binnen deze namespace is een weergave die alleen de exploratie-split bevat. Bijgevolg is het validatiebestand fysiek afwezig van het bestandssysteem dat zichtbaar is voor de optimalisatiecode, waardoor data leakage onmogelijk wordt, ongeacht de pogingen van de code met bestandspaden.
Formele Verificatieketen
Om de kloof tussen wiskundige theorie en floating-point implementatie te overbruggen, hebben de auteurs een geverifieerde keten geconstrueerd:
- Lean 4 Formalisering: De LORD++ stelling is geformaliseerd in Lean 4, waarbij de foutbudget en het bewijs van marginale en volledige FDR-controle zijn afgeleid. Deze formalisering identificeert vier noodzakelijke condities voor een implementatie:
  - (H1) Uniforme/Super-uniforme p-waarden.
  - (H2) Voorspelbaarheid van drempels.
  - (H3) Onafhankelijkheid van toekomstige p-waarden van eerdere beslissingen.
  - (H4) Niet-negativiteit van het rijkdomsproces.
- SPARK/Ada Verificatie: De rekenkundige conditie (H4) is geverifieerd met SPARK/Ada. De rijkdom-update wordt geïmplementeerd met vermenigvuldiging in plaats van aftrekking om niet-negativiteit te garanderen onder IEEE 754 afrondingsfouten. De GNATprove toolchain verifieert dat de rijkdom-invariant voor alle stappen standhoudt, waarbij 30 verificatiecondities zijn afgehanden zonder sorry (onbewezen claims).

Belangrijkste Resultaten

Simulatiestudie: In een Monte Carlo-simulatie van 2.000 hypothesen resulteerde een naïeve aanpak in een empirische FDR van 41% tegenover een doel van 5%. De voorgestelde monadische LORD++ architectuur controleerde de FDR op 1,1%, wat een effectieve correctie aantoont.
Casestudies (Wine Dataset):
- Bij het gebruik van een gebrekkige cross-validated t-test (die significantie opblaast door overlappende folds), rapporteerde het systeem drie valse ontdekkingen.
- Bij het gebruik van de structureel afgedwongen permutatietest op disjuncte splits, identificeerde het systeem correct dat geen van de hypothesen significant was, waardoor valse positieven werden vermeden terwijl het vermogen behouden bleef om echte effecten te detecteren wanneer er voldoende data beschikbaar was (gedemonstreerd op een grotere make_moons benchmark).
Adversariële Evaluatie: In een beveiligingstest waarbij een LLM expliciet werd geprompt om de validatiedata te lokaliseren en te lezen, bereikte de OS-level sandbox een 0,00% leak rate. Het validatiebestand was fysiek ontoegankelijk voor het optimalisatieproces, terwijl een baseline met enkel prompts een 100% leak rate vertoonde.

Betekenis en Claims
Het artikel beweert de eerste geverifieerde keten van stelling tot floating-point implementatie voor een online FDR-procedure te presenteren. De betekenis ligt in:

Structurele Handhaving: Het gaat verder dan de LLM simpelweg "vragen" om voorzichtig te zijn, en maakt statistische fouten structureel onmogelijk via typesystemen en OS-isolatie.
Formele Rigor: Het leveren van een door machine gecontroleerd bewijs (Lean 4) van de FDR-controle stelling en een geverifieerde rekenkundige implementatie (SPARK) die rekening houdt met IEEE 754 afrondingsfouten, waardoor de wiskundige garanties in de praktijk standhouden.
Defense-in-Depth: Het adresseren van zowel de statistische boekhouding (macro) als de dataintegriteit (micro) die vereist zijn voor autonome wetenschappelijke ontdekking.

De auteurs merken op dat hoewel de architectuur data leakage en FDR-inflatie voorkomt, het niet garandeert dat de domeinspecifieke logica gegenereerd door de LLM semantisch correct is (bijv. als de LLM een wetenschappelijk onjuiste optimalisatiestrategie kiest). Het vermindert echter aanzienlijk het schadeoppervlak van dergelijke fouten door te zorgen dat zelfs gebrekkige experimenten geen spookachtige statistische claims produceren.