Los investigadores presentan LAMP, un marco multiagente que sintetiza pruebas verificadas por el kernel de Lean 4 para la Combinatoria sobre Palabras proporcionando conocimiento estructurado del dominio a través de una ontología. Este enfoque aborda la falta de lemas especializados en probadores existentes entrenados principalmente con datos de Mathlib.
- Los autores presentan una nueva formalización en Lean 4 de la Combinatoria sobre Palabras que contiene ocho módulos y 93 declaraciones de definiciones centrales y lemas fundamentales.
- LAMP coordina un Planificador, Constructor y Verificador utilizando acceso al Protocolo de Contexto del Modelo a la ontología específica del dominio sin requerir ajuste fino del probador.
- En pruebas a través de 90 teoremas que abarcan tres niveles de dificultad, LAMP sintetizó pruebas verificadas para el 96.7% de los casos, superando a las líneas base sin andamiaje y a probadores especializados.
- Los estudios de ablación indican que eliminar la arquitectura basada en herramientas o separar el Planificador del Constructor reduce cada uno el rendimiento en aproximadamente 12 puntos porcentuales.
Este marco permite la síntesis confiable de pruebas en dominios matemáticos poco representados al aprovechar conocimiento estructural explícito en lugar de depender únicamente de las capacidades del modelo.