Daily Arxiv

Esta página recopila y organiza artículos sobre inteligencia artificial publicados en todo el mundo.
La información aquí presentada se resume utilizando Google Gemini y el sitio se gestiona sin fines de lucro.
Los derechos de autor de los artículos pertenecen a sus autores y a las instituciones correspondientes; al compartir el contenido, basta con citar la fuente.

APOLLO: LLM automatizado y colaboración Lean para razonamiento formal avanzado

Created by
  • Haebom

Autor

Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

Describir

APOLLO es un sistema automatizado de demostración de teoremas que combina el compilador Lean y la capacidad de razonamiento de LLM para demostrar teoremas matemáticos. Mientras que los métodos convencionales de demostración de teoremas basados en LLM generan pruebas que superan los sistemas de verificación mediante numerosos (miles) muestreos, APOLLO utiliza un flujo de trabajo modular en el que LLM genera pruebas, los agentes corrigen errores sintácticos en las pruebas, Lean identifica errores, aísla subteoremas fallidos, utiliza un solucionador automático y ejecuta LLM de forma económica en los objetivos restantes. Este proceso de recombinación y reverificación de las subpruebas corregidas se repite hasta un número máximo de intentos controlable por el usuario. En el benchmark miniF2F, alcanza una precisión del 84,9 % en modelos con menos de 8 000 millones de parámetros, manteniendo un coste de muestreo inferior a 100. Además, mejora la precisión de GoedelProverSFT al 65,6 % y reduce la complejidad de la muestra de 25 600 a varios cientos.

Takeaways, Limitations

•
Takeaways:
◦
Demostramos que las modificaciones específicas de la guía del compilador a la salida de LLM mejoran significativamente la eficiencia y la precisión.
◦
Presentamos un paradigma general escalable para la demostración automática de teoremas.
◦
Se logró una alta precisión con un bajo costo de muestreo (84,9 % en el benchmark miniF2F, 65,6 % en GoedelProverSFT).
◦
Se mejoró significativamente la precisión de los modelos de propósito general (del 3-7% a más del 40%).
•
Limitations:
◦
Actualmente, solo se presenta el rendimiento de puntos de referencia específicos (miniF2F, GoedelProverSFT) y la generalización a otros puntos de referencia o teoremas más complejos requiere más investigación.
◦
El rendimiento de APOLLO depende de los compiladores LLM y Lean utilizados, y se necesita más investigación sobre su compatibilidad y portabilidad con otros sistemas.
◦
Se necesita más investigación sobre la optimización de parámetros, como por ejemplo establecer un número máximo de intentos controlable por el usuario.
👍
Made with Slashpage