Our thesis tackles the challenge of translating natural language (NL) into first-order logic (FOL), an area where traditional methods have struggled due to the inherent ambiguity of natural language. By addressing this ambiguity, we aim to enhance the clarity and precision of automated reasoning. Our study focuses on utilizing the latest 7 billion parameter version of Llama2, optimized with techniques like LoRa and quantization, and integrating it with Z3, a state-of-the-art theorem prover. This integration facilitates the automatic determination of the truth value of a set of premises and a conclusion, ensuring logical consistency and accuracy. We employ a dual approach that involves fine-tuning Llama2 for enhanced NL to FOL translation and leveraging Z3 to check the satisfiability of these premises. We are impressed by the notable results of our study, with the model achieving nearly 70 percent accuracy in FOL validity for a set of premises and a conclusion. This performance not only aligns with but also slightly surpasses current benchmarks in the field, indicating a high rate of correct translations. The integration of a generative model like Llama2 with a deterministic solver like Z3 represents a significant advancement in the realm of automated reasoning and natural language processing. Our work contributes to the field by presenting a novel method that offers more accurate and logically consistent NL to FOL translations than existing approaches. It opens new pathways for sophisticated, reliable AI systems, bridging the gap between machine learning and formal logic, and enhancing the ability to automatically evaluate logical validity.
Nuestra tesis aborda el desafío de traducir el lenguaje natural (NL) a lógica de primer orden (FOL), un área donde los métodos tradicionales han tenido dificultades debido a la ambigüedad inherente del lenguaje natural. Al abordar esta ambigüedad, buscamos mejorar la claridad y precisión del razonamiento automatizado. Nuestro estudio se centra en utilizar la última versión de 7 mil millones de parámetros de Llama2, optimizada con técnicas como LoRa y cuantización, e integrarla con Z3, un demostrador de teoremas de vanguardia. Esta integración facilita la determinación automática del valor de verdad de un conjunto de premisas y una conclusión, asegurando consistencia lógica y precisión. Empleamos un enfoque dual que involucra el ajuste fino de Llama2 para una mejor traducción de NL a FOL y el uso de Z3 para verificar la satisfacibilidad de estas premisas. Estamos impresionados por los resultados notables de nuestro estudio, con el modelo logrando casi un 70 por ciento de precisión en la validez de FOL para un conjunto de premisas y una conclusión. Este rendimiento no solo se alinea con, sino que también supera ligeramente los puntos de referencia actuales en el campo, indicando una alta tasa de traducciones correctas. La integración de un modelo generativo como Llama2 con un solucionador determinista como Z3 representa un avance significativo en el ámbito del razonamiento automatizado y el procesamiento del lenguaje natural. Nuestro trabajo contribuye al campo presentando un método novedoso que ofrece traducciones de NL a FOL más precisas y lógicamente consistentes que los enfoques existentes. Abre nuevos caminos para sistemas de IA sofisticados y confiables, cerrando la brecha entre el aprendizaje automático y la lógica formal, y mejorando la capacidad de evaluar automáticamente la validez lógica.
