Insights
AI가 자동으로 큐레이션·번역·정리하는 기술 동향 피드입니다.
DateSAT은 날짜 및 달력 기간 제약 조건을 표현하고 해결하기 위한 최초의 프레임워크입니다. 불규칙한 월 크기나 윤년 같은 복잡한 규칙을 처리하기 위해 SMT 공식으로 환원하는 다섯 가지 전략을 제안하며, Z3를 백엔드로 구현되었습니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 arXiv cs.PL (Programming Languages)의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기날짜와 달력 기간(즉, 일, 월, 년)은 소프트웨어, 데이터 및 문서 분석을 포함하는 작업에서 빈번하게 등장합니다. 이전 연구에 따르면, 날짜 및 달력 계산을 포함하는 컴퓨터 로직은 까다로운 규칙(예: 불규칙한 크기의 월), 모호성(예: "1월 31일"로부터 한 달 뒤의 일정 예약), 그리고 예외 케이스(예: 윤년)로 인해 오류가 발생하기 쉽다는 것이 밝혀졌습니다. 그러나 기존의 프로그램 분석 및 검증 도구들은 날짜에 대한 네이티브 지원(native support)을 제공하지 않아, 달력 산술(calendrical arithmetic)을 포함하는 연산을 기호적으로(symbolically) 추론하기 어렵습니다. 본 논문은 날짜 및 달력 기간을 포함하는 만족 가능성 제약 조건(satisfiability constraints)을 표현하고 해결하기 위한 최초의 프레임워크인 DateSAT을 제시합니다. 본 논문은 먼저 입력 언어와 날짜 및 기간 산술의 의미론(semantics)을 정형화합니다. 그런 다음, 정수(integers)를 포함하는 SMT 공식으로의 환원을 기반으로 DateSAT 제약 조건을 해결하기 위한 다섯 가지 별도의 전략을 제시하며, 이를 Z3를 백엔드(backend)로 사용하여 구현하였습니다. 우리는 LLM 프롬프팅(prompting), 문법 기반 샘플링(grammar-based sampling), 그리고 법률 문서 마이닝(mining legal documents)을 사용하여 합성된 450개의 DateSAT 제약 조건 데이터셋을 구축하였으며, DateSAT 솔버(solver) 성능에 대한 실증적 평가를 제시합니다.