🤖 AI

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

L'article présente PriorProof, une méthode automatisée et sans ontologie pour quantifier la nouveauté des techniques de preuve formelle dans Lean en mesurant la surprise de leurs empreintes de dépendance par rapport à un a priori ancré dans le temps, démontrant un accord modéré avec les experts humains et servant de signal décomposable et interprétable plutôt que de remplacement au jugement d'expert.

Auteurs originaux : Neel Somani

Publié 2026-07-21

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Neel Somani

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous déambulez dans une immense bibliothèque de concepts mathématiques en constante expansion. Dans cette bibliothèque, chaque nouveau livre (une preuve) doit citer les livres plus anciens qu'il a utilisés pour construire ses arguments. Habituellement, lorsqu'un mathématicien écrit une nouvelle preuve, il essaie d'utiliser les outils les plus courants et les plus éprouvés disponibles à ce moment-là. Mais parfois, ils empruntent un chemin sauvage et inattendu, utilisant une combinaison étrange d'outils anciens que personne n'avait pensé à mélanger auparavant. La grande question est : comment savoir, rien qu'en regardant la liste des livres qu'ils ont utilisés, si leur chemin était vraiment surprenant ou simplement un détour routinier ? C'est le puzzle de la « nouveauté » dans la mathématique formelle. Si les humains peuvent débattre pour savoir si une preuve est « élégante » ou « originale », les ordinateurs luttent avec ces sentiments flous. Ils ont besoin d'une méthode rigoureuse et mécanique pour mesurer si une preuve a emprunté une route qui était peu probable de se produire compte tenu de ce qui était connu à l'époque. C'est là qu'intervient l'idée de « surprisal » (la surprise) — voyez cela comme une mesure de la mesure à laquelle la bibliothèque dit : « Attendez, je ne m'attendais pas à ce que vous utilisiez cet outil spécifique pour ce travail ! »

Entrez dans PriorProof, un nouvel outil conçu pour agir comme un bibliothécaire voyageant dans le temps. Au lieu de demander à un humain : « Cette preuve était-elle ingénieuse ? », PriorProof pose une question froide et implacable : « Si nous figeions la bibliothèque à l'instant exact où cette preuve a été écrite, à quel point la liste des outils utilisés serait-elle surprenante ? » Les chercheurs ont construit un système qui examine une preuve formelle (écrite dans un langage appelé Lean), en dépouille le formatage sophistiqué, et crée une « empreinte » de la machinerie mathématique spécifique utilisée. Ensuite, il remonte le temps pour prendre un instantané de la bibliothèque à partir d'un cliché de la bibliothèque avant que cette preuve n'existe. Il demande : « Sur la base d'autres preuves ayant des objectifs similaires à cette époque, quelle était la probabilité que quelqu'un utilise ces outils spécifiques ? » Si la réponse est « très improbable », la preuve reçoit un score de « nouveauté » élevé. L'étude a montré que ce score mécanique concorde souvent avec les experts humains sur le fait qu'une preuve a emprunté la route la plus inhabituelle, surtout lorsque la différence entre les scores est importante. Cependant, les auteurs sont prudents et précisent que ce n'est pas une baguette magique qui résout tout ; c'est un signal utile qui fonctionne mieux lorsque l'écart entre deux preuves est évident, et cela ne mesure pas la « beauté » ou l'« importance » des mathématiques, mais seulement à quel point le chemin était inattendu.

Le Bibliothécaire Voyageur dans le Temps

Imaginez que vous êtes un détective essayant de déterminer si un voleur a utilisé une méthode secrète, jamais vue auparavant, pour forcer un coffre-fort. Vous ne pouvez pas demander au voleur ce qu'il pensait, mais vous pouvez regarder les outils qu'il a laissés derrière lui. PriorProof est ce détective, mais pour les preuves mathématiques. Il ne se soucie pas du mobile du voleur ou de l'aspect spectaculaire du cambriolage ; il ne s'intéresse qu'aux outils (les constantes et les lemmes mathématiques) utilisés pour résoudre le problème et si ces outils étaient un choix étrange pour la période concernée.

Voici comment fonctionne le tour de magie, étape par étape :

L'Empreinte : Lorsqu'un mathématicien écrit une preuve en Lean (un langage informatique pour les mathématiques), l'ordinateur la transforme en une liste longue et détaillée de chaque outil utilisé. PriorProof prend cette liste et la nettoie, regroupant les outils similaires en « familles » (comme regrouper tous les marteaux ensemble, ou tous les tournevis). C'est l'« empreinte ».
La Machine à Remonter le Temps : Le système voyage ensuite dans le passé. Il saisit un instantané de toute la bibliothèque mathématique datant d'avant la rédaction de la preuve. Il examine toutes les autres preuves écrites à cette époque qui tentaient de résoudre des problèmes similaires.
La Prédiction : En utilisant un modèle informatique intelligent (un modèle de langage), il prédit : « Si j'écrivais une preuve pour ce problème à l'époque, quels outils utiliserais-je probablement ? » Il construit une attente « a priori », comme une prévision météorologique pour les outils mathématiques.
Le Score de Surprise : Enfin, il compare les outils réellement utilisés dans la nouvelle preuve par rapport aux prévisions. Si la preuve a utilisé des outils que la prévision jugeait très improbables (faible probabilité), le système lui attribue un score de « surprisal » élevé. Un score élevé signifie : « Wow, c'était une route très étrange à prendre ! »

Ce que le Détective a Découvert

Les chercheurs ont testé ce système sur une section spécifique de la bibliothèque mathématique appelée Topologie (qui traite des formes et des espaces). Ils ne se sont pas contentés de deviner ; ils ont mis en place un test en aveugle. Ils ont pris 100 paires de preuves et les ont présentées à trois experts en mathématiques. Les experts devaient choisir, dans chaque paire, quelle preuve avait emprunté la route la « moins standard » (la plus surprenante). Ils ne voyaient pas les scores ; ils utilisaient simplement leur cerveau.

Ensuite, ils ont comparé les choix des experts humains avec les prédictions de PriorProof. Voici le résultat :

Sur 76 paires de preuves uniques (certaines ayant été présentées plusieurs fois pour vérifier la cohérence), PriorProof a été en accord avec la majorité des experts humains sur 53 d'entre elles. Cela représente environ 69,7 %.
Pour les 12 paires qui avaient été spécifiquement choisies parce qu'elles étaient des exemples « de manuel » évidents de preuves surprenantes versus standard, PriorProof a eu raison 11 fois (environ 91,7 %).
Pour les 64 autres paires, un peu plus complexes, il a réussi 42 fois (environ 65,6 %).

Les auteurs ont également examiné l'« écart de score » — la différence entre le score de surprise des deux preuves d'une même paire. Ils ont trouvé un motif net : lorsque l'écart était énorme (signifiant qu'une preuve était beaucoup plus surprenante que l'autre), le système était très fiable, s'accordant avec les humains 84,2 % du temps. Mais quand l'écart était faible (les deux preuves étant de surprise similaire), le système était moins sûr de lui, ne s'accordant qu'avec 63,2 % du temps. Cela suggère que l'outil est excellent pour repérer les « grandes surprises », mais devient imprécis lorsque les différences sont subtiles.

Ce qu'il n'est PAS (et ce qu'il exclut)

Il est crucial de comprendre ce que PriorProof ne prétend pas être. Les auteurs sont très clairs à ce sujet :

Ce n'est pas une mesure de l'« Originalité » ou du « Génie » : Un score élevé ne signifie pas que le mathématicien était un génie. Cela signifie simplement qu'il a utilisé une combinaison d'outils étranges. Parfois, une route étrange n'est qu'un détour maladroit, pas une intuition brillante.
Ce n'est pas une mesure de l'« Importance » : Une preuve peut être incroyablement importante pour le monde des mathématiques mais utiliser des outils très standards et banals. PriorProof donnerait un score faible, même si elle changeait l'histoire.
Ce n'est pas un « Détecteur de Plagiat » : Le système ne se soucie pas de savoir si quelqu'un a copié une preuve. Il ne s'intéresse qu'à la probabilité statistique des outils utilisés.
Ce n'est pas un juge « Parfait » : Les auteurs déclarent explicitement que leur méthode n'est pas un « problème résolu ». En fait, lorsqu'ils ont comparé PriorProof à un puissant modèle de langage IA (GPT-5-mini), l'IA a effectivement été en accord avec les experts humains un peu plus souvent (environ 78,9 % contre 69,7 %). Cependant, la différence n'était pas statistiquement significative pour dire que l'un était définitivement meilleur que l'autre. La véritable valeur de PriorProof n'est pas de battre l'IA, mais d'être transparent. Vous pouvez regarder le score et voir exactement quel outil a causé la surprise, alors que l'IA est une « boîte noire » qui donne simplement une réponse.

L'Essentiel à Retenir

PriorProof est une nouvelle façon mécanique de mesurer à quel point une preuve mathématique est « non standarde » en observant à quel point le choix de ses outils était surprenant au moment où elle a été écrite. Il fonctionne suffisamment bien pour être en accord avec les experts humains environ deux tiers du temps, et il est encore plus performant lorsque la différence entre deux preuves est flagrante. Il ne nous dit pas si une preuve est belle, importante ou brillante, mais il nous donne un signal temporel fiable qui dit : « Hé, ce chemin était inattendu. » C'est un outil destiné aux chercheurs pour identifier des cas intéressants à étudier, et non un juge final de la grandeur mathématique. Les auteurs suggèrent qu'à l'avenir, nous pourrions l'utiliser pour aider à repérer des preuves générées par machine intéressantes ou pour étudier l'évolution des bibliothèques mathématiques, mais pour l'instant, c'est simplement une façon très intelligente et très spécifique de mesurer la surprise.

Résumé Technique : PriorProof

Énoncé du Problème

Les bibliothèques de preuves formelles, telles que Mathlib pour Lean, offrent un enregistrement unique du développement mathématique : le terme de preuve élaboré liste explicitement les constantes utilisées, et le contrôle de version identifie précisément quelles déclarations existaient au moment de l'écriture. Cela permet une investigation mécanique de la non-standardité de la route de preuve relative au temps : déterminer à quel point la route d'une preuve était « surprenante » ou non standard par rapport aux techniques disponibles lorsqu'elle a été écrite.

Alors que les évaluations existantes des prouveurs de théorèmes appris se concentrent sur la capacité à prouver un théorème, le coût de recherche ou la transférabilité, elles ne mesurent pas directement si une preuve réussie suit une route qui aurait rendu probable l'usage de techniques antérieures. Les philosophes et les mathématiciens analysent depuis longtemps des vertus de la preuve telles que l'explication, la pureté et l'élégance, mais celles-ci sont difficiles à opérationnaliser mécaniquement. PriorProof s'attaque à un construit plus étroit : la nouveauté de la route, définie comme l'écart entre l'empreinte de dépendance d'une preuve et la distribution attendue des dépendances pour des énoncés similaires dans l'état antérieur de la bibliothèque.

Méthodologie

PriorProof est une mesure trimestrielle, ponctuelle, pour les preuves Lean 4/Mathlib. Le pipeline opère sur une déclaration de théorème $D$ écrite à un instant $t$ à travers trois étapes principales :

1. Extraction de l'Empreinte de Dépendance

Le système extrait une « empreinte de famille de dépendances » pondérée à partir du terme de preuve élaboré $p_D$ :

Extraction : Il utilise getUsedConstants de Lean pour identifier les constantes réellement référencées par le terme de preuve, en excluant les simples imports de fichiers.
Filtrage : Un filtre déterministe élimine les récurseurs générés, les coercitions, la plomberie de typeclass de routine et le code de base des tactiques (tactic boilerplate).
Traversée de la Frontière : Les dépendances sont remplacées récursivement par les anciennes dépendances sur lesquelles elles reposent jusqu'à ce que la traversée atteigne des déclarations établies dans la capture de la bibliothèque avant $t$ . L'établissement est défini par un seuil de réutilisation pré-bin pour éviter que des déclarations co-introduites n'apparaissent comme établies.
Repli de Famille (Family Backoff) : Chaque constante survivante est associée à la « famille de dépendance » la plus fine (espace de noms, module ou zone de la bibliothèque) possédant au moins cinq occurrences pré-bin. Cela réduit la nouveauté accidentelle due à des noms rares sans nécessiter d'ontologie construite à la main.
Résultat : Un ensemble pondéré $\Phi_t(D) = \{(f_i, w_i)\}$ représentant les familles de dépendances observées.

2. Construction du Prior Conditionné par l'Énoncé

Pour déterminer ce qui était « attendu », le système récupère des énoncés de théorèmes similaires dans une capture de la bibliothèque strictement antérieure au trimestre de la cible ( $L_{<b(t)}$ ) :

Récupération : Un encodeur de transformateur de phrases (fine-tuné sur des paires contrastives pré-bin) récupère les $k=32$ plus proches voisins d'énoncés basés sur la similitude cosinus.
Lissage : Un prior hiérarchiquement lissé $q_t(f|D)$ $q_{t} (f ∣ D)$ est construit comme un mélange des distributions de familles empiriques provenant de :
- Voisins récupérés ( $q_{r,t}$ )
- Espace de noms de la cible ( $q_{n,t}$ )
- Module de la cible ( $q_{m,t}$ )
- La bibliothèque pré-bin complète ( $q_{g,t}$ )
Optimisation : Les poids de mélange et les paramètres de lissage sont sélectionnés en maximisant la log-vraisemblance chronologique des familles observées dans les preuves antérieures, garantissant que le prior est prédictif plutôt que ajusté à l'étude humaine.

3. Score

Le score PriorProof $S_t(D)$ est la surprisal pondérée de l'empreinte observée sous le prior construit :
$S_t(D) = \sum_{i=1}^{m_D} w_i [-\log q_t(f_i | D)]$
Un score élevé indique qu'une preuve utilise des familles de dépendances qui étaient improbables pour des théorèmes antérieurs ayant des énoncés similaires. Pour les comparaisons par paires, la métrique sélectionne la preuve ayant le score le plus élevé, utilisant l'écart de score absolu $\Delta(A, B)$ comme signal de confiance interne.

Contributions Clés

Définition Mécanique : Une définition de la non-standardité de la route de preuve relative au temps comme surprisal de l'empreinte de dépendance, ne nécessitant aucune ontologie de technique construite à la main ni étiquettes humaines.
Discipline Temporelle : Une discipline de fuite rigoureuse où la récupération, le support de famille, les comptes de réutilisation et le fine-tuning de l'encodeur sont strictement restreints aux données pré-bin.
Étude Empirique : Une étude en aveugle sur la topologie de Mathlib impliquant une validation mécanique, une comparaison par trois évaluateurs et une base de référence par modèle de langage.
Preuve de Calibration de l'Extrémité : Preuve empirique que l'écart de score absolu sert d'indicateur de fiabilité candidat, où les écarts plus importants corrèlent avec un accord plus élevé avec les évaluateurs humains, bien que la relation ne soit pas une escalier monotone résolu.

Résultats

L'étude a évalué 100 présentations en aveugle (se réduisant à 76 paires de preuves distinctes) contre trois évaluateurs de domaine conservés et des bases de référence de modèles de langage (gpt-5/gpt-5-mini).

Accord avec les Évaluateurs : PriorProof est en accord avec la majorité des trois évaluateurs sur 53/76 paires (69,7 %).
- Paires Canoniques : 11/12 (91,7 %) sur 12 contrastes canoniques sélectionnés à la main.
- Paires Stratifiées : 42/64 (65,6 %) sur l'ensemble plus large.
Base de Référence du Modèle de Langage : La meilleure condition de modèle de langage est en accord sur 60/76 paires (78,9 %). Un test de McNemar comparant PriorProof et le modèle a produit $p=0,210$ , indiquant que la différence n'est pas établie statistiquement avec cet échantillon de taille.
Calibration de l'Écart de Score :
- Dans la tranche de l'écart de score le plus petit, l'accord était de 12/19 (63,2 %), compatible statistiquement avec le hasard.
- Dans la tranche de l'écart de score le plus grand, l'accord était de 16/19 (84,2 %).
- Les tranches intermédiaires étaient non monotones, et les intervalles de confiance étaient larges. L'article conclut que cela soutient une tendance de calibration de l'extrémité (les écarts élevés sont plus fiables) plutôt qu'une courbe de calibration universelle résolue.
Validation Mécanique : Les empreintes observées ont reçu une probabilité chronologique significativement plus élevée que les alternatives aléatoires. Les études d'ablation ont confirmé que les composants de récupération et de lissage contribuent de manière significative au score, tandis que les vérifications de redondance n'ont trouvé aucun « hit » vivant dans le corpus curaté (bien que le chemin imbriqué soit dormant en raison de limitations de l'arrière-plan).

Signification et Revendications

L'article présente PriorProof non pas comme un remplacement du jugement expert ou du modèle, ni comme une théorie complète de la nouveauté mathématique. Au lieu de cela, il est positionné comme un signal décomposable et ancré dans le temps.

Portée : La métrique cible spécifiquement si une route de preuve utilise des mécanismes antérieurs distribués de manière inattendue. Elle est aveugle à la nouveauté définitionnelle, à la valeur explicative, à l'élégance ou au crédit d'auteur.
Indicateur de Fiabilité : L'utilité principale identifiée est l'écart de score. Les résultats suggèrent que lorsque l'écart de score entre deux preuves est important, la préférence de la métrique est plus susceptible de s'aligner sur le jugement humain. Lorsque l'écart est faible, la métrique est moins fiable.
Limites : Les auteurs notent explicitement que la métrique peut être manipulée en ajoutant des mécanismes rares et non pertinents, et que l'implémentation actuelle manque de normalisation sensible aux sous-termes (la détection de redondance imbriquée est inactive). La portée statistique est limitée à un seul domaine mathématique (topologie) et à une taille d'échantillon spécifique.
Utilité Future : La métrique est destinée à être un instrument de recherche pour analyser les preuves formelles vérifiées, prioriser les cas pour examen expert, et étudier les preuves générées par machine pour voir si elles reproduisent des schémas attendus ou découvrent des routes méritant l'attention humaine. C'est un générateur d'hypothèses, pas un arbitre de l'originalité.