Assistentes baseados em llms no desenvolvimento de software e na prova de teoremas

Abstract

Este trabalho apresenta uma análise do impacto de assistentes de código baseados em LLM (Large Language Model) no desenvolvimento de software e na provas de teoremas. Além de uma análise de alguns trabalhos relacionados a este campo, o trabalho apresenta um relato da experiência do autor no desenvolvimento de um projeto de software, utilizando assistentes baseados em LLMs. Também fizemos uma análise de como os assistentes de código baseados em IA lidam com assistentes de prova de teoremas como o Lean. No final, é feita uma projeção como será a inserção dessas ferramentas no futuro da criação de software.

This paper presents an analysis of the impact of LLM-based code assistants on software development and theorem proving. In addition to a review of some works related to this field, it is presented an account of the author’s experience in developing a software project using LLM-based assistants. We also conducted an analysis of how AI-based code assistants interact with theorem proving assistants such as Lean. In conclusion, a analisys is made regarding the integration of these tools into the future of software development.