AI for software engineering: from probable to provable

• URL: http://arxiv.org/abs/2511.23159v1
• Date: Fri, 28 Nov 2025 13:14:45 GMT
• Title: AI for software engineering: from probable to provable
• Authors: Bertrand Meyer,
• Abstract summary: This paper looks at how to combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification.<n>The solution? Combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification.
• Score: 31.729786132250425
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Vibe coding, the much-touted use of AI techniques for programming, faces two overwhelming obstacles: the difficulty of specifying goals ("prompt engineering" is a form of requirements engineering, one of the toughest disciplines of software engineering); and the hallucination phenomenon. Programs are only useful if they are correct or very close to correct. The solution? Combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification, supported by modern proof tools.

Related papers

• Agentic AI for Software: thoughts from Software Engineering community [9.966138715949205]
  At the code level, common software tasks include code generation, testing, and program repair.<n>Key to successfully developing agentic AI-based software will be to resolve the core difficulty in software engineering - the deciphering and clarification of developer intent.<n>A successful deployment of agentic technology into software engineering would involve making conceptual progress in such intent inference via agents.
  arXiv  Detail & Related papers  (2025-08-24T12:57:21Z)
• Quantum Artificial Intelligence for Software Engineering: the Road Ahead [9.447783914028262]
  This paper presents a roadmap towards the application of Quantum AI (QAI) in software engineering.<n>We consider two of the main categories of QAI, i.e., quantum optimization algorithms and quantum machine learning.<n>We provide an overview of some of the possible challenges that need to be addressed to make the application of QAI for software engineering successful.
  arXiv  Detail & Related papers  (2025-05-07T20:47:18Z)
• Challenges and Paths Towards AI for Software Engineering [55.95365538122656]
  We discuss progress in AI for software engineering in threefold manner.<n>First, we provide a structured taxonomy of concrete tasks in AI for software engineering.<n>Second, we outline several key bottlenecks that limit current approaches.
  arXiv  Detail & Related papers  (2025-03-28T17:17:57Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  We advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level.<n>We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
  arXiv  Detail & Related papers  (2024-12-20T17:19:24Z)
• Abstraction Engineering [6.091612632147657]
  Abstraction is already used across many disciplines involved in software development. This paper looks at these new challenges and proposes to address them through the lens of Abstraction. We discuss the foundations of Abstraction Engineering, identify key challenges, highlight the research questions that help address these challenges, and create a roadmap for future research.
  arXiv  Detail & Related papers  (2024-08-26T07:56:32Z)
• AI in Software Engineering: A Survey on Project Management Applications [3.156791351998142]
  Machine Learning (ML) employs algorithms that undergo training on data sets, enabling them to carry out specific tasks autonomously. AI holds immense potential in the field of software engineering, particularly in project management and planning.
  arXiv  Detail & Related papers  (2023-07-27T23:02:24Z)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  We study whether conveying information about uncertainty enables programmers to more quickly and accurately produce code. We find that highlighting tokens with the highest predicted likelihood of being edited leads to faster task completion and more targeted edits.
  arXiv  Detail & Related papers  (2023-02-14T18:43:34Z)
• Automated Machine Learning: A Case Study on Non-Intrusive Appliance Load Monitoring [81.06807079998117]
  We propose a novel approach to enable Automated Machine Learning (AutoML) for Non-Intrusive Appliance Load Monitoring (NIALM)<n>NIALM offers a cost-effective alternative to smart meters for measuring the energy consumption of electric devices and appliances.
  arXiv  Detail & Related papers  (2022-03-06T10:12:56Z)
• Competition-Level Code Generation with AlphaCode [74.87216298566942]
  We introduce AlphaCode, a system for code generation that can create novel solutions to problems that require deeper reasoning. In simulated evaluations on recent programming competitions on the Codeforces platform, AlphaCode achieved on average a ranking of top 54.3%.
  arXiv  Detail & Related papers  (2022-02-08T23:16:31Z)
• The application of artificial intelligence in software engineering: a review challenging conventional wisdom [0.9651131604396904]
  This survey chapter is a review of the most commonplace methods of AI applied to software engineering. The review covers methods between years 1975-2017, for the requirements phase, 46 major AI-driven methods are found. The purpose of this chapter is to answer the following questions: is there sufficient intelligence in the SE lifecycle?
  arXiv  Detail & Related papers  (2021-08-03T15:59:59Z)
• Explainable AI for Software Engineering [12.552048647904591]
  We first highlight the need for explainable AI in software engineering. Then, we summarize three successful case studies on how explainable AI techniques can be used to address the aforementioned challenges.
  arXiv  Detail & Related papers  (2020-12-03T00:42:29Z)
• Machine Learning for Software Engineering: A Systematic Mapping [73.30245214374027]
  The software development industry is rapidly adopting machine learning for transitioning modern day software systems towards highly intelligent and self-learning systems. No comprehensive study exists that explores the current state-of-the-art on the adoption of machine learning across software engineering life cycle stages. This study introduces a machine learning for software engineering (MLSE) taxonomy classifying the state-of-the-art machine learning techniques according to their applicability to various software engineering life cycle stages.
  arXiv  Detail & Related papers  (2020-05-27T11:56:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.