LLM으로 안정성 증명서 합성하고 형식검증기로 검증
원제 LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
추천 12댓글 2
Key Point
동적 시스템의 안정성 증명이 형식검증기와 LLM으로 자동화되는 방식이 바뀌고 있으며, 기존 솔버 중심 접근을 넘는 실질적 성과를 보여준다.
핵심 요약
- Lyapunov 함수와 barrier certificate는 비선형 고차원 시스템의 안정성과 안전성을 보장하지만, 이들을 합성하고 검증하는 것은 여전히 난제이다.
- 기존 방식은 수치해석 솔버, 구간 방법, SMT 솔버 등을 사용하는데, 완화(relaxation)가 필요하거나 보수적이거나 차원과 비선형성에 따라 확장성이 나빠진다.
- 표준 벤치마크는 솔버가 다룰 수 있는 저차원 다항식 시스템으로 지배되어 실제 공학 응용과 거리가 있다.
- 이 논문은 105개 사례로 구성된 DynaCertBench 벤치마크를 제시하며, 80개의 기존 시스템에 고차원 변종과 새로운 비선형 결합 시스템을 추가했다.
- 안정성, 도달 영역, 전방 불변성, 안전성 등 4가지 작업을 포괄한다.
- LLM2Cert 프레임워크는 LLM으로 증명서 후보를 생성하고, SMT 솔버 또는 Lean Proof-Repair 에이전트로 검증한다.
- DynaCertBench에서 LLM2Cert는 105개 중 81개(77.1%)를 검증했으며, 피드백 없는 원샷(one-shot) 제안 대비 17.1 percentage point 개선했다.
- 81개의 검증된 증명서 중 22개는 All-SMT 방식이 미해결로 남긴 사례이다.