Claude sotmet a examen les seves proves de programari

De provar exemples a demostrar una regla

Anthropic presenta un mètode que parteix de les proves que els desenvolupadors ja havien preparat. Aquestes proves reben entrades i assenyalen determinats errors fent que el programa falli. El treball transforma aquesta condició en una especificació matemàtica: demostrar que no es produeix cap fallada per a cap entrada dins de l'abast definit.

Segons l'empresa, la diferència respecte de generar moltes entrades de prova és l'abast de l'afirmació. Executar exemples serveix per buscar casos que facin fallar el programa, però no garanteix recórrer tots els camins possibles. Una demostració vàlida descarta les fallades previstes al llarg de qualsevol camí accessible des del punt d'entrada, sempre dins de les condicions establertes.

Qui escriu la prova i qui l'accepta

Segons Anthropic, la biblioteca i la prova existent es compilen per obtenir un executable. A partir d'aquest executable, dels models formals i de la propietat d'absència de fallades es genera l'especificació que ha de satisfer la demostració. Claude escriu la prova; el nucli de Rocq comprova que s'ajusta a aquesta especificació.

Segons l'empresa, el volum de les demostracions no obliga a revisar manualment cada línia. Cal confiar en els models de la màquina i del sistema operatiu, en els enunciats exactes que s'han demostrat i en el mateix comprovador. Aquesta separació permet verificar el resultat del model, però manté components de confiança que han de continuar sent correctes.

La garantia té un perímetre

Anthropic afirma que el resultat es refereix als executables compilats i als punts d'entrada verificats. La garantia inclou que l'execució acabi amb normalitat, sense els errors de memòria ni les assercions fallides previstos, per a les respostes del sistema operatiu i les distribucions de memòria modelades. Les condicions d'execució formen part del resultat, no són detalls intercanviables.

Buscar errors mentre es construeix la demostració

Anthropic afirma que els intents de demostració van descobrir errors que les proves automàtiques difícilment haurien trobat. Alguns requerien entrades grans amb una estructura molt concreta o una seqüència particular d'operacions. El procediment permetia corregir el codi, regenerar l'especificació i continuar la demostració sobre la versió modificada.

Segons l'empresa, aquesta capacitat de modificar el programa exigia vigilar els pedaços. Els investigadors penalitzaven qualsevol modificació i premiaven que es demostrés quines entrades canviaven de comportament i que fossin poques. També registraven i auditaven els pedaços per detectar dreceres que complissin l'objectiu formal a costa d'alterar la tasca.

El que continua fora de la demostració

Segons Anthropic, els executables estudiats fan servir una arquitectura i una manera d'enllaçar les biblioteques que difereixen de les de moltes instal·lacions reals. La demostració no es pot aplicar automàticament a altres màquines o configuracions. A més, el mecanisme que detecta errors de memòria no els identifica tots: demostrar que no s'activen les seves alarmes no cobreix els errors que aquest mecanisme no observa.

Anthropic sosté que tampoc no es van verificar tots els punts d'entrada de cada biblioteca. Fins i tot si es cobrissin tots, podrien quedar parts sense cobrir, com ara el codi al qual no es pot arribar des d'aquests punts. Una altra aplicació pot fer un mal ús d'una biblioteca i corrompre la seva pròpia memòria; cobrir aquesta mancança requereix especificar les obligacions de qui crida cada funció i respectar-les.