NEURAL NETWORK METHODS FOR MATHEMATICAL TEXTS FORMALISATION

Abstract

This paper examines the potential of large language models (LLMs) to automate the conversion of mathematical statements from natural language into formal expressions, thereby streamlining the process of solution generation. With advancements in artificial intelligence, particularly in natural language processing, models such as GPT-4 and LLaMA-3 present promising applications for mathematical formalisation tasks. These models showcase significant capabilities in text comprehension and translation, which help reduce ambiguities in natural language descriptions of mathematical problems. The effectiveness of these models is evaluated in the context of transitioning from natural language to mathematical formalism. While LLMs excel at semantic analysis and text translation, challenges persist in their application to precise computations and symbolic manipulation, which are critical for solving complex mathematical problems with accuracy. To address these limitations, integration with formal proof systems such as LEAN is explored, enhancing the process of generating formal proofs and ensuring logical consistency in mathematical arguments. Furthermore, the integration of LLMs with formal systems is investigated for its potential to facilitate the development of systems that automatically generate proofs from mathematical texts. By leveraging the strengths of LLMs in linguistic understanding and the precision of formal systems, a hybrid approach is proposed to improve the reliability of automated problem-solving processes. The findings indicate that with continued development, LLMs can significantly contribute to automating mathematical reasoning. However, ongoing refinement is necessary to fully realise their potential in academic and educational contexts, particularly in handling complex mathematical reasoning and extensive problem sets.