실제 세계 소프트웨어의 에이전트 기반 검증 최적화

요약

기존 코딩 에이전트는 동등성 검사에서 취약점을 보였습니다. 본 연구는 기계 검증된 증명을 통해 성능을 개선하면서도 원본 코드와 기능적으로 동일함을 보장하는 '에이전트 기반 검증 최적화'를 제안합니다. 이를 위해 C, C++, Go, Rust 등 다양한 언어를 지원하는 프레임워크 Aqueduct를 개발했습니다.

핵심 포인트

• 기존 에이전트는 동등성 검사에서 취약하여 의도된 동작을 보장하기 어려움.
• 에이전트 기반 검증 최적화는 기계 증명을 통해 성능 개선과 기능적 동등성을 동시에 확보함.
• Lean 4를 활용하여 함수 및 저장소 수준의 최적화를 공식화하고 프레임워크 Aqueduct를 개발함.
• 실제 애플리케이션에 적용 시, 알고리즘 변경을 포함한 증명된 리라이트가 속도 향상을 가져옴.