💻 computer science

Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

이 논문은 신뢰할 수 없는 LLM이 프로그래밍 언어 간의 자기 인증 및 충실도 등급이 매겨진 번역을 생성할 수 있도록 하는 Lean 4 기계화된 계산법과 이중 평면 시스템("hurdy-gurdy")을 제시하며, 이를 통해 지속적으로 진화하는 인간 검증 기반의 신뢰 그래프가 점점 더 높은 확신과 함께 결정 가능한 프로그램 질문들로 수렴하도록 보장한다.

원저자: Christoph Kirsch

게시일 2026-07-20

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Christoph Kirsch

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

탐정의 딜레마: 메신저를 믿을 수 없을 때

당신이 자동차 엔진이나 비디오 게임 캐릭터의 행동처럼 복잡한 기계에 대한 미스터리를 풀려고 한다고 상상해 보십시오. 당신은 다음과 같은 질문을 던집니다: "내가 시속 50마일로 가속 페달을 밟으면 이 차가 충돌할까?" 이 질문에 답하기 위해, 당신은 단순히 차를 바라보는 것만으로는 부족합니다. 차의 무질서한 실제 역학 관계를 수학 방정식과 같이 똑똑한 컴퓨터 솔버(solver)가 이해할 수 있는 언어로 번역해야 합니다. 하지만 여기에 함정이 있습니다. 차를 수학으로 번역하는 사람이 실수를 할 수도 있다는 점입니다. 아마도 그들은 기어 하나를 빠뜨렸거나, 브레이크가 작동하는 방식을 오해했을 수도 있습니다. 만약 번역가가 틀렸다면, 수학 솔버는 '틀린 질문'에 대해 '완벽한 정답'을 내놓게 됩니다.

컴퓨터 과학의 세계에서 이것은 '번역'의 문제입니다. 우리는 프로그램의 안전성을 확인하기 위해 한 언어(예: C 또는 Python)에서 다른 언어(예: 솔버를 위한 논리 퍼즐)로 프로그램을 옮겨야 할 때가 많습니다. 전통적으로 과학자들은 번est가 완벽하다는 것을 단 한 번의 증명을 통해 입증하려고 노력했습니다. 마치 누구나 운전하기 전에 다리가 안전한지 인증하는 것과 같습니다. 하지만 이는 매우 어려운 일이며, 특히 번역기가 복렴하거나 심지어 인공지능에 의해 작성된 경우라면 더욱 그렇습니다. 이 논문은 다른 질문을 던집니다. 만약 우리가 번역기가 완벽하다는 것을 증명하는 것을 포기하는 대신, 번역기가 작동하는 동안 그 실수를 잡아내는 시스템을 구축한다면 어떨까요? 이것은 단 한 명의 가이드가 숲을 안내하도록 믿는 것과, 서로의 지도를 확인하는 팀의 가이드들이 있는 것의 차이입니다. 그리고 만약 그들이 의견이 다를 경우, 당신은 멈춰 서서 누가 틀렸는지 파악해야 한다는 규칙이 있는 상태 말입니다.

"허디 거디(Hurdy-Gurdy)" 머신: 신뢰할 수 있는 답변을 만드는 공장

이 논문은 **허디 거디(hurdy-gurdy)**라고 불리는 시스템을 소개합니다 (음악을 연주하기 위해 크랭크를 돌리는 악기의 이름을 땄지만, 여기서는 답변을 만들어낸다는 의미입니다). Christoph Kirsch가 이끄는 저자들은 컴퓨터 프로그램을 다루는 새로운 방식을 제안합니다. 즉, 모든 단계가 확인되고 모든 답변에 영수증(증거)이 첨부되는 '전화기 놀이(telephone)' 게임처럼 취급하는 것입니다.

핵심 아이디어는 단순하지만 강력합니다: 번역가를 믿지 말고, 프로세스를 믿으십시오.

C 언어로 작성된 프로그램에 대해 질문이 있다고 가정해 봅시다. 시스템은 이 프로그램을 단 하나의 경로로 보내는 대신, 두 개의 서로 다른 경로로 보냅니다.

번역 (The Translation): 프로그램은 더 단순한 논리 언어로 번역됩니다 (마치 소설을 수학 방정식으로 바꾸는 것과 같습니다).
이중 확인 (The Double-Check): 시스템은 원래의 프로그램과 번역된 버전을 나란히 실행합니다. 그리고 두 프로그램이 동일하게 작동하는지 확인합니다. 만약 그렇다면 잘 된 일입니다! 만약 그렇지 않다면, 시스템은 마치 심판이 선수의 반칙 순간에 휘슬을 부는 것처럼, 두 프로그램이 어느 지점에서 갈라졌는지를 정확히 지목합니다.
"위트니스(Witness)" 트릭: 만약 솔버가 "네, 충돌이 가능합니다"라고 말한다면, 시스템은 단순히 솔버의 말을 그대로 믿지 않습니다. 시스템은 그 "증거"(충돌을 일으키는 구체적인 조건들)를 가지고 번역 과정을 역순으로 거슬러 올라갑니다. 그 조건들을 원래의 프로그램에 다시 입력합니다. 만약 원래의 프로그램이 실제로 충돌한다면, 그 답변은 100% 진짜입니다. 시스템이 범죄 현장을 "재현(replay)"해낸 것입니다.

두 개의 평면: 구축과 사용

이 시스템은 공장 바닥과 전시장처럼 두 개의 뚜렷한 모드를 가집니다.

사용 평면 (The Use Plane - 전시장): 이곳에서 답변이 만들어집니다. 여기서 AI(또는 인간)는 질문을 던집니다. 시스템은 단순히 추측하지 않습니다. 경로를 선택하고, 번역을 확인하며, 만약 답변이 "네, 가능합니다"라면 재현(replay)을 실행하여 증명합니다. 만약 답변이 "아니요, 불가능합니다"라면, 시스템은 여러 번역기, 여러 솔버, 그리고 수학적으로 검증된 인증서라는 일련의 확인 체계에 의존하여 확신을 얻습니다.
진화 평면 (The Evolution Plane - 공장): 이곳은 시스템이 성장하는 곳입니다. 만약 시스템이 질문에 답할 수 없다면, 그냥 포기하지 않습니다. 시스템은 왜 실패했는지(예: "특정 유형의 루프에 대한 번역기가 없습니다")를 기록합니다. 그런 다음 AI를 사용하여 그 빈틈을 채울 새로운 번역기를 만듭니다. 새로 만들어지면, 이 번역기는 기존의 것들과 대조 테스트를 거칩니다. 통과하면 레지스트리에 추가됩니다. 실패하면 수정됩니다. 이 루프는 무한히 반복되며 시스템을 더 똑똑하고 신뢰할 수 있게 만들지만, 결정적으로 성장 과정 자체는 질문에 답하지 않습니다. 그것은 오직 답변을 위한 도구를 구축할 뿐입니다.

"신뢰할 수 없는 저자들"이라는 반전

이 논문의 가장 놀라운 부분은 번역기 자체가 신뢰할 수 없는 AI 에이전트에 의해 구축되었다는 점입니다. 저자들은 직접 코드를 짠 것이 아니라, 한 페이지 분량의 설명서를 바탕으로 AI 모델에게 번역기를 작성하도록 요청했습니다. 보통 이런 상황은 재앙이 될 것입니다. 하지만 시스템이 모든 단계를 확인하기 때문에, AI의 실수는 즉시 포착되었습니다.

예를 들어, 한 실험에서 AI 번역기가 특정 명령어를 놓쳐서 원래 프로그램과 다르게 동작하게 만들었습니다. 시스템의 "스퀘어 체크(square check, 양방향 비교)"가 오류를 즉시 발견했고, 정확히 어떤 라인과 어떤 변수가 잘못되었는지 짚어냈습니다. 시스템은 그 후 번역기를 수정했습니다. 이 논문은 AI 저자가 틀릴 수 있음에도 불구하고, 시스템의 *구조(architecture)*가 최종 답변의 신뢰성을 보장한다는 것을 보여줍니다.

시스템이 찾아낸 것 (그리고 찾지 못한 것)

저자들은 2026년 7월의 작업 스냅샷을 바탕으로 이 시스템을 실행했습니다. 측정 결과는 다음과 같습니다.

커버리지 (Coverage): 그들은 13가지의 서로 다른 언어(C, Python, 심지어 화학 반응 네트워크 포함)로부터 프로그램을 논리 솔버로 성공적으로 번역했습니다. RISC-V 프로세서 언어의 경우, 특정 명령어 유형 96개 중 96개 모두를 커버했습니다. 즉, 시스템이 정보를 놓치지 않고 모든 명령어를 처리할 수 있음을 의미합니다.
일치성 (Agreement): 동일한 질문을 두 가지 다른 번역 경로(하나는 매뉴얼 기반, 하나는 형식 모델 기반)로 보냈을 때, 테스트 케이스에서 답변이 100% 일치했습니다.
결함 포착 (Defects Caught): 시스템은 자체 번역기와 도구에서 24개의 구체적인 결함을 찾아냈습니다. 어떤 것은 단순한 오타였고, 어떤 것은 AI가 컴퓨터 명령의 작동 방식을 오해한 논리적 오류였습니다. 결정적으로, 시스템은 인간이 코드를 들여다보지 않고도 이러한 오류를 찾아냈습니다.
"사각지대" (The Blind Spot): 시스템은 한계점도 발견했습니다. 만약 두 개의 서로 다른 번역기가 (둘 다 동일한 규칙을 오해했기 때문에) 똑같은 실수를 저지른다면, 시스템은 이를 잡아낼 수 없습니다. 이를 "공통 모드 고장(common-mode failure)"이라고 합니다. 논문은 이것이 리스크임을 인정하지만, 시스템은 다양한 출처의 번역을 사용하여 이 위험을 최소화하도록 설계되었습니다.
LLM 플레이어: 그들은 AI가 시스템을 사용하여 질문에 답할 수 있는지 테스트했습니다. 한 실험에서 도구가 없는 AI는 8개 중 7개의 질문을 맞혔지만 어려운 문제에서는 추측했습니다. 반면 시스템을 사용하는 AI는 8개 중 8개를 모두 맞혔으며, 모든 답변에는 기계로 검증된 증거가 첨부되었습니다.

결론

이 논문은 모든 컴퓨터 안전 문제를 해결했다고 주장하는 것이 아닙니다. AI 번역기가 이제 완벽해졌다고 말하는 것도 아닙니다. 대신, 신뢰할 수 없는 부품들로 신뢰할 수 있는 시스템을 구축할 수 있음을 증명합니다.

모든 번역을 잠재적인 실수로 간주하고, 개선 사항이 반드시 적용되도록 하는 "래칫(ratchet, 역행 방지 장치)"을 구축함으로써, 시스템은 신뢰의 사다리를 만듭니다. 만약 질문이 "이런 일이 일어날 수 있는가?"라면, 시스템은 사건을 재현하여 증명할 수 있습니다. 만약 답변이 "아니요, 이것은 불가능합니다"라면, 시스템은 독립적인 확인 절차와 수학적으로 검증된 인증서 체인을 사용하여 확신을 얻습니다.

저자들은 이 접근 방식—경로의 그래프를 사용하고, 모든 단계를 확인하며, 증거를 재현하는 방식—이 현대 소프트웨어의 복잡성을 다루는 데 있어 유효한 방법임을 결과적으로 보여줍니다. 이는 도구를 만드는 사람들(또는 AI)이 결함이 있을지라도 말입니다. 이것은 "저자를 신뢰하는 것"에서 "구조를 신뢰하는 것"으로의 패러다임 전환입니다.

기술 요약: 신뢰할 수 없는 저자, 신뢰할 수 있는 답변

문제 정의

본 논문은 프로그램을 분석(예: 도달 가능성, 어설션 유효성 검사)하는 데 사용되는 도구들이 신뢰할 수 없는 상황에서, 프로그램에 관한 질문에 답하는 근본적인 과제를 다룹다. 전통적인 접근 방식은 단일 번역기의 정당성을 한 번 증명하거나(예: Compile) 단일 번역기의 모든 실행을 검증하는 것에 의존한다. 그러나 이러한 방법들은 단일한 "번역의 엣지(edge)"를 가정한다. 본 논문은 다양한 소스 언어, 다양한 추론 대상, 그리고 잠재적으로 신뢰할 수 없는 저자(LLM 포함)가 포함된 복잡한 생태계에서, 번역 과정은 여러 언어와 경로로 이루어진 그래프를 형성한다고 주장한다. 이 그래프 내에서는 모든 번역이 실패 지점이 될 수 있다. 핵심 문제는 어떻게 하면 모든 구성 요소에 대한 보편적 증명을 요구하지 않으면서도, 이처럼 이질적이고 독립적으로 구축되었으며 잠재적으로 신뢰할 수 없는 번ay들을 하나의 시스템으로 결합하여 신뢰할 수 있는 답변을 제공할 것인가 하는 점이다.

방법론: 충실도 등급이 매겨진 번역의 계산법 (The Calculus of Fidelity-Graded Translations)

저자들은 공식적인 계산법과 hurdy-gurdy라고 불리는 플랫폼 구현을 제안한다. 이 방법론은 공유 레지스트리에서 만나는 두 개의 뚜렷한 "평면(plane)"으로 구성된다.

1. 사용 평면 (질문에 답하기)

이 평면은 번역을 노드가 언어이고 엣지가 번역 쌍인 그래프로 취급한다.

쌍(Pair)과 사각형(Square): 기본 단위는 번역기 $T$ $T$ , 타겟-투-소스 역전송 $\Lambda$ $Λ$ , 그리고 공유 인터프리터로 구성된 쌍 $(A, B)$ $(A, B)$ 이다. 쌍은 **방향성 교환 사각형(directional commuting square)**을 통해 검증된다:
- 정확성(Exactness): 소스의 동작은 역전송된 타겟의 동작과 동일하다 (유지된 관측 가능성에 대한 이분 모형).
- 과잉 근사(Over-approximation): 소스의 동작이 타겟의 동작에 의해 시뮬레이션된다 (가짜 동작은 허용하되 소스의 동작은 보존함).
- 결정 가능성(Decidability): 특정 프로그램에 대해, 사각형은 양측을 모두 실행하고 투영된 트레이스를 비교함으로써 확인된다. 만약 두 측이 일치하지 않으면, 실패는 특정 단계와 관측 가능성으로 국소화된다.
합성과 계약(Composition and Contracts): 경로는 그래프를 통과하는 경로들의 합성이다. 경로의 계약은 네 가지 축에 의해 정의되는 각 홉(hop)의 **성분별 하한(componentwise meet)**이다:
- 보증 클래스(Assurance Class): none에서 replay, per-run, universal까지의 계층 구조.
- 방향(Direction): 정확(Exact) 또는 과잉 근사(Over-approximation).
- 유지된 관측 가능성(Kept Observables): 각 홉에 의해 보존되는 관측 가능성의 교집합 (손실은 누적됨).
- 비용(Cost): 실행 시간으로 측정됨.
신뢰 메커니즘:
- 실행당 재확립(Per-Run Re-establishment): "신뢰할 수 있는" 홉이라 할지라도, 스퀘어 오라클이 특정 실행에 대해 통과한다면 동적으로 검증될 수 있다.
- 분기 상호 확증(Branch Corroboration): 두 개의 독립적으로 유도된 경로(다양한 접두사)가 동일한 판정에 동의하면, 그 증거는 개별 경로의 등급보다 더 강력하다.
- 존재적/보편적 비대칭성(Existential/Universal Asymmetry):
  - 존재적 답변 (도달 가능함): 자기 인증적이다. 솔버의 증거(witness)는 역전송되어 소스 인터프리터에서 **재생(replay)**된다. 만약 재생이 해당 동작을 보인다면, 번역기 오류와 상관없이 답변은 참이다 (신뢰 기반: 소스 인터프리터의 적절성).
  - 보편적 답변 (도달 불가능함): 자기 인증적이지 않다. 이는 등급의 합성, 분기 합의, 그리고 공식 인증서(예: 검증된 체커에 의해 체크되는 DRAT 증명)에 의존한다.

2. 진화 평면 (그래프 확장하기)

이 평면은 번역 그래프의 성장을 관리한다.

신뢰할 수 없는 생성: 쌍은 브리프(brief)를 바탕으로 독립적인 LLM 에이전트에 의해 구현된다.
래칫(The Ratchet): 시스템은 가산적 성장 모델을 강제한다. 새로운 기여는 이전의 판정을 무효화하지 않으면서 커버리지를 확장해야 한다.
수요 및 등록: 답변 불가능한 질문은 "수요(demand)"로 기록된다. 새로운 쌍에 대한 권고 사항은 증거를 바탕으로 생성된다. 인간의 등록이 최종 관문이며, 시스템은 자율적으로 질문에 답하는 것이 아니라 질문을 수행할 수 있는 능력을 키우는 것이다.

주요 기여

방향성 및 충실도 등급이 매겨진 쌍의 계산법: 정확성이 과잉 근사의 특수한 경우이며, 합성이 보증, 방향, 손실, 비용에 걸친 "최약체 연결(weakest link)"의 meet으로 정의되는 공식 프레임워크.
계약 대수(Contract Algebra): 이질적인 증거를 합성하는 메커니즘. 본 논문은 "per-run" 체크와 "universal" 보증이 어떻게 결합하는지, 그리고 손실(버려진 관측 가능성)이 경로를 따라 어떻게 누적되는지를 정식화한다.
존재적/보편적 비대칭성: 증거(witness)를 전달하는 답변(소스 재생을 통한 자기 인증)과 그렇지 않은 답변(등급화된 신뢰 및 인증서 필요)을 구분하는 아키텍처 원칙.
두 평면 아키텍처: "사용(answering)" 평면과 "진화(building)" 평면의 분리를 통해, 신뢰할 수 없는 에이전트들이 시스템을 구축하게 하면서도 교차 검증, 다양성, 래칫을 통해 신뢰를 보장한다.
기계화(Mechanization): 패스팅 정리(pasting theorem), 국소화(localization), 엔드 투 엔드 비대칭성 정리를 포함한 구성적 핵심 요소들이 Lean 4(약 1,250라인)로 기계화되었으며, 깨끗한 공리 감사(axiom audit)를 거쳤다.

결과 및 평가

본 논문은 인간의 의미론적 코드 리뷰 없이 전적으로 LLM 에이전트에 의해 구축된 hurdy-gurdy 플랫폼의 "2026년 7월 스냅샷"을 평가한다.

커버리지 및 정확성: 시스템은 13개의 언어와 15개의 등록된 쌍을 커버한다. RISC-V, AArch64, eBPF, Wasm, EVM, Python 등을 위한 경로를 성공적으로 합성했다.
- 분기 합의: RISC-V(수동 유도 vs Sail 유도) 및 AArch64를 위한 이중 경로는 테스트된 12개의 모든 도달 가능성 질문에 대해 일치했으며, 보편적(도달 불가능) 판정에서도 그러했다.
- 컴플라이언스 벤치마크: RISC-V 테스트 스위트에서 유도된 78개의 질문 벤치마크는 경로 간 100% 일치 및 실제 정답 대비 100% 정확도를 보이며 해결되었다.
결함 탐지: 아키텍처는 다음을 포함하여 LLM이 생성한 코드에서 24개의 결함을 잡아냈다:
- 인터프리터와 번로가 모두 동일하게 잘못 인식한 명령(예: MUL을 ADD로 오인)의 침묵하는 디코딩 오류(외부 다양성에 의해서만 포착된 "맹점").
- 한 솔버는 허용하지만 다른 솔버는 거부하는 잘못된 형식의 중간 표현(IR).
- 플랫폼 자체의 계측 결함(예: 거짓 증명을 수락하는 체커 어댑터).
탈출률 실험: 시드된 RISC-V 번역기의 의미론적 변이(mutation)를 시스템의 게이트로 테스트했다.
- "스퀘어 스위트(conjoined probes)"는 55개 중 51개의 변이를 잡아냈다.
- 나머지 4개는 유도된 벤치마크에 의해 잡혔다.
- 최종 라운드에서 **제로 탈출(zero escapes)**이 관찰되었으나, 저자들은 이것이 변이 패밀리를 측정하는 것이지 모든 가능한 오류에 대한 제로 탈출률을 의미하는 것은 아니라고 명시했다.
- 공통 모드 실패(두 스퀘어의 양쪽 다 틀린 경우)는 다양한 분기(Sail 경로)나 외부 차이 분석에 의해서만 포착되었으며, 이는 독립적인 의미론적 앵커의 필요성을 입증한다.
LLM 플레이어 실험: LLM 에이전트에게 플랫폼을 사용하여 질문에 답하도록 과제를 부여했다.
- 두 번째 반복(v2)에서, LLM 플레이어는 어려운 BTOR2 도달 가능성 질문 8개 중 8개를 모두 맞힌 반면, 도움을 받지 못한 LLM은 8개 중 7개를 맞혔다.
- 결정적으로, LLM 플레이어의 답변에는 기계적으로 검증된 증거 산출물(예: 재생된 witness, LRAT 인증서)이 동반되었으나, 도움을 받지 못한 LLM은 "말뿐인 확신"과 신뢰 점수에 의존했다.
성능: 모든 홉을 체크하고 witness를 재생하는 규율의 오버헤드는 솔버 호출에 비해 매우 작다. 번역에는 밀리초가 걸리며, 시간이 주로 솔버에 의해 지배된다.

의의 및 주장

본 논문은 번역에 대한 신뢰는 저자를 신뢰하는 것이 아니라 아키텍처에 의해 제조될 수 있음을 입증한다고 주장한다.

분산 시스템 관점: 번역기를 실패할 수 있는 컴포넌트로 취급하며, 보편적 증명을 통해 방지하기보다는 선언된 투영, 결정 가능한 체크, 독립적인 경로를 통해 실패를 제어한다.
신뢰의 "래칫": 시스템은 진화하도록 설계되었다. 커버리지와 보증은 단조롭게 증가하며, 그래프가 확장되어도 이전의 판정은 보존된다.
제한된 범위: 저자들은 이 시스템이 "데이터화된 능력 스냅샷"임을 명시한다. 이는 결정 불가능성을 해결하거나 모든 형식 검증을 대체한다고 주장하지 않는다. "증명된(proved)" 계층은 특정하고 경계가 정해진 질문을 위해서만 존재한다. 시스템은 인터프리터 적절성과 구조적 다양성 가정의 경험적 배출에 의어한다.
비대칭성: 논문은 존재적 답변의 경우 신뢰는 "거의 무료"(재생을 통해)인 반면, 보편적 답변의 경우 시스템이 등급화된 계층, 분기, 인증서를 통해 의식적으로 보증을 "구매"해야 한다고 결론짓는다.

이 연구는 이러한 원칙 위에 구축된 시스템이, 아키텍처가 엄격한 교차 검증과 합성 계약을 강제하는 한, 신뢰할 수 없는 저자(인간 또는 AI)가 검증된 추론 인프라를 구축하는 데 기여할 수 있게 한다고 제안한다.