Formalize Everything

Language models are being used to assist human work across various fields, including coding and documentation, based on their ability to address both natural and formal language. However, we should now be able to use language models to define new problems and solve them. Specification writing using formal language is a prime example of such problems.

Writing specifications in formal language is crucial for verification and accuracy, but it requires so much time and effort that it is rarely done except for very important projects. However, by utilizing language models, we can write specifications in natural language and convert them to formal language, significantly reducing the time and effort required for specification writing.

One challenging aspect is that there is no clear way to verify whether the natural language has been properly translated into formal language. This is a new problem that no one has considered before, as translating natural language into formal language was previously impossible.

Nevertheless, its impact is undoubtedly clear. It will become possible to write and verify all rules, including requirements, laws, and security regulations, in formal language. The technology of translating natural language into formal language will serve as a bridge for programming language theory to solve real-world problems beyond programming languages. We hope our research will become the foundation for this future.