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

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