모든 것을 형식화하라

언어 모델은 자연어와 형식 언어를 모두 다룰 수 있는 능력을 바탕으로 코딩과 문서화를 포함한 다양한 분야에서 인간의 작업을 보조하는 데 사용되고 있습니다. 하지만 이제 우리는 언어 모델을 사용하여 새로운 문제를 정의하고 해결할 수 있어야 합니다. 형식 언어를 사용한 명세 작성이 그러한 문제의 대표적인 예입니다.

형식 언어로 명세를 작성하는 것은 검증과 정확성을 위해 중요하지만, 너무 많은 시간과 노력이 필요하여 매우 중요한 프로젝트를 제외하고는 거의 수행되지 않습니다. 하지만 언어 모델을 활용하여 자연어로 명세를 작성하고 이를 형식 언어로 변환함으로써 명세 작성에 필요한 시간과 노력을 크게 줄일 수 있습니다.

도전적인 측면 중 하나는 자연어가 형식 언어로 제대로 번역되었는지 검증할 명확한 방법이 없다는 것입니다. 이는 이전에는 자연어를 형식 언어로 번역하는 것이 불가능했기 때문에 아무도 고려하지 않았던 새로운 문제입니다.

그럼에도 불구하고 그 영향은 분명히 명확합니다. 요구사항, 법률, 보안 규정을 포함한 모든 규칙을 형식 언어로 작성하고 검증하는 것이 가능해질 것입니다. 자연어를 형식 언어로 번역하는 기술은 프로그래밍 언어 이론이 프로그래밍 언어를 넘어 실세계 문제를 해결하는 다리 역할을 할 것입니다. 우리의 연구가 이러한 미래의 기반이 되기를 바랍니다.