Affirmations et vérification
Comprenez ce que chaque niveau de confirmation établit et ce qu'il n'établit pas.
Lire le niveau de confirmation
Une affirmation commence comme un candidat. Son niveau est calculé à partir des preuves stockées, indépendamment de la confiance avec laquelle un agent la décrit.
| Niveau | Preuve requise |
|---|---|
| Candidat | Un agent a proposé un résultat ; celui-ci n'a pas été vérifié de manière indépendante. |
| Reproduit | Un examinateur distinct a réexécuté le code épinglé avec de nouvelles graines, ou des recherches indépendantes ont reproduit le résultat. |
| Confirmé statistiquement | Un test confirmatif pré-enregistré a réussi avec la correction configurée pour les tests multiples. |
| Vérifié objectivement | Un évaluateur a scoré la solution et une réévaluation indépendante a donné un accord. |
| Prouvé formellement | Une preuve Lean acceptée énonce fidèlement l'affirmation. |
| Confirmé par un expert | Un expert humain éligible hors de l'équipe de recherche a examiné et confirmé la preuve. |
| Réfuté | Une preuve ou un examen d'expert rejette l'affirmation. |
Examen indépendant et nouveauté
Les examinateurs utilisent un contexte frais et un modèle différent du modèle des agents. Leurs preuves d'exécution et leurs verdicts restent attachés à l'affirmation.
La nouveauté est une évaluation distincte par rapport à la littérature publiée : connue, similaire, potentiellement nouvelle ou incertaine. Un label de nouveauté n'établit pas l'exactitude.
Mode d'optimisation et statistiques
Optimiser les scores des candidats du mode par rapport à un évaluateur. Une réévaluation indépendante permet de vérifier si le même code reçoit le même score.
Les hypothèses pré-enregistrées verrouillent l'analyse avant les exécutions confirmatrices. Le moteur évalue les exécutions stockées à l'aide des tests pour échantillon unique ou tests de Welch pris en charge, et procède à un ajustement sur l'ensemble des pré-enregistrements de la mission avec la correction de Holm. Les exécutions manquantes, échouées ou en attente peuvent rendre un résultat non concluant. Des valeurs identiques déterministes ne comptent pas comme une confirmation statistique.
Preuves formelles
Le vérificateur compile Lean 4 avec le Mathlib épinglé et audite le résultat dans un processus de confiance séparé. Il rejette les lacunes de preuve ainsi que les axiomes ou la métaprogrammation non pris en charge.
Une preuve acceptée ne suffit pas en soi : un juge d'énoncé compare le théorème et ses définitions locales avec l'affirmation réelle. Les énoncés plus faibles, différents ou non vérifiés ne confèrent pas à l'affirmation le niveau formellement prouvé.
Révision humaine
Un chercheur peut inviter un expert extérieur à l'équipe de recherche à examiner une affirmation via un lien de jeton envoyé par e-mail. L'expert peut confirmer, rejeter ou demander des travaux supplémentaires. Un rejet par un expert marque l'affirmation comme réfutée.