IsabeLLM: 합의 알고리즘의 형식 검증에 적용된 자동 정리 증명 (Automated Theorem Proving)

인공지능 (AI)의 발전은 정리 증명 (Theorem Proving)을 위한 AI가 컴퓨터 시스템을 형식적으로 검증 (formally verifying)하는 유망한 수단이 되도록 이끌었습니다. 형식 검증 (formal verification)은 필요한 전문 지식과 노력의 양 때문에 전통적으로 안전 필수 (safety-critical) 시스템을 위해 예약되어 왔으나, AI는 이러한 작업량의 상당 부분을 자동화하고 훨씬 더 접근하기 쉽게 만드는 데 도움을 줄 수 있습니다. 블록체인 기반 시스템은 점점 더 인기를 얻고 있으며 악의적인 행위자들의 빈번한 공격 대상이 되고 있으며, 이는 종종 막대한 금융 손실로 이어져 이러한 시스템을 더 잘 검증하고 취약점을 완화해야 할 필요성을 강조합니다. 이러한 시스템에서 논쟁의 여지 없이 가장 중요한 구성 요소는 잠재적으로 적대적인 환경에서 노드들이 결정에 동의할 수 있도록 하는 합의 프로토콜 (consensus protocol)입니다. 본 논문에서 우리는 Isabelle 내의 자동 정리 증명 도구인 IsabeLLM을 개선합니다. 구체적으로, 우리는 대규모 언어 모델 (Large Language Model, LLM)에 제공되는 컨텍스트를 개선하기 위해 검색 증강 생성 (Retrieval-Augmented Generation, RAG) 프레임워크, 오류 추적 (Error tracing) 및 반례 생성 (counterexample generation)을 구현합니다. 또한 효율성 향상을 위해 최신 버전의 Isabelle 및 Sledgehammer와의 호환성도 구현되었습니다. 우리는 Bitcoin의 작업 증명 (Proof of Work) 합의 검증을 완료하는 능력에 있어 두 가지 버전의 IsabeLLM의 성능을 비교합니다.