🤖 AI

PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

Het artikel introduceert PriorProof, een geautomatiseerde, ontologievrije methode voor het kwantificeren van de nieuwheid van formele bewijstechnieken in Lean door de verrassing (surprisal) van hun afhankelijkheidsvoetafdrukken te meten ten opzichte van een tijdgeankerde prior, waarbij een matige overeenstemming met menselijke experts wordt aangetoond en het dient als een decomponeerbaar, interpreteerbaar signaal in plaats van een vervanging voor deskundige beoordeling.

Oorspronkelijke auteurs: Neel Somani

Gepubliceerd 2026-07-21

📖 8 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Neel Somani

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 door een enorme, steeds groter wordende bibliotheek van wiskundige ideeën wandelt. In deze bibliotheek moet elk nieuw boek (een bewijs) de oudere boeken citeren die het gebruikte om zijn argumenten op te bouwen. Meestal gebruiken wiskundigen bij het schrijven van een nieuw bewijs de meest voorkomende, goed ingestelde instrumenten die op dat moment beschikbaar zijn. Maar soms nemen ze een wilde, onverwachte route, waarbij ze een vreemde combinatie van oude instrumenten gebruiken die voorheen door niemand werd bedacht om te mengen. De grote vraag is: hoe weten we, enkel door naar de lijst met boeken te kijken die ze hebben gebruikt, of hun pad werkelijk verrassend was of slechts een routinematige omweg? Dit is het puzzelstukje van "nieuwheid" in de formele wiskunde. Hoewel mensen kunnen discussiëren over de vraag of een bewijs "elegant" of "origineel" is, hebben computers moeite met deze vage gevoelens. Ze hebben een harde, mechanische manier nodig om te meten of een bewijs een route nam die onwaarschijnlijk zou zijn gebeurd gezien wat er op dat moment bekend was. Hier komt het idee van "surprisal" (verrassing) om de hoek kijken—denk aan het als een maatstaf voor hoeveel een bewijs de bibliotheek doet zeggen: "Wacht, ik had niet verwacht dat je dat specifieke gereedschap voor deze klus zou gebruiken!"

Maak kennis met PriorProof, een nieuwe tool ontworpen om te fungeren als een tijdreizende bibliothecaris. In plaats van een mens te vragen: "Was dit bewijs slim?", vraagt PriorProof een kille, harde vraag: "Als we de bibliotheek zouden bevriezen op het exacte moment dat dit bewijs werd geschreven, hoe verrassend zou de lijst met gebruikte instrumenten dan zijn?" De onderzoekers bouwden een systeem dat een formeel bewijs (geschreven in een taal genaamd Lean) bekijkt, de mooie opmaak weglaat en een "voetafdruk" maakt van de specifieke wiskundige machinerie die wordt gebruikt. Vervolgens reist het terug in de tijd naar een momentopname van de bibliotheek uit de periode voordat dit bewijs bestond. Het vraagt: "Op basis van andere bewijzen met vergelijkbare doelen uit die eerdere tijd, hoe waarschijnlijk was het dat iemand deze specifieke instrumenten zou gebruiken?" Als het antwoord "zeer onwaarschijnlijk" is, krijgt het bewijs een hoge "nieuwheidsscore". De studie toonde aan dat deze mechanische score vaak overeenkomt met menselijke experts over welke bewijzen de meer ongebruikelijke route namen, vooral wanneer het verschil in scores groot is. De auteurs waarschuwen echter dat dit geen toverstaf is die alles oplost; het is een nuttig signaal dat het beste werkt wanneer het verschil tussen twee bewijzen duidelijk is, en het meet niet de "schoonheid" of "belangrijkheid" van de wiskunde, maar enkel hoe onverwacht het pad was.

De Tijdreizende Bibliothecaris

Stel je voor dat je een detective bent die probek te achterhalen of een dief een geheim, nog nooit eerder vertoonde methode heeft gebruikt om een kluis te kraken. Je kunt de dief niet vragen wat hij dacht, maar je kunt wel kijken naar de instrumenten die hij heeft achtergelaten. PriorProof is die detective, maar dan voor wiskundige bewijzen. Het geeft niet om het motief van de dief of hoe cool de overval eruitzag; het geeft alleen om de instrumenten (de wiskundige constanten en lemma's) die werden gebruikt om het probleem op te lossen en of die instrumenten een vreemde keuze waren voor die tijdperiode.

Zo werkt de goocheltruc, stap voor stap:

De Voetafdruk: Wanneer een wiskundige een bewijs schrijft in Lean (een computertaal voor wiskunde), zet de computer dit om in een lange, gedetailleerde lijst van elk instrument dat het heeft gebruikt. PriorProof neemt deze lijst en ruimt deze op door vergelijkbare instrumenten in "families" te groeperen (zoals het groeperen van alle hamers samen, of alle schroevendraaiers). Dit is de "voetafdruk".
De Tijdmachine: Het systeem reist vervolgens terug in de tijd. Het pakt een momentopname van de gehele wiskundige bibliotheek van vóór het bewijs werd geschreven. Het kijkt naar alle andere bewijzen die rond die tijd werden geschreven die probeerden soortgelijke problemen op te lossen.
De Voorspelling: Met behulp van een slim computermodel (een taalmodel) voorspelt het: "Als ik destijds een bewijs voor dit probleem zou schrijven, welke instrumenten zou ik dan waarschijnlijk gebruiken?" Het bouwt een "prior" verwachting op, zoals een weersverwachting voor wiskundige instrumenten.
De Verrassingsscore: Ten slotte vergelijkt het de werkelijke instrumenten die in het nieuwe bewijs zijn gebruikt met de weersverwachting. Als het bewijs instrumenten gebruikte die de voorspelling als zeer onwaarschijnlijk beschouwde (lage waarschijnlijkheid), geeft het systeem een hoge "surprisal"-score. Een hoge score betekent: "Wauw, dat was een vreemde route om te nemen!"

Wat de Detective Ontdekte

De onderzoekers testten dit systeem op een specifiek deel van de wiskundige bibliotheek genaamd Topologie (die gaat over vormen en ruimtes). Ze gokten niet zomaar; ze zetten een blinde test op. Ze namen 100 paren bewijzen en lieten deze zien aan drie menselijke wiskundige experts. De experts moesten in elk paar kiezen welk bewijs de "minder standaard" (meer verrassende) route had genomen. Zij zagen de scores niet; ze gebruikten simpelweg hun brein.

Vervolgens vergeleken ze de keuzes van de menselijke experts met wat PriorProof voorspelde. Dit was het resultaat:

Van de 76 unieke paren bewijzen (sommige werden meerdere keren getoond om de consistentie te controlen), stemde PriorProof in 53 gevallen overeen met de meerderheid van de menselijke experts. Dat is ongeveer 69,7%.
Voor de 12 paren die specifiek waren gekozen omdat het overduidelijke "schoolvoorbeeld"-gevallen waren van verrassend versus standaard bewijzen, had PriorProof het in 11 gevallen bij het rechte eind (ongeveer 91,7%).
Voor de andere 64 paren, die wat lastiger waren, had het er 42 goed (ongeveer 65,6%).

De auteurs keken ook naar de "scoregap"—het verschil tussen de verrassingsscore van de twee bewijzen in een paar. Ze vonden een helder patroon: wanneer de kloof groot was (wat betekende dat het ene bewijs veel verrassender was dan het andere), was het systeem zeer betrouwbaar en stemde het in 84,2% van de gevallen overeen met de mensen. Maar wanneer de kloof klein was (de twee bewijzen waren even verrassend), was het systeem minder zeker en stemde het slechts in 63,2% van de gevallen overeen. Dit suggereert dat het hulpmiddel geweldig is in het opsporen van de "grote verrassingen", maar wazig wordt wanneer de verschillen subtiel zijn.

Wat het NIET is (en wat het uitsluit)

Het is cruciaal om te begrijpen wat PriorProof niet beweert te zijn. De auteurs zijn hier heel duidelijk over:

Het is geen maatstaf voor "Originaliteit" of "Genialiteit": Een hoge score betekent niet dat de wiskundige een genie was. Het betekent alleen dat hij een vreemde combinatie van instrumenten gebruikte. Soms is een vreemde route gewoon een onhandige omweg, en geen brilante inzichten.
Het is geen maatstaf voor "Belangrijkheid": Een bewijs kan ongelooflijk belangrijk zijn voor de wereld van de wiskunde, maar gebruikmaken van zeer standaard, saaie instrumenten. PriorProof zou een lage score geven, zelfs als het de geschiedenis zou veranderen.
Het is geen "Plagiaatdetector": Het systeem geeft niet om het feit of iemand een bewijs heeft gekopieerd. Het geeft alleen om de statistische waarschijnlijkheid van de gebruikte instrumenten.
Het is geen "Perfecte" rechter: De auteurs geven expliciet aan dat hun methode geen "opgelost probleem" is. Sterker nog, toen ze PriorProof vergeleken met een krachtig AI-taalmodel (GPT-5-mini), stemde de AI zelfs iets vaker overeen met de menselijke experts (ongeveer 78,9% tegenover 69,7%). Echter, het verschil was niet statistisch significant genoeg om te kunnen zeggen dat de één definitief beter was dan de ander. De echte waarde van PriorProof is niet dat het de AI verslaat, maar dat het transparant is. Je kunt naar de score kijken en precies zien welk instrument de verrassing veroorzaakte, terwijl de AI een "black box" is die alleen een antwoord geeft.

De Kernboodschap

PriorProof is een nieuwe, mechanische manier om te meten hoe "niet-standaard" een wiskundig bewijs is door te kijken naar hoe verrassend de keuzes voor instrumenten waren op het moment dat het werd geschreven. Het werkt goed genoeg om in twee derde van de gevallen overeen te komen met menselijke experts, en het werkt nog beter wanneer het verschil tussen twee bewijzen overduidelijk is. Het vertelt ons niet of een bewijs mooi, belangrijk of briljant is, maar het geeft ons wel een betrouwbaar, tijdgestempeld signaal dat zegt: "Hé, dit pad was onverwacht." Het is een instrument voor onderzoekers om interessante gevallen te vinden om te bestuderen, en niet een definitieve rechter over wiskundige grootheid. De auteurs suggereren dat we dit in de toekomst kunnen gebruiken om te helpen bij het opsporen van interessante door machines gegenereerde bewijzen of om te bestuderen hoe wiskundige bibliotheken evolueren, maar voor nu is het slechts een zeer slimme, zeer specifieke manier om verrassing te meten.

Technische Samenvatting: PriorProof

Probleemstelling

Formele bewijsbibliotheken, zoals de Mathlib van Lean, bieden een uniek verslag van wiskundige ontwikkeling: de geëlaborerde bewijsterm vermeldt expliciet de gebruikte constanten, en versiebeheer identificeert exact welke declaraties aanwezig waren op het moment van schrijven. Dit maakt een mechanische investigatie mogelijk naar tijd-relatieve bewijsroute-niet-standaardheid: bepalen hoe "verrassend" of niet-standaard een bewijsroute was ten opzichte van de technieken die beschikbaar waren toen het werd geschreven.

Terwijl bestaande evaluaties van geleerde theorembewijzers zich richten op of een stelling bewezen is, de zoekkosten, of overdraagbaarheid, meten zij niet direct of een succesvol bewijs een route volgt die door de eerdere bibliotheek waarschijnlijk zou zijn gemaakt. Filosofen en wiskundigen hebben lang deugden van bewijzen zoals verklaring, zuiverheid en elegantie geanalyseerd, maar deze zijn moeilijk mechanisch te operationaliseren. PriorProof adresseert een nauwer construct: route-nieuwheid, gedefinieerd als de afwijking van de afhankelijkheidsvoetafdruk van een bewijs van de verwachte distributie van afhankelijkheden voor vergelijkbare beweringen in de eerdere staat van de bibliotheek.

Methodologie

PriorProof is een per kwartaal uitgevoerde, tijdgebonden maatstaf voor Lean 4/Mathlib-bewijzen. De pijplijn werkt op een stellingdeclaratie $D$ geschreven op tijdstip $t$ via drie primaire stadia:

1. Extractie van de Afhankelijkheidsvoetafdruk

Het systeem extraheert een gewogen "afhankelijkheidsfamilie-voetafdruk" uit de geëlabereerde bewijsterm $p_D$ :

Extractie: Het gebruikt Lean's getUsedConstants om constanten te identificeren die daadwerkelijk door de bewijsterm worden geraadpleegd, waarbij loutere bestandimporten worden uitgesloten.
Filtering: Een deterministische filter verwijdert gegenereerde recursoren, coercions, routine typeclass-plumbing en tactic-boilerplate.
Frontier Traversal: Afhankelijkheden worden recursief vervangen door oudere afhankelijkheden waarop zij rusten, totdat de traversatie de declaraties bereikt die in de snapshot van de bibliothek vóór $t$ zijn vastgesteld. Vaststelling wordt gedefinieerd door een vooraf bepaalde hergebruik-drempelwaarde (pre-bin reuse-count threshold) om te voorkomen dat gelijktijdig geïntroduceerde declaraties als gevestigd worden beschouwd.
Family Backoff: Elke overlevende constante wordt gekoppeld aan de fijnste "afhankelijkheidsfamilie" (namespace, module of bibliotheekgebied) met ten minste vijf pre-bin voorkomens. Dit vermindert accidentele nieuwheid door zeldzame namen zonder dat een handmatig gebouwde ontologie vereist is.
Resultaat: Een gewogen verzameling $\Phi_t(D) = \{(f_i, w_i)\}$ die de geobserveerde afhankelijkheidsfamilies representeert.

2. Statement-geconditioneerde Prior Constructie

Om te bepalen wat "verwacht" werd, haalt het systeem vergelijkbare stellingbeweringen op uit een bibliotheeksnapshot die strikt eerder is dan het kwartaal van de doelstelling ( $L_{<b(t)}$ ):

Retrieval: Een sentence-transformer encoder (fijn afgestemd op pre-bin contrastieve paren) haalt de $k=32$ dichtstbijzijnde buren op basis van cosinus-gelijkenis.
Smoothing: Een hiërarchisch gesmoothte prior $q_t(f|D)$ $q_{t} (f ∣ D)$ wordt geconstrueerd als een mengeling van empirische familieverdelingen uit:
- De opgehaalde buren ( $q_{r,t}$ )
- De doel-namespace ( $q_{n,t}$ )
- De doel-module ( $q_{m,t}$ )
- De volledige pre-bin bibliotheek ( $q_{g,t}$ )
Optimalisatie: Mengselsgewichten en smoothing-parameters worden geselecteerd door de chronologische log-likelihood van geobserveerde families in eerdere bewijzen te maximaliseren, waardoor de prior voorspellend is in plaats van afgestemd op de menselijke studie.

3. Scoring

De PriorProof score $S_t(D)$ is de gewogen verrassing (surprisal) van de geobserveerde voetafdruk onder de geconstrueerde prior:
$S_t(D) = \sum_{i=1}^{m_D} w_i [-\log q_t(f_i | D)]$
Een hoge score geeft aan dat het bewijs afhankelijkheidsfamilies gebruikt die onwaarschijnlijk waren voor eerdere stellingen met vergelijkbare beweringen. Voor paarvergelijkingen selecteert de metriek het bewijs met de hogere score, waarbij het absolute scoreverschil $\Delta(A, B)$ als intern betrouwbaarheidssignaal wordt gebruikt.

Belangrijkste Bijdragen

Mechanische Definitie: Een definitie van tijd-relatieve bewijsroute-niet-standaardheid als afhankelijkheidsvoetafdruk-verrassing, die geen handmatig gebouwde techniek-ontologie of menselijke labels vereist.
Temporele Discipline: Een rigoureuze lekage-discipline waarbij retrieval, familie-ondersteuning, hergebruik-tellingen en encoder-fijnstelling strikt beperkt zijn tot pre-bin data.
Empirische Studie: Een geblindeerde studie op de Mathlib-topologie met mechanische validatie, een drie-rater vergelijking en een taalmodel-baseline.
Endpoint-Kalibratie Bewijs: Empirisch bewijs dat het absolute scoreverschil dient als een kandidaat-betrouwbaarheidsindicator, waarbij grotere verschillen correleren met een hogere overeenstemming met menselijke raters, hoewel de relatie geen opgeloste monotone trapfunctie is.

Resultaten

De studie evalueerde 100 geblindeerde presentaties (samengevallen tot 76 unieke onderliggende bewijs-paren) tegen drie behouden domein-raters en taalmodel-baselines (gpt-5/gpt-5-mini).

Overeenstemming met Raters: PriorProof stemde overeen met de meerderheid van de drie raters op 53/76 paren (69,7%).
- Canonieke Paren: 11/12 (91,7%) op 12 handgekozen canonieke contrasten.
- Gestreifieerde Paren: 42/64 (65,6%) op de bredere set.
Taalmodel Baseline: De beste taalmodel-conditie stemde overeen op 60/76 paren (78,9%). Een McNemar-test die PriorProof en het model vergeleek, leverde $p=0,210$ op, wat aangeeft dat het verschil bij deze steekproefomvang niet statistisch vastgesteld is.
Score Gap Kalibratie:
- In de kleinste score-gap bin was de overeenstemming 12/19 (63,2%), statistisch compatibel met toeval.
- In de grootste score-gap bin was de overeenstemming 16/19 (84,2%).
- De binnenste bins waren niet-monotoon, en de betrouwbaarheidsintervallen waren breed. Het paper concludeert dat dit een endpoint-kalibratie-tendens ondersteunt (hoge gaps zijn betrouwbaarder) in plaats van een opgeloste, universele kalibratiecurve.
Mechanische Validatie: Geobserveerde voetafdrukken ontvingen significant hogere chronologische waarschijnlijkheid dan willekeurige alternatieven. Ablatie-studies bevestigden dat retrieval en smoothing-componenten betekenisvol bijdragen aan de score, terwijl redundantiecontroles geen "live" hits vonden in de gecureerde corpus (hoewel de geneste pad was inactief vanwege backend-beperkingen).

Betekenis en Claims

Het paper presenteert PriorProof niet als een vervanging voor expert- of modeloordeel, noch als een volledige theorie van wiskundige nieuwheid. In plaats daarvan wordt het gepositioneerd als een decomponeerbaar, tijd-verankerd signaal.

Scope: De metriek richt zich specifal op of een bewijsroute onverwacht verdeelde eerdere machinerie gebruikt. Het is blind voor definitionele nieuwheid, verklarende waarde, elegantie of auteursrecht.
Betrouwbaarheidsindicator: De primaire geïdentificeerde bruikbaarheid is de score gap. De resultaten suggereren dat wanneer de score gap tussen twee bewijzen groot is, de voorkeur van de metriek waarschijnlijker overeenkomt met het menselijk oordeel. Wanneer de gap klein is, is de metriek minder betrouwbaar.
Beperkingen: De auteurs merken expliciet op dat de metriek kan worden gemanipuleerd door irrelevante zeldzame machinerie toe te voegen, en dat de huidige implementatie geen subterm-bewuste normalisatie mist (geneste redundantie detectie is inactief). De statistische reikwijdte is beperkt tot één wiskundig domein (topologie) en een specifieke steekproefomvang.
Toekomstig Nut: De metriek is bedoeld als een onderzoeksinstrument voor het analyseren van gecontroleerde formele bewijzen, het prioriteren van gevallen voor deskundige beoordeling, en het bestuderen van door machines gegenereerde bewijzen om te zien of zij verwachte patronen reproduceren of routes ontdekken die menselijke aandacht verdienen. Het is een hypothesegenerator, geen arbiter van originaliteit.