에이전틱 코드 추론: 실행 없이 코드 의미를 분석하는 세미-포멀 추론 기법

기존 LLM 에이전트는 코드를 실행하지 않고 분석할 때 추측에 의존해 오류를 범하는 경우가 많았다. 이 논문은 구조화된 논리 단계를 강제하는 방법론을 통해 실행 환경 구축 없이도 정밀한 코드 분석이 가능함을 입증했다. 이는 보안이나 복잡한 레거시 시스템처럼 실행이 어려운 환경에서 AI의 활용도를 극대화한다.

Transformer 기반의 LLM은 Chain-of-Thought(CoT)를 통해 복잡한 문제를 풀 수 있지만, 코드 분석 시에는 함수 이름이나 변수명만 보고 동작을 짐작하는 '추측성 오류'에 취약하다. 특히 여러 파일에 걸쳐 함수가 호출되는 경우, 중간 과정을 생략하고 결과만 내놓는 경향이 있어 신뢰도가 떨어진다.

이 논문은 이를 해결하기 위해 수학적 증명(Formal)과 자연어 사고(Informal)의 중간 단계인 '세미-포멀' 구조를 제안한다. 이는 에이전트에게 사고의 자유를 주되, 반드시 각 단계마다 코드상의 증거(Evidence)를 문서화하도록 강제하는 방식이다. 마치 개발자가 코드를 한 줄씩 머릿속으로 따라가며(Tracing) 버그를 찾는 과정을 정형화된 서식으로 만든 것과 같다.

이러한 구조화는 에이전트가 함수 내부를 실제로 탐색하게 만들고, 변수의 상태 변화를 명시적으로 기록하게 유도한다. 결과적으로 '이름이 같으니 똑같이 동작하겠지'라는 안일한 판단을 막고, 실행 없이도 실제 런타임에서 발생할 수 있는 미묘한 차이를 발견할 수 있게 한다.

세미-포멀 추론은 네 가지 핵심 단계로 구성된 템플릿을 사용한다. 첫째, PREMISES 단계에서 각 패치가 수정하는 파일과 변경 사항을 명시한다. 둘째, ANALYSIS 단계에서 특정 테스트 케이스에 대해 각 패치가 어떻게 반응할지 실행 경로(Execution Trace)를 기술한다. 셋째, COUNTEREXAMPLE 단계에서 두 패치의 결과가 달라지는 구체적인 지점을 식별한다. 마지막으로 CONCLUSION 단계에서 논리적 근거를 바탕으로 최종 판정을 내린다.

수학적 개념인 '테스트 기반 패치 등가성(Patch Equivalence Modulo Tests)'은 다음과 같이 계산된다. [두 개의 패치 P1, P2와 테스트 수트 T 입력] → [각 패치를 적용한 상태에서 T의 통과/실패 여부를 각각 예측] → [두 예측 결과 벡터가 완벽히 일치하는지 비교] → [일치하면 등가, 다르면 비등가로 판정]. 이 과정에서 에이전트는 [입력값 → 함수 호출 → 상태 변화 → 출력값]의 순서로 연산 원리를 풀어서 서술해야 한다.

상호 절차적 추론(Interprocedural Reasoning)을 강화하기 위해, 에이전트가 함수 호출을 만날 때마다 해당 함수의 정의를 찾아가서 분석하도록 유도하는 구조를 갖췄다. 이는 단순히 함수의 시그니처만 보는 것이 아니라, 실제 구현부의 로직이 현재 맥락의 변수들과 어떻게 상호작용하는지를 추적하게 함으로써 정확도를 높인다.

Opus-4.5 모델을 사용한 패치 등가성 검증 실험에서 세미-포멀 추론은 88.8%의 전체 정확도를 기록하여 표준 추론(78.2%)을 크게 앞질렀다. 특히 등가 패치를 맞추는 정확도는 93%에 달해, 실행 없이도 높은 신뢰도의 보상 신호를 생성할 수 있음을 보여주었다.

결함 위치 식별(Fault Localization) 벤치마크인 Defects4J에서는 Top-5 정확도가 표준 에이전틱 방식 대비 5~12%p 향상되었다. 이는 에이전트가 단순히 에러 메시지에 의존하지 않고, 코드의 논리적 흐름을 추적하여 버그의 근본 원인을 더 잘 찾아냈음을 의미한다.

코드 질의응답(RubberDuckBench)에서도 세미-포멀 방식은 87.0%의 정확도를 달성하여 표준 방식(78.3%)보다 8.7%p 높은 성능을 보였다. 분석 결과, 구조화된 템플릿이 에이전트의 '이름 기반 추측'을 억제하고 실제 데이터 흐름을 분석하도록 강제한 것이 주요 승인이었다.

본 연구의 핵심은 LLM의 추론 과정을 '인증서(Certificate)' 형태로 정형화한 것이다. 이는 기존의 비구조화된 CoT가 가진 불투명성을 해결한다. 세미-포멀 템플릿은 에이전트가 논리적 비약을 할 수 없도록 칸 채우기 형식을 취하며, 이는 사람이 에이전트의 판단 근거를 검토할 때도 매우 유리하다.

기술적으로는 'PREMISE → CLAIM → PREDICTION'으로 이어지는 추론 체인을 구축했다. 모든 예측은 반드시 명시된 전제와 코드상의 증거로부터 도출되어야 한다. 이는 형식 검증(Formal Verification)의 엄격함과 LLM의 유연한 언어 이해 능력을 결합한 하이브리드 접근 방식이다.

구현 측면에서 에이전트는 bash 도구를 사용하여 코드베이스를 탐색하며, 최대 100단계의 상호작용을 통해 컨텍스트를 수집한다. 이 과정에서 에이전트는 스스로 가설을 세우고(Hypothesis), 코드를 읽어 이를 확인하거나 수정하는 '자기 반성(Self-reflection)' 과정을 거친다.

한계점으로는 여전히 매우 복잡한 간접 참조(Indirection)나 소스 코드가 없는 서드파티 라이브러리의 동작을 추측할 때 오류가 발생할 수 있다는 점이 확인되었다. 또한 표준 추론 대비 약 2.8배 더 많은 추론 단계가 필요하여 계산 비용이 증가하는 트레이드오프가 존재한다.

에이전트가 소스 코드를 볼 수 없는 서드파티 라이브러리의 동작을 추측할 때 오류가 발생한다. 또한 매우 복잡한 간접 참조(Indirection)가 포함된 버그를 놓치는 경향이 있으며, 표준 추론보다 약 2.8배 더 많은 단계를 거쳐야 하므로 추론 비용이 높다.