"알고리즘 안 짭니다"… 조건만 적으면 AI가 코드 짜고 수학적 증명까지 끝내는 러스트 도구 등장

요약 개발자가 원하는 함수의 동작 명세와 제약 조건만 Rust 문법과 유사한 매크로(`djinn!`) 안에 적어두면, LLM(대형 언어 모델)이 알아서 실제 실행 가능한 코드를 작성하고 수학적 증명까지 완료해 주는 도구 'rust-djinn'이 공개되어 화제를 모으고 있습니다. 일반적으로 정렬(sort) 함수를 만들 때 정렬 알고리즘을 직접 짜는 대신, "결과 배열의 길이는 원본과 같다", "포함된 원소의 개수가 같다", "앞 원소는 뒤 원소보다 작거나 같다"는 식의 참/거짓 제약 조건만 작성하면 지니(Djinn)가 이를 기반으로 실제 동작 코드를 구현합니다. 이때 매크로 내부의 반복문 등은 명령형 루프가 아니라 모든 원소에 대해 성립해야 하는 '조건(전칭 한정)' 역할을 합니다. 이 도구는 Rust 코드를 증명 보조 도구인 Lean 등으로 변환해 정리(theorem)를 증명하는 'Aeneas'를 기반으로 설계되었습니다. 사용자가 복잡한 정형 검증 언어나 Lean을 직접 배울 필요 없이, `cargo djinn implement` 명령어 하나만 실행하면 백그라운드에서 LLM 에이전트가 호출되어 요구사항을 충족하는 코드를 짜고 Lean/Aeneas를 통해 해당 코드가 명세를 100% 만족함을 증명해 냅니다. 검증이 통과된 코드만 기존 Rust 프로젝트와 결합되어 안전하게 컴파일됩니다. 또한 `cargo djinn optimize` 명령을 실행하면 에이전트들이 코드를 최적화하는 루프를 돌며, 벤치마크상 더 빠르면서도 여전히 수학적 검증을 통과하는 개선된 코드만을 남기는 '언덕 오르기(hill climbing)' 방식의 성능 개선까지 지원합니다. 인간 개발자는 LLM이 짠 복잡한 구현 코드를 일일이 코드 리뷰할 필요 없이 명세 작성에만 집중할 수 있는 시대를 보여주는 흥미로운 시도로 평가받고 있습니다.