기능적 동등성 여부? 코드 동등성을 위한 그래프 기반 미분 서로게이트 실행

두 프로그램이 기능적으로 동등한지 판단하는 것은 코드 현대화, 패치 검증, 리팩토링 및 코드 생성 평가의 핵심입니다. 하지만 일반적인 신호들은 불완전합니다. 테스트는 유한한 입력만 커버하며, 텍스트적 유사성은 구현과 동작을 혼동시키고, 제약 없는 LLM 판단은 감사하기 어렵습니다. 프로그램이 구식이거나, 라이선스가 있거나, 이용할 수 없거나, 안전하지 않은 환경에 의존하는 경우 직접 실행은 종종 불가능합니다. 우리는 타입이 지정된 프로그램 그래프 증거와 미분 서로게이트 실행을 결합한 선택적 동등성 평가 에이전트인 FEAgent를 소개합니다. FEAgent는 먼저 공개 인터페이스와 동작적으로 관련된 그래프 앵커들을 정렬한 다음, 콜-플로우(call-flow), 제어-플로우(control-flow), 데이터-플로우(data-flow), 타입(type), 임포트(import), 효과 관계에 걸쳐 경계가 지정된 쿼리를 발행합니다. 다음으로, 브랜치 인식 생성기 에이전트가 차별화하는 입력들을 제안하고, 두 개의 블라인드 LLM 서로게이트가 소스 및 타겟 관측 가능한 값들을 독립적으로 예측합니다. 모든 주장과 예측된 불일치는 증거 원장(evidence ledger)에 기록됩니다. 이후 결정론적 조정기(deterministic reconciler)는 경로가 발견되거나 증거가 충돌하는 경우 결정을 강요하기보다는 EQUIVALENT, INEQUIVALENT 또는 UNCLEAR를 반환합니다. 우리는 함수 수준 동등성과 리포지토리 수준 버그 패치에서 FEAgent를 평가했으며, 여기서 기존의 오라클은 벤치마크 레이블이나 통과하는 테스트 스위트입니다. 이 오라클과의 모든 불일치는 직접 실행을 통해 심사되며, 이는 벤치마크 레이블의 오류와 유닛 테스트만으로는 포착되지 않은 동작적 편차를 드러냅니다. EquiBench에서 실행 결과는 평가된 1,200쌍 중 216쌍(18.0%)에 대해 FEAgent가 발표된 레이블과 불일치함을 확인했습니다. SWE-bench Verified에서는 테스트 통과 에이전트 패치 331개 중 94개(28.4%)가 참조 패치와 다름을 보여주었습니다. 따라서 FEAgent는 테스트와 형식 검증 사이의 감사 계층 역할을 하며, 증거를 검토 가능하게 유지하고 불확실성을 명시적으로 표현하면서도 동등성의 증명을 주장하지 않습니다.