형식 계약(Formal contracts)은 소프트웨어 테스트 및 검증에 필수적이지만, 작성하는 과정 자체가 노동 집약적이고 오류가 발생하기 쉽습니다. LLM은 자연어 사양으로부터 실행 가능한 단언(executable assertions)을 합성함으로써 자동 형식화(autoformalization)라는 유망한 경로를 제공하며, 이를 통해 비형식적인 개발자의 의도와 공식적인 실행 가능 사양 사이의 격차를 해소합니다. 우리는 Monty: 단언에 대한 자동 형식화 프레임워크를 제시합니다. 이 프레임워크는 단언의 유효성 기대(expectations of validity) 및 자연어의 모호성 문제를 다룹니다. 우리의 기술은 새로운 적합도 점수 측정법(conformance score metric)을 사용하여 형식화를 필터링하고, 공식화된 단언에 대해 코드를 테스트하여 얻은 유효성 점수를 기반으로 합니다. 우리는 22개의 컬렉션형 Java 클래스에서 파생된 541개의 단언 생성 작업에 걸쳐 우리의 접근 방식을 평가했으며, 이 기술이 단언을 번역하기 위해 LLM을 단순하게 사용하는 경우보다 더 신뢰성 있게 정답(ground truth)을 생성함을 보여줍니다 (평균적으로 정밀도에서 최대 20점 향상).