AI wrote my compiler. A mathematical proof checks its work on every build.

개요

AI가 작성한 컴파일러의 정확성을 검증하기 위해 수학적 증명을 활용하며, 이는 AI 에이전트가 코드를 수정하고 빌드하는 과정에서 발생하는 오류를 효과적으로 관리하고 코드 품질을 유지하는 데 중점을 둡니다.

주요 내용

* 수정 생존율(Modification Survival Rate, MSR) 중심 설계: AI가 코드를 작성하고 컴파일 실패 시 오류 메시지를 통해 수정하도록 3회까지 재시도하게 하여, 최초 완벽성보다 수정 루프의 수렴성을 측정합니다.
* 구문 단순화: MSR을 기준으로, AI 모델에게 명확한 영향을 주지 않는 불필요한 구문(예: fn 키워드)은 제거하여 코드 작성의 복잡성을 줄입니다.
* 실패 원인 분석 및 해결: AI의 실패는 주로 표준 라이브러리 추측(hallucination)과 타 언어 습관 모방에서 발생하며, 이는 치트 시트(cheatsheet) 업데이트 및 구체적인 진단 메시지를 통해 해결합니다.
* 컴파일러 오류 메시지의 API화: 인간이 아닌 AI 에이전트가 이해하도록 오류 메시지를 설계하며, almide explain 및 almide fix와 같은 도구를 통해 명확한 진단과 구체적인 수정 제안을 제공합니다.
* 결정론적 수정 도구: almide fix는 누락된 임포트, 잘못된 함수 호출 등을 자동으로 수정하여 AI 에이전트의 추가적인 시행착오를 줄입니다.
* AI 에이전트의 코드베이스 관리: 코드를 여러 Rust crate로 분할하여 에이전트의 작업 범위를 제한하고, codopsy와 같은 정적 분석 도구를 활용하여 코드 복잡성을 관리하고 개선합니다.
* 수학적 증명을 통한 컴파일러 신뢰 확보: AI가 작성한 컴파일러의 신뢰성을 위해, 모든 빌드마다 생성된 코드와 함께 메모리 연산을 증명하는 인증서(certificate)를 발행하고, 검증된(proven) 체커가 이를 확인합니다.
* Perceus 메모리 관리: GC(Garbage Collector) 없이 컴파일 타임에 참조 카운팅을 통해 메모리를 관리하며, AI 에이전트가 작성하는 코드에 대한 증명 부담을 줄여줍니다.
* Lean 및 Rocq 활용: Lean은 Perceus의 메모리 관리 규칙 자체의 건전성을 수학적으로 증명하고, Rocq는 각 빌드의 인증서가 규칙을 따르는지 검증하는 데 사용됩니다.

시사점

AI 에이전트가 코드 작성 및 유지보수에 활용되는 미래에서, 컴파일러의 설계 및 검증 방식은 AI의 특성에 맞춰 변화해야 하며, 수학적 증명과 같은 강력한 도구를 통해 코드의 정확성과 신뢰성을 확보하는 것이 중요합니다.