Síntesis de programas

En 2013, investigadores de UPenn , UC Berkeley y MIT propusieron un marco unificado para problemas de síntesis de programas llamado Síntesis Guiada por Sintaxis (estilizada como SyGuS). [ ^{6 ] La} entrada a un algoritmo SyGuS consiste en una especificación lógica junto con una gramática de expresiones libre de contexto que restringe la sintaxis de las soluciones válidas. ^{[ 7 ]} Por ejemplo, para sintetizar una función f que devuelva el máximo de dos enteros, la especificación lógica podría ser la siguiente:

( f ( x , y ) = x ∨ f ( x , y ) = y ) ∧ f ( x , y ) ≥ x ∧ f ( x , y ) ≥ y

y la gramática podría ser:

< Exp > ::= x | y | 0 | 1 | < Exp > + < Exp > | ite( < Cond > , < Exp > , < Exp > ) < Cond > ::= < Exp > <= < Exp >

donde "ite" significa "si-entonces-si no". La expresión

iterar(x <= y, y, x)

Sería una solución válida, porque se ajusta a la gramática y a la especificación.

Desde 2014 hasta 2019, la Competencia Anual de Síntesis Guiada por Sintaxis (o SyGuS-Comp) comparó los diferentes algoritmos para la síntesis de programas en un evento competitivo. ^{[ 8 ]} La competencia utilizó un formato de entrada estandarizado, SyGuS-IF, basado en SMT-Lib 2 . Por ejemplo, el siguiente SyGuS-IF codifica el problema de sintetizar el máximo de dos enteros (como se presentó anteriormente):

(lógica de conjunto LIA) (synth-fun f ((x Int) (y Int)) Int ((i Entero) (c Entero) (b Booleano)) ((i Int (cxy (+ ii) (ite bii))) (c Int (0 1)) (b Booleano ((<= ii))))) (declarar-var x Int) (declarar-variable y Int) (restricción (>= (fxy) x)) (restricción (>= (fxy) y)) (restricción (o (= (fxy) x) (= (fxy) y))) (verificar-síntesis)

Un solucionador compatible podría devolver el siguiente resultado:

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

La síntesis inductiva guiada por contraejemplos (CEGIS) es un enfoque eficaz para construir sintetizadores de programas de sonido. ^{[ 9 ] [ 10 ]} CEGIS implica la interacción de dos componentes: un generador que genera programas candidatos y un verificador que comprueba si los candidatos satisfacen la especificación.

Dado un conjunto de entradas I , un conjunto de programas posibles P y una especificación S , el objetivo de la síntesis de programas es encontrar un programa p en P tal que para todas las entradas i en I , se cumpla S ( p , i ). CEGIS está parametrizado sobre un generador y un verificador:

• El generador toma un conjunto de entradas T y produce un programa candidato c que es correcto en todas las entradas de T , es decir, un candidato tal que para todas las entradas t de T , se cumple S ( c , t ).
• El verificador toma un programa candidato c y devuelve verdadero si el programa satisface S en todas las entradas, y de lo contrario devuelve un contraejemplo , es decir, una entrada e en I tal que S ( c , e ) falla.

CEGIS ejecuta el generador y el verificador en un bucle, acumulando contraejemplos:

El algoritmo cegis es la entrada : Generador de programas generar , verificador verificar , especificación spec , salida : Programa que satisface spec o falla entradas := conjunto vacío bucle candidato := generar ( especificación , entradas ) si verificar ( especificación , candidato ) entonces devolver candidato sino verificar produce un contraejemplo e agregar e a entradas fin si

Las implementaciones de CEGIS suelen utilizar solucionadores SMT como verificadores.

CEGIS se inspiró en el refinamiento de abstracción guiado por contraejemplos (CEGAR). ^{[ 11 ]}

Las reglas de demostración incluyen:

• Resolución no clausal (véase la tabla).

Por ejemplo, la línea 55 se obtiene resolviendo fórmulas de aserción.${\displaystyle E}$desde el 51 y${\displaystyle F}$de 52 que comparten alguna subfórmula común${\displaystyle p}$. La resolvente se forma como la disyunción de${\displaystyle E}$, con${\displaystyle p}$reemplazado por${\displaystyle {\it {true}}}$, y${\displaystyle F}$, con${\displaystyle p}$reemplazado por${\displaystyle {\it {false}}}$. Esta resolvente se deduce lógicamente de la conjunción de${\displaystyle E}$y${\displaystyle F}$. En términos más generales,${\displaystyle E}$y${\displaystyle F}$Es necesario tener solo dos subfórmulas unificables.${\displaystyle p_{1}}$y${\displaystyle p_{2}}$, respectivamente; su resolvente se forma entonces a partir de${\displaystyle E\theta }$y${\displaystyle F\theta }$como antes, donde${\displaystyle \theta }$es el unificador más general de${\displaystyle p_{1}}$y${\displaystyle p_{2}}$. Esta regla generaliza la resolución de cláusulas . ^{[ 22 ]}

Los términos del programa de las fórmulas principales se combinan como se muestra en la línea 58 para formar la salida de la resolvente. En el caso general,${\displaystyle \theta }$También se aplica a este último. Dado que la subfórmula${\displaystyle p}$aparece en la salida, se debe tener cuidado de resolver solo en subfórmulas que correspondan a propiedades computables .

• Transformaciones lógicas.

Por ejemplo,${\displaystyle E\land (F\lor G)}$puede transformarse en${\displaystyle (E\land F)\lor (E\land G)}$) tanto en las afirmaciones como en los objetivos, ya que ambos son equivalentes.

• Separación de afirmaciones conjuntivas y de objetivos disyuntivos.

Un ejemplo se muestra en las líneas 11 a 13 del siguiente ejemplo ilustrativo.

• Inducción estructural .

Esta regla permite la síntesis de funciones recursivas . Para una pre- y postcondición dadas "Dado${\displaystyle x}$de tal manera que${\displaystyle {\textit {pre}}(x)}$, encontrar${\displaystyle f(x)=y}$de tal manera que${\displaystyle {\textit {post}}(x,y)}$", y un ordenamiento adecuado proporcionado por el usuario${\displaystyle \prec }$del dominio de${\displaystyle x}$, siempre es recomendable añadir una aserción "${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$". ^{[ 23 ]} Resolver con esta aserción puede introducir una llamada recursiva a${\displaystyle f}$en el plazo del programa.

Un ejemplo se encuentra en Manna, Waldinger (1980), págs. 108-111, donde se sintetiza un algoritmo para calcular el cociente y el resto de dos enteros dados, utilizando el método del bien ordenado.${\displaystyle (n',d')\prec (n,d)}$definido por${\displaystyle 0\leq n'<n}$(pág. 110).

Murray ha demostrado que estas reglas son completas para la lógica de primer orden . ^{[ 24 ]} En 1986, Manna y Waldinger añadieron reglas generalizadas de resolución E y paramodulación para manejar también la igualdad; ^{[ 25 ]} posteriormente, estas reglas resultaron ser incompletas (pero no obstante correctas ). ^{[ 26 ]}

Como ejemplo sencillo, un programa funcional para calcular el máximo${\displaystyle M}$de dos números${\displaystyle x}$y${\displaystyle y}$se puede derivar de la siguiente manera.

Partiendo de la descripción del requisito " El máximo es mayor o igual que cualquier número dado, y es uno de los números dados ", la fórmula de primer orden${\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$se obtiene como su traducción formal. Esta fórmula debe ser demostrada. Mediante la skolemización inversa , ^{[ nota 4 ]} se obtiene la especificación en la línea 10, donde una letra mayúscula y una minúscula denotan una variable y una constante de Skolem , respectivamente.

Después de aplicar una regla de transformación para la ley distributiva en la línea 11, el objetivo de la demostración es una disyunción y, por lo tanto, se puede dividir en dos casos, a saber, las líneas 12 y 13.

En cuanto al primer caso, al resolver la línea 12 con el axioma de la línea 1 se produce la instanciación de la variable del programa.${\displaystyle M}$en la línea 14. Intuitivamente, el último conjuntivo de la línea 12 prescribe el valor que${\displaystyle M}$debe tomarse en este caso. Formalmente, la regla de resolución no clausal que se muestra en la línea 57 anterior se aplica a las líneas 12 y 1, con

• p es la instancia común x=x de A=A y x=M , obtenida al unificar sintácticamente las últimas fórmulas,
• F[ p ] siendo verdadero ∧ x=x , obtenido de la línea 1 instanciada (apropiadamente rellena para hacer visible el contexto F[⋅] alrededor de p ), y
• G[ p ] siendo x ≤ x ∧ y ≤ x ∧ x = x , obtenido de la línea instanciada 12,

flexible ${\displaystyle \lnot (}$verdadero ∧ falso ) ∧ ( x ≤ x ∧ y ≤ x ∧ verdadero${\displaystyle )}$, que se simplifica a${\displaystyle x\leq x\land y\leq x}$.

De manera similar, la línea 14 produce la línea 15 y luego la línea 16 por resolución. Además, el segundo caso,${\displaystyle x\leq M\land y\leq M\land y=M}$En la línea 13, se maneja de manera similar, lo que finalmente da como resultado la línea 18.

En un último paso, ambos casos (es decir, las líneas 16 y 18) se unen, utilizando la regla de resolución de la línea 58; para que esa regla sea aplicable, fue necesario el paso preparatorio 15 → 16. Intuitivamente, la línea 18 podría leerse como "en caso${\displaystyle x\leq y}$, la salida${\displaystyle y}$es válido (con respecto a la especificación original), mientras que la línea 15 dice "en caso${\displaystyle y\leq x}$, la salida${\displaystyle x}$es válido; el paso 15 → 16 estableció que ambos casos 16 y 18 son complementarios. ^{[ nota 5 ]} Dado que tanto la línea 16 como la 18 vienen con un término de programa, una expresión condicional da como resultado la columna del programa. Dado que la fórmula objetivo${\displaystyle {\textit {true}}}$Se ha derivado, la prueba está hecha y la columna del programa de la "${\displaystyle {\textit {true}}}$"La línea contiene el programa.