Resumen: La prueba del teorema automatizado (ATP) en idiomas formales sigue siendo un desafío formidable en la IA, exigiendo una deducción lógica rigurosa y navegando en vastos espacios de búsqueda. Mientras que los modelos de lenguaje grande (LLM) han mostrado un rendimiento prometedor, los retrocesos existentes a menudo sufren una guía de búsqueda sesgada, lo que lleva a ineficiencias y estrategias de prueba subóptima. Este documento presenta el Prover de búsqueda multiperspectiva (PROVERSE MPS), un nuevo sistema ATP paso a paso diseñado para superar estas limitaciones. MPS-PROVER incorpora dos innovaciones clave: una estrategia de curación de datos posteriores a la capacitación altamente efectiva que poda aproximadamente el 40% de los datos de capacitación redundantes sin sacrificar el rendimiento, y un mecanismo de búsqueda de árboles de varias perspectivas. Esta búsqueda integra un modelo crítico aprendido con reglas heurísticas estratégicamente diseñadas para diversificar la selección de tácticas, evitar quedarse atrapados en estados improductivos y mejorar la robustez de búsqueda. Las evaluaciones extensas demuestran que el Provergido de MPS logra un rendimiento de vanguardia en múltiples puntos de referencia desafiantes, incluidos Minif2F y ProofNet, superando los modelos de parámetros 7B anteriores. Además, nuestros análisis revelan que los MPS-PROVER generan pruebas significativamente más cortas y más diversas en comparación con los métodos existentes a prueba de paso y a prueba, resaltan su eficiencia y eficacia. Nuestro trabajo avanza las capacidades del razonamiento formal basado en LLM y ofrece un marco sólido y un análisis integral para desarrollar Proverrones del teorema más potentes.
Publicado Originalme en rss.arxiv.org El 18 de mayo de 2025.
Ver Fuente Original
