Formal Methods in the AI Era
Changes and possibilities brought about by the emergence of large language models
Changing Environment Surrounding Formal Methods
Formal methods are a technology with several decades of track record, but their adoption in general software development has been limited due to high barriers to entry. However, the rapid advancement of large language models (LLMs) is showing signs of change in this situation.
Support for Specification Writing: Since LLMs can handle both natural language and formal languages, support is becoming increasingly available for converting requirements expressed in natural language by domain experts into formal specifications. This has the potential to lower the barrier of mathematical expert knowledge.
Interactive Specification Refinement: A process of gradually clarifying ambiguous parts of specifications through dialogue with LLMs can be envisioned. By repeatedly asking clarifying questions such as "Is this interpretation correct?", implicit assumptions that humans have not noticed can be made explicit, with potential benefits.
Automation of Verification: By having AI handle test case generation and mock creation based on formal specifications, the process of early confirmation of specification validity has the potential to become more efficient.
Role of Formal Specifications in AI Agent Development
In an era where AI agents automatically generate code, formal specifications are thought to have potential for new roles.
Clear Instructions to AI: Natural language prompts tend to contain ambiguity, but formal specifications can provide mathematically unambiguous instructions to AI. This is expected to improve the quality and accuracy of code generated by AI.
Verification Standard for Generated Code: If a formal specification exists, the code generated by AI can be mechanically verified to conform to the specification. This provides an objective judgment criterion for the fundamental question 'Is the code written by AI correct?'
Contracts Between Multi-Agents: When multiple AI agents collaborate to conduct development, formal specifications can serve as a means to define module boundaries and contracts. With each agent's scope of responsibility clearly defined, there is potential to reduce problems at the time of integration.
Unsolved Challenges
While the combination of AI and formal methods has significant potential, many challenges remain to be solved at this time.
LLM Formal Specification Generation Accuracy: There is insufficient accumulation of knowledge about how accurately current LLMs generate formal specifications and under what conditions reliability deteriorates.
Scalability: While effective in small-scale systems, it remains to be verified whether the same approach functions for large and complex systems.
Redefinition of Human Role: How will the skills and roles required of humans change when AI handles formal specifications? New abilities such as expression of domain knowledge and ability to interact with AI may be needed.
IID Systems Research
IID Systems is researching an approach that leverages formal specifications using VDM-SL as contracts between AI agents. Specific methodologies and insights—such as specification-centric short-cycle development, interactive elicitation of non-functional requirements, and multi-agent collaborative architecture—are disclosed on the 'Research Projects' page.