대규모 언어 모델(LLMs)의 발전에도 불구하고, 형식 소프트웨어 검증을 위한 자동 증명 생성은 여전히 상당 부분 해결되지 않은 문제로 남아 있다. LLM은 자연어처리(NLP), 비전, 코드 생성에서는 우수한 성능을 보이지만, 형식 검증은 여전히 상당한 인력 투입을 필요로 한다. 대화형 정리 증명(ITP)은 엄격한 논리 제약 하에서 수작업으로 증명을 구성해야 하므로 확장성이 제한되는데, 예를 들어 seL4 마이크로커널을 검증하는 데는 수십 년의 노력이 요구되었다. 기존의 LLM 기반 접근법은 이 과정을 자동화하려고 시도하지만 여전히 한계가 있다. 대부분은 단발성 생성 또는 얕은 검색에 의존하는데, 이는 소규모 증명에는 효과적일 수 있으나, 깊은 구조적 의존성을 갖는 크고 상호 연관된 검증 과제로는 확장되지 못한다. 본 연구에서는 PROMISE(PROof MIning via Structural Embeddings)를 제시한다. PROMISE는 증명 생성을 증명 상태 전이(proof-state transitions)에 대한 상태 기반 탐색(stateful search)으로 재구성하는, 구조를 인지하는 프레임워크이다. 표면 수준의 검색 대신, PROMISE는 증명 상태와 전술(tactic) 전이로부터 구조적 패턴을 채굴(mines)하여 반복적 탐색 과정에서 호환되는 증명 조각(proof fragments)을 검색하고 적응할 수 있게 한다. 우리는 PROMISE를 seL4 벤치마크에서 여러 LLM 백엔드에 걸쳐 평가하고 Selene 및 Rango와 같은 기존 시스템과 비교한다. PROMISE는 일관되게 기존 방법보다 우수한 성능을 보이며, 모델 전반에 걸친 견고성을 유지하면서 최대 +26점 향상(상대적 증가 186%)을 달성한다. 이는 확장 가능한 정리 증명을 위한 구조 인지형 증명 채굴의 효과를 보여준다.

*본 초록은 AI를 통해 원문을 번역한 내용입니다. 정확한 내용은 하기 원문에서 확인해주세요.