Technische Samenvatting: CausalForge

Probleemstelling

Het automatiseren van theoretisch onderzoek in causale inferentie staat voor een kritieke flessenhals: de betrouwbare evaluatie van gegenereerde resultaten. Hoewel Large Language Models (LLMs) snel conjecturen, bewijzen en papers kunnen genereren, hebben ze moeite met het evalueren van hun eigen juistheid. Empirische studies wijzen uit dat LLM-reviewers onbetrouwbaar zijn; ze accepteren gefabriceerde papers vaak met een frequentie die dicht bij toeval ligt en slagen er niet in om correcte van incorrecte stellingen te onderscheiden.

Alleen vertrouwen op formele verificatie (bijv. via de Lean 4 proof assistant) is onvoldoende om twee redenen:

1. Kosten: Het formaliseren van resultaten vanuit de eerste beginselen is arbeidsintensief. Geautomatiseerde ontdekking vereist een herbruikbare, geverifieerde bibliotheek van causale stellingen om te voorkomen dat de standaardtheorie voor elke run opnieuw moet worden opgebouwd.
2. Getrouwheid (Faithfulness): Een door een machine gecontroleerd bewijs garandeert dat een formele stelling volgt uit de aannames, maar het garandeert niet dat de formele stelling de beoogde wetenschappelijke claim getrouw weergeeft. Een LLM kan een type-gecontroleerd bewijs produceren voor een triviale definitie, een stelling met tegenstrijdige hypothesen, of een resultaat waarbij een onbewezen stap is vervangen door een axioma.

Methodologie: Het CausalForge-framework

CausalForge is een zelfverbeterend agentisch framework ontworpen voor het automatiseren van theoretisch onderzoek in causale inferentie. Het integreert een fundamentele formele bibliotheek met een meerfasige pijplijn die de nadruk legt op zowel de bewijs-soundness als de getrouwheid van de stellingen.

Kerncomponenten

1. Causalean (De Bibliotheek):

   • Een fundamentele Lean 4-bibliotheek met 7.035 machine-gecontroleerde declaraties die betrekking hebben op grafische modellen, structurele causale modellen (SCMs), potentiële uitkomsten, identificatie, schatting en asymptotische statistiek.
   • Opgebouwd met LLM-assistentie onder menselijk ontwerp en toezicht, biedt het een retrieval-interface voor agenten om geverifieerde primitieven (bijv. backdoor adjustment, double machine learning estimators) te hergebruiken.
   • Het handhaaft een strikte scheiding tussen de kernbibliotheek en de pijplijn-specifieke lemma's, waardoor de bibliotheek via een feedbackloop kan groeien.

2. CausalSmith (De Pijplijn):

   • Een deterministische toestandsmachine die vier fasen uitvoert: Discovery (Ontdekking), Formalization (Formalisering), Proof Construction (Bewijsconstructie) en Presentation (Presentatie).
   • Logic Graph (Logica-grafiek): Het centrale artefact is een logica-grafiek waarbij knopen stellingen vertegenwoordigen (definities, lemma's, stellingen) en randen afhankelijkheden vertegenwoordigen. Deze grafiek houdt het "kritieke pad" bij van gated nodes (onbewezen substraat) versus geciteerde nodes (geleende resultaten).
   • Discovery: Selecteert onderzoeksonderwerpen (ofwel door de gebruiker opgegeven of autonoom geselecteerd uit hiaten in de literatuur) en stelt resultaten in natuurlijke taal voor.
   • Formalization & Proof: Mapt de logica-grafiek naar Lean 4-declaraties, vult bewijslast in met behulp van Causalean-retrieval en construeert bewijzen.
   • Statement Audit (De Kerninnovatie): Een specifieke "statement match" gate die verifieert of de formele Lean 4-declaratie logisch overeenkomt met de beoogde natuurlijke-taalclaim. Dit omvat:
     • Het controleren op "onbewezen afkortingen" (bijv. sorry, admit, verborgen axioma's).
     • Het detecteren van "vacuïteit" (definities die reduceren tot True, onvervulbare hypothesen).
     • Het waarborgen van "getrouwheid" via back-translatie: het converteren van de beoogde claim naar een Lean-vormige hypothese/conclusie-lijst en het vergelijken daarvan met de formele declaratie om logische equivalentie te waarborgen (noch sterker, noch zwakker).
   • Convergence Review: Een dual-model review van de volledige bevroren grafiek vóór presentatie om afwijkingen in de betekenis van de stelling te voorkomen.

3. Zelfverbeteringsmechanisme:

   • Run Record: Elke run (geaccepteerd, gedegradeerd of gefaald) wordt gelogd. Gefaalde runs voorkomen dat toekomstige agenten doodlopende wegen opnieuw bewandelen; gedegradeerde runs verfijnen de doelstellingen voor nieuwheid.
   • Library Feedback: Wanneer een run een nieuwe, dragende lemma vereist die niet aanwezig is in Causalean, gaat het systeem over naar de "study mode" om dit te bewijzen. Zodra dit is geverifieerd en beoordeeld op herbruikbaarheid, wordt het lemma gepromoveerd naar Causalean, waardoor de bibliothek voor toekomstige runs wordt uitgebreid.

Belangrijkste Bijdragen

1. Causalean Library: Een brede, machine-gecontroleerde formalisering van de causale inferentie-toolkit (7.035 declaraties) die dient als een geverifieerde basis voor automatische ontdekking.
2. CausalSmith Pipeline: Een end-to-end systeem dat autonoom onderwerpen selecteert, resultaten voorstelt, ze formaliseert, bewijst in Lean 4 en de getrouwheid van de formele stellingen auditeert.
3. Statement Audit Mechanism: Een innovatieve aanpak om de kloof tussen formele verificatie en wetenschappelijke intentie te overbruggen. Door de logica-grafiek node-voor-node te auditeren, zorgt het systeem ervoor dat een door de kernel geaccepteerd bewijs overeenkomt met de specifieke wetenschappelijke claim die wordt gemaakt, in plaats van slechts een syntactisch geldige stelling te zijn.
4. Empirische Evaluatie: Een catalogus van 123 geregistreerde autonome onderzoeksruns, inclusocief 9 geaccepteerde resultaten die technische hiaten in de bestaande literatuur dichten.

Resultaten

Het systeem werd geëvalueerd met behulp van 123 geregistreerde runs:

• Uitkomsten: 9 runs werden geaccepteerd, 44 werden gedegradeerd (sound maar gebrek aan nieuwheid) en 70 faalden (afgewezen bij voorstel of wiskundige afleiding).
• Prestatiepatronen: Het systeem blinkt uit in Statistical Theory, Experimentation en Panel Methods, waar het erin slaagde technische hiaten te dichten (bijv. het matchen van upper bounds aan bekende lower bounds). Het had moeite met Exact Identification, Partial Identification en SCM clusters, waar de bijdrage een nieuw conceptueel idee vereist in plaats van technische verfijning. In deze gebieden produceerde het systeem vaak resultaten die wiskundig correct waren, maar reduceerden tot bekende constructies (bijv. "generieke Manski-stijl buitenste inkapseling").
• Flagship Result: Het systeem slaagde erin een minimax-kloof te dichten in de Average Treatment Effect (ATE) schatting onder hoogdimensionale discrete confounding. Het construeerde een berekenbare estimator die een $\log^2$-factor kloof sloot tussen bekende upper en lower bounds vastgesteld door Zeng et al. [54]. Dit resultaat werd machine-gecontroleerd, geaudit op statement-getrouwheid en formeel gekoppeld aan de Lean 4-ontwikkeling.
• Bibliotheekgroei: De feedbackloop heeft succesvol 13 nieuwe lemma's (bijv. Bretagnolle–Huber affinity bounds, Fano's inequality) van specifieke runs gepromoveerd naar de algemene Causalean-bibliotheek.

Betekenis en Claims

Het paper stelt dat CausalForge een nieuw vertrouwensmodel biedt voor geautomatiseerd theoretisch onderzoek door drie verschillende vragen te scheiden:

1. Proof Soundness (Bewijs-soundness): Gegarandeerd door de Lean 4-kernel.
2. Statement Faithfulness (Getrouwheid van de stelling): Geverifieerd door de statement audit (vergelijking van formele vs. beoogde claims).
3. Scientific Significance (Wetenschappelijke relevantie): Blijft een menselijk oordeel, geïnformeerd door maar niet bepaald door de nieuwheidstiers van de pijplijn.

De auteurs beweren dat dit framework de onbetrouwbaarheid van LLM-reviewers aanpakt door evaluatie te funderen in formele verificatie, terwijl het expliciet de grenzen erkent van automatisering wat betreft de betekenis van stellingen. Het systeem demonstreert dat geautomatiseerde agenten machine-gecontroleerde, getrouwe causale stellingen kunnen produceren, met name in domeinen waar technische hiaten goed gedefinieerd zijn. Het paper merkt echter bescheiden op dat het huidige systeem beperkt is in het genereren van werkelijk nieuwe conceptuele ideeën en dat de betrouwbaarheid van de LLM-gebaseerde nieuwheids- en getrouwheidsaudits verdere rigoureuze studie vereist. Het werk claimt niet de menselijke onderzoeker te vervangen, maar te dienen als een formeel gefundeerde, zelfverbeterende tool voor het verkennen van de grenzen van de causale inferentie-theorie.