💻 computer science

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

Dit paper presenteert *FormalScience*, een mens-in-de-lus agentisch systeem dat domeinexperts helpt om complexe wetenschappelijke redeneringen (zoals natuurkunde) efficiënt en nauwkeurig te vertalen naar formeel verifieerbare Lean4-code.

Oorspronkelijke auteurs: Jordan Meadows, Lan Zhang, Andre Freitas

Gepubliceerd 2026-04-28

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Jordan Meadows, Lan Zhang, Andre Freitas

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 voor dat je een briljante natuurkundige bent die een ingewikkeld verhaal vertelt over hoe sterren branden of hoe atomen dansen. Je gebruikt prachtige tekeningen, pijltjes, Griekse letters en een soort "gevoel" voor de natuur. Dat is informele wetenschap: het is prachtig, maar het is ook een beetje "vrijblijvend". Je kunt een foutje maken in je logica zonder dat iemand het direct ziet.

Aan de andere kant heb je de formele wereld: dit is de wereld van computers en wiskundige bewijzen (zoals de taal Lean). Hier is niets toegestaan. Elke stap moet ijzersterk zijn, als een digitale ketting waar elk schakeltje perfect in elkaar grijpt. Als er één foutje in zit, blokkeert de hele machine.

Het probleem: Het is voor een computer ontzettend moeilijk om dat prachtige, rommelige verhaal van de natuurkundige om te zetten in die perfecte, strakke digitale ketting. De computer begrijpt de "vibe" van de natuurkunde niet; hij ziet alleen maar een berg vreemde tekens.

Wat hebben deze onderzoekers gedaan? (De "Vertaler-Assistent")

De onderzoekers hebben FormalScience bedacht. Zie dit niet als een robot die alles in zijn eentje doet, maar als een super-slimme vertaalmachine met een menselijke supervisor.

Stel je voor dat je een vertaler hebt die een boek van het Nederlands naar een heel ingewikkelde code-taal moet vertalen.

De Robot (AI): De AI probeert de natuurkundige tekst te vertalen naar de computer-taal.
De Controleur (De Mens): Een echte natuurkundige kijkt over de schouder mee. De AI zegt: "Ik heb het vertaald!", en de mens zegt: "Ho even, je hebt de essentie van de zwaartekracht hier veranderd in een simpele optelsom. Doe het opnieuw!"
De Correctie-lus: De AI krijgt de feedback, probeert het opnieuw, en de computer (de "solver") geeft direct aan of de code technisch gezien wel werkt.

Door dit samen te doen, hebben ze een enorme database gemaakt genaamd FormalPhysics: 200 natuurkundige puzzels die nu zowel in "mensentaal" als in "perfecte computer-taal" bestaan.

Het grote gevaar: "De Betekenis-Dief" (Semantic Drift)

Dit is het meest fascinerende deel van het onderzoek. De onderzoekers ontdekten iets geks. Soms lukt het de AI wel om een code te schrijven die de computer accepteert (de code is "geldig"), maar de betekenis is verdwenen. Ze noemen dit Semantic Drift.

Ik gebruik graag de metafoor van de "Lego-truc":

Stel je voor dat ik je vraag om een hyperrealistisch model van de Eiffeltoren te bouwen met Lego. Je bent een beetje lui, dus je bouwt in plaats daarvan gewoon een simpele, rechtopstaande toren van bruine blokjes.

De computer zegt: "Gefeliciteerd! Het is een toren, hij staat stevig en hij is niet omgevallen. Het is goedgekeurd!" (Dit is de Formele Geldigheid).
De natuurkundige zegt: "Maar dit is geen Eiffeltoren! Waar zijn de bogen? Waar is de structuur? Je hebt de essentie gestolen!" (Dit is de Betekenis-drift).

In de natuurkunde gebeurt dit ook: de AI maakt de wiskunde soms "te simpel" om de computer tevreden te stellen. Een ingewikkelde beweging van een elektron wordt dan plotseling een simpel getalletje. De computer is blij omdat de rekensom klopt, maar de natuurkunde is eigenlijk verdwenen.

Waarom is dit belangrijk?

Waarom zouden we dit willen? Omdat we in de toekomst computers willen hebben die echte wetenschappelijke ontdekkingen doen. Als we een AI willen bouwen die nieuwe medicijnen ontwerpt of nieuwe energiebronnen vindt, moet die AI niet alleen "geloofwaardig klinken", maar moet hij onweerlegbaar bewijs kunnen leveren.

Dit onderzoek is een belangrijke stap: het laat zien hoe we de brug kunnen slaan tussen de creatieve, menselijke natuurkunde en de ijzeren, logische wereld van de computer – en het waarschuwt ons dat we heel goed moeten opletten dat de computer de waarheid niet "plat slaat" om het makkelijk te maken.

Technische Samenvatting: FormalScience

1. Het Probleem: De Kloof tussen Natuurlijke en Formele Taal in de Wetenschap

Het proces van autoformalisatie — het automatisch omzetten van informele wiskundige redeneringen (zoals LaTeX) naar formeel verifieerbare code (zoals Lean4) — is een grote uitdaging voor Large Language Models (LLMs). In wetenschappelijke disciplines zoals de natuurkunde is dit probleem extra complex door:

Domeinspecifieke notatie: Concepten zoals Dirac-notatie (bra-ket) en vectorcalculus zijn niet direct ondersteund in standaard formele bibliotheken (zoals Mathlib).
Semantische Drift: Er ontstaat een kloof tussen wat de natuurlijke taal zegt en wat de formele code daadwerkelijk verifieert. Een model kan code genereren die weliswaar compileert (syntactisch correct is), maar de fysieke betekenis volledig mist (semantisch incorrect).
Hallucinaties en Complexiteit: Naarmate de wiskundige complexiteit toeneemt, neemt de betrouwbaarheid van LLM's af.

2. Methodologie: Het FormalScience Pipeline

De auteurs introduceren FormalScience, een domein-agnostisch, human-in-the-loop agentisch proces dat bedoeld is om hoogwaardige formele datasets te genereren met minimale kosten. Het proces bestaat uit vier fasen:

Informele QA-generatie: Met behulp van few-shot prompting en een menselijke expert worden uit eenvoudige vergelijkingen rijke, contextuele vraag-antwoordparen (stelling en bewijs) gegenereerd in LaTeX.
Iteratieve Code-correctie: Een agent gebruikt de Lean4-compiler als feedbackloop. Als de code niet compileert, krijgt de LLM de foutmeldingen terug om de code te verbeteren.
Menselijke Semantische Validatie: In tegenstelling tot puur automatische methoden, grijpt een menselijke expert in om te controleren of de formele code de betekenis van de natuurlijke taal nog steeds correct weergeeft. Als de alignment (overeenstemming) laag is, wordt de code opnieuw gegenereerd.
Post-processing: De uiteindelijke output is een dataset van triples $(S, P, C)$ : de natuurlijke stelling ( $S$ ), het natuurlijke bewijs ( $P$ ), en de formele Lean4-code ( $C$ ).

3. Belangrijkste Bijdragen

FormalPhysics Dataset: Een nieuwe benchmark bestaande uit 200 universiteitsniveau natuurkundeproblemen (kwantummechanica en elektromagnetisme) inclusief hun formele Lean4-representaties. Deze dataset is complexer en bevat meer wiskundige objecten dan bestaande benchmarks zoals miniF2F of ProofNet.
Karakterisering van Semantische Drift: De auteurs bieden een systematische analyse van hoe betekenis verloren gaat tijdens formalisatie. Ze identificeren vier categorieën:
- Notational Collapse: Complexe operatoren (bijv. Dirac) worden gereduceerd tot simpele scalairen.
- Abstraction Elevation: Fysieke berekeningen worden vervangen door abstracte algebraïsche eigenschappen (bijv. een integraal wordt een simpele substitutie).
- Proof Strategy Substitution: Het bewijs wordt correct uitgevoerd, maar via een totaal andere methode dan de informele tekst.
- Implicit Premise Selection: De formele taal dwingt het expliciet maken van verborgen aannames af (wat vaak een verbetering is).
Agentic Code Generation: Een nieuw framework dat gebruikmaakt van een "patch agent" die minimale wijzigingen (unified diffs) aanbrengt om semantische fouten te herstellen.

4. Resultaten

Prestaties van Modellen: De auteurs evalueerden diverse modellen. Terwijl standaard zero-shot benaderingen en eenvoudige self-refinement methoden vaak falen in het produceren van valide natuurkundige code, bereikt de agentische aanpak (GPT-OSS-20B) een validiteit van 31%.
De Alignment-Validiteit Trade-off: Een cruciale ontdekking is dat er een negatieve correlatie bestaat tussen formele validiteit (het compileren van de code) en semantische alignment. Modellen die "slimmer" proberen te compileren, neigen ernaar de fysica te abstraheren of te versimpelen om de compiler te pleasen, waardoor de fysieke inhoud verloren gaat.
Efficiëntie: De FormalScience-pipeline stelt een enkele expert in staat om in één maand tijd een hoogwaardige dataset te bouwen voor een fractie van de kosten van traditionele methoden.

5. Betekenis en Impact

Dit werk is significant omdat het aantoont dat formele validiteit alleen niet voldoende is voor wetenschappelijke verificatie. Het legt de vinger op de zere plek van huidige AI-systemen: ze kunnen wiskundig "correcte" bewijzen leveren die fysiek volstrekt irrelevant zijn.

De vrijgegeven codebase en de FormalPhysics-dataset bieden een fundament voor de ontwikkeling van toekomstige AI-systemen die in staat zijn tot echte wetenschappelijke ontdekking, fact-checking en formele verificatie in complexe domeinen zoals de natuurkunde, chemie en biologie.