💻 computer science

A Foundation for Differentiable Logics using Dependent Type Theory

Dit artikel presenteert een unificerend raamwerk in het Rocq-bewijsassistentie-systeem, gebaseerd op afhankelijke type-theorie, om analytische, algebraïsche en bewijstheoretische eigenschappen van differentieerbare logica's en fuzzy-logica's systematisch te vergelijken en te formaliseren.

Oorspronkelijke auteurs: Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark

Gepubliceerd 2026-03-02

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark

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 zeer slimme robot wilt bouwen die auto's kan besturen of ziektes kan diagnosticeren. Deze robot is een neuraal netwerk, een soort digitaal brein dat leert door duizenden voorbeelden te bekijken. Maar hoe weet je of deze robot veilig is? Wat als hij een verkeersbord mist of een patiënt verkeerd diagnoseert?

Om dit te voorkomen, willen we de robot "trainen" om niet alleen goed te presteren, maar ook om specifieke regels (veiligheidseisen) te volgen. Hier komt dit wetenschappelijke paper om de hoek kijken. Het gaat over het bouwen van een gemeenschappelijke bouwplaat voor wiskundige regels die robots kunnen begrijpen en waar ze zich aan kunnen houden.

Hier is een uitleg in simpele taal, met een paar creatieve vergelijkingen:

1. Het Probleem: De Talenbarrière

Stel je voor dat je een groep architecten hebt die allemaal verschillende talen spreken.

De ene groep (de Fuzzy Logici) spreekt een taal die al honderd jaar oud is. Ze zijn experts in het bouwen van stevige, wiskundige fundamenten (algebra) en weten precies hoe hun regels in elkaar zitten. Maar hun regels zijn soms wat "stug": als een deel van de regel niet klopt, is het hele antwoord "fout", zonder ruimte voor nuance.
De andere groep (de Machine Learning Experts) spreekt een nieuwe, moderne taal. Ze hebben regels ontworpen die perfect werken voor het trainen van robots. Deze regels zijn "zacht" en kunnen kleine verbeteringen doorgeven (zoals een lichte duw in de goede richting). Maar ze weten niet precies hoe deze regels in elkaar zitten op een diep wiskundig niveau.

Het probleem is dat deze twee groepen niet met elkaar kunnen praten. Ze gebruiken verschillende meetlatjes en begrijpen elkaars regels niet. Dit maakt het moeilijk om te weten welke regels het beste zijn voor het bouwen van veilige AI.

2. De Oplossing: De Universele Vertaler

De auteurs van dit paper hebben een universele vertaler gebouwd. Ze hebben een digitale werkplaats (met een tool genaamd Rocq, een soort super-rekenmachine die geen fouten maakt) gecreëerd waarin ze alle verschillende soorten regels in één taal hebben vertaald.

Ze hebben gekeken naar:

De oude, stevige regels (zoals Gödel en Lukasiewicz).
De nieuwe, flexibele regels (zoals DL2 en STL).

Ze hebben deze regels naast elkaar gelegd en gekeken: "Werken ze op dezelfde manier? Zijn ze veilig? Kunnen we ze bewijzen?"

3. De Drie Pilaren van de Test

Om de regels te testen, hebben ze drie soorten "proeven" gebruikt, die ze als drie pilaren voor een huis zien:

De Stevige Fundering (Algebra):
Dit gaat over de structuur. Stel je voor dat je een legpuzzel hebt. Als je twee stukjes naast elkaar legt, moet het er logisch uitzien, ongeacht de volgorde. De auteurs hebben bewezen dat sommige regels (zoals de oude fuzzy regels) een perfecte, stevige puzzel zijn. Andere regels (zoals de nieuwe machine learning regels) zijn soms wat rommeliger: als je stukjes verwisselt, valt de puzzel misschien uit elkaar. Ze hebben precies in kaart gebracht welke regels wel en welke niet stevig genoeg zijn.
De Soepele Beweging (Analyse):
Dit is het belangrijkste voor het trainen van robots. Stel je voor dat je een auto op een helling rijdt. Je wilt niet dat de auto plotseling stopt als je het gaspedaal een heel klein beetje loslaat. Je wilt dat de auto soepel reageert op elke kleine beweging.
In de wereld van AI noemen ze dit Shadow-lifting. Het betekent: als je een regel een klein beetje verbetert, moet het resultaat ook een klein beetje verbeteren, zodat de robot weet welke kant op hij moet bewegen.
- De auteurs hebben ontdekt dat sommige oude regels hier niet goed in zijn (ze zijn te "stug").
- Ze hebben ook een nieuwe wiskundige tool (een regel van L'Hôpital, een soort wiskundige "sleutel") toegevoegd aan hun gereedschapskist om te bewijzen dat de nieuwe regels wel soepel bewegen.
De Bouwtekeningen (Bewijstheorie):
Dit gaat over de logica van het bewijzen. Als je zegt "Deze auto is veilig", moet je dat kunnen bewijzen met een logisch stappenplan. De auteurs hebben voor de nieuwe regels (die nog nooit eerder zo werden getoetst) nieuwe bouwtekeningen gemaakt. Ze hebben bewezen dat als je deze tekeningen volgt, je zeker weet dat de regels kloppen.

4. Waarom is dit belangrijk?

Vroeger was het een gok. Als je een AI wilde trainen om veilig te zijn, moest je hopen dat de regels die je koos wel werkten. Soms bleek later dat de regels een foutje hadden of dat ze niet goed samenwerkten.

Met deze nieuwe "universele bouwplaat" kunnen onderzoekers nu:

Vergelijken: Ze kunnen precies zien welke regels het beste zijn voor een specifieke taak.
Fouten vinden: Ze hebben al fouten gevonden in bestaande wetenschappelijke papers die door mensen met de hand waren berekend. De computer heeft gezegd: "Hé, hier klopt iets niet!"
Veiligheid garanderen: In de toekomst kunnen we AI-systemen bouwen die niet alleen slim zijn, maar waarvan we wiskundig kunnen bewijzen dat ze zich aan de regels houden.

Samenvattend

Dit paper is als het bouwen van een gemeenschappelijke taal voor twee groepen experts die al lang met elkaar hadden moeten praten. Ze hebben een digitale werkplaats gemaakt waar ze kunnen testen of de regels voor slimme robots stevig genoeg zijn, soepel genoeg bewegen, en logisch bewezen kunnen worden. Hierdoor kunnen we in de toekomst veel veiliger en betrouwbaardere AI-systemen bouwen.

Probleemstelling

Differentieerbare logieken (Differentiable Logics - DL's) zijn een familie van kwantitatieve logieken die ontstaan zijn in de machine learning-literatuur. Ze worden gebruikt om logische eigenschappen om te zetten in differentieerbare verliesfuncties, wat essentieel is voor "property-guided training" van neurale netwerken (waarbij het netwerk getraind wordt om specifieke eigenschappen te voldoen in plaats van alleen data te fiten).

Er zijn echter drie fundamentele problemen met de huidige staat van DL's:

Gebrek aan theoretische onderbouwing: Hoewel DL's analytische eigenschappen hebben (zoals differentieerbaarheid), ontbreekt er vaak een bijbehorende algebraïsche en bewijstheoretische theorie.
Fragmentatie en inconsistentie: Er bestaat een "dierentuin" van verschillende logieken (zoals fuzzy logieken, DL2, en STL) die verschillende domeinen gebruiken (bijv. $[0,1]$ , $]-\infty, 0]$ , of $]-\infty, +\infty[$ ), verschillende semantische definities hebben en niet met elkaar vergeleken kunnen worden op een gestructureerde manier.
Conflicterende eigenschappen: Er is een fundamenteel conflict tussen wenselijke eigenschappen. Bijvoorbeeld, het is onmogelijk om tegelijkertijd idempotentie, associativiteit en shadow-lifting (een eigenschap die zorgt voor geleidelijke verbetering tijdens training) te bereiken. Bestaande werken missen vaak een systematische analyse van deze trade-offs.

De auteurs stellen dat er een principieel, unificerend wiskundig kader nodig is om deze logieken te analyseren, te vergelijken en te verifiëren.

Methodologie

De auteurs gebruiken Interactieve Theorema Bewijzen (Interactive Theorem Proving - ITP) om een unificerend kader te bouwen. Specifiek gebruiken ze de Rocq (voorheen Coq) bewijshulp en de MathComp bibliotheek (Mathematical Components).

De aanpak bestaat uit drie hoofdaspecten:

Unificatie via Dependent Types: Ze definiëren een generieke syntaxis voor differentieerbare logieken. Door gebruik te maken van dependent types en intrinsieke typing (intrinsic typing), zorgen ze ervoor dat alleen geldige en goedgetypte formules voor elke specifieke logica kunnen worden geconstrueerd. Dit voorkomt typefouten en maakt het mogelijk om meerdere logieken (Gödel, Łukasiewicz, Yager, Product, DL2, STL) in één raamwerk te coderen.
Algebraïsche Analyse: Ze interpreteren de logieken binnen het kader van geresideerde roosters (residuated lattices). Dit is een algebraïsche structuur die traditioneel wordt gebruikt voor substructurele logieken en fuzzy logieken. Ze testen welke logieken voldoen aan de axioma's van geresideerde roosters (zoals commutativiteit, associativiteit, distributiviteit en het residuatie-axioma).
Analytische en Bewijstheoretische Analyse:
- Analytisch: Ze formaliseren eigenschappen zoals shadow-lifting (het vermogen van een connectief om een positieve partiële afgeleide te hebben, wat essentieel is voor gradient descent). Hiervoor moesten ze de regel van L'Hôpital formaliseren in de MathComp-Analysis bibliotheek, omdat deze nog niet beschikbaar was.
- Bewijstheoretisch: Ze definiëren en verifiëren sequentie-calculi (sequent calculi) voor de logieken. Voor bestaande fuzzy logieken formaliseren ze bestaande hypersequent-calculi. Voor DL2 en een beperkte versie van STL (STL∞) stellen ze nieuwe, geluid (sound) calculi op.

Belangrijkste Bijdragen

Unificerend Formalisatiekader: De auteurs hebben een uitgebreide formalisatie van diverse differentieerbare logieken in Rocq gerealiseerd. Dit omvat een generieke syntaxis die zowel fuzzy logieken als machine learning-geïnspireerde logieken (DL2, STL) omvat.
Algebraïsche Karakterisering: Ze tonen aan hoe nieuwe DL's (zoals DL2 en STL) kunnen worden gemapt naar geresideerde roosters. Ze ontdekten dat STL∞ (de limiet van STL wanneer de parameter $\nu \to \infty$ ) wel voldoet aan de algebraïsche eisen van een geresideerd rooster, terwijl STLν (met eindige $\nu$ ) dit niet doet.
Formalisatie van L'Hôpital's Regel: Om shadow-lifting voor STLν te bewijzen, hebben ze de regel van L'Hôpital toegevoegd aan de MathComp-Analysis bibliotheek. Dit is een significante bijdrage aan de wiskundige basis van de Rocq-ecosysteem.
Nieuwe Sequentie-Calculi: Ze hebben nieuwe, geluid sequentie-calculi ontworpen en bewezen voor DL2 en STL∞. Dit vult een leemte in de literatuur, aangezien deze logieken eerder geen bewijstheoretische semantiek hadden.
Correctie van Literatuur: Tijdens het formaliseren ontdekten en corrigeerden ze fouten in eerdere handmatige bewijzen (pen-and-paper proofs) in de literatuur, met name wat betreft de shadow-lifting eigenschap van STLν en de interpretatie van vergelijkingen in fuzzy logieken.
Toepassing in Machine Learning: Ze tonen aan hoe deze formalisatie direct kan worden toegepast om verliesfuncties te genereren voor eigenschap-gestuurde training, met een voorbeeld van $\epsilon$ - $\delta$ -robustheid.

Resultaten

De resultaten worden samengevat in een uitgebreide tabel (Tabel 6 in het artikel) die de eigenschappen van elke logica vergelijkt:

Algebraïsch: Gödel, Łukasiewicz, Yager, Product, DL2 en STL∞ vormen geresideerde roosters. STLν doet dit niet vanwege het ontbreken van associativiteit.
Analytisch (Shadow-lifting): DL2 en Product logica voldoen aan shadow-lifting. STLν voldoet ook (na correctie en volledige bewijsvoering). Gödel, Łukasiewicz, Yager en STL∞ voldoen niet aan shadow-lifting omdat ze min/max gebruiken, wat niet overal differentieerbaar is.
Bewijstheoretisch: Geluid calculi zijn gedefinieerd en bewezen voor Gödel, Łukasiewicz, Product, DL2 en STL∞. Voor STLν en Yager is een volledig calculus nog niet gedefinieerd of onbekend.
Trade-offs: De studie bevestigt de stelling dat het onmogelijk is om idempotentie, associativiteit en shadow-lifting tegelijkertijd te hebben. STLν kiest voor shadow-lifting en verliest associativiteit; STL∞ kiest voor associativiteit en algebraïsche schoonheid, maar verliest shadow-lifting.

Betekenis en Impact

Deze paper is van groot belang voor zowel de gemeenschap van formele verificatie als die van machine learning:

Brug tussen gemeenschappen: Het artikel verbindt de rijke algebraïsche en bewijstheoretische traditie van fuzzy logieken (uit de logica-gemeenschap) met de analytische behoeften van machine learning. Het toont aan dat deze twee werelden kunnen worden verenigd.
Betrouwbaarheid: Door gebruik te maken van interactieve theoremabewijzen, bieden de auteurs een gegarandeerd correcte basis voor de semantiek van differentieerbare logieken. Dit is cruciaal voor het ontwikkelen van betrouwbare tools voor de verificatie van neurale netwerken.
Tooling voor Property-Guided Training: De formalisatie biedt een solide theoretische onderbouwing voor tools zoals Vehicle, die eigenschappen van neurale netwerken specificeren en vertalen naar verliesfuncties. Het helpt bij het kiezen van de juiste logica voor een specifieke toepassing (bijv. als shadow-lifting cruciaal is, moet men kiezen voor DL2 of STLν in plaats van Gödel).
Basis voor Toekomstig Onderzoek: De unificatie en de toegevoegde bibliotheken (zoals L'Hôpital's regel) vormen een fundament voor toekomstig werk, zoals het formaliseren van volledigheid (completeness), het uitbreiden naar first-order logieken, en het certificeren van compilers voor domeinspecifieke talen in AI.

Kortom, dit werk legt de wiskundige en formele fundering voor het begrijpen, vergelijken en betrouwbaar toepassen van differentieerbare logieken in de moderne AI.