"AI가 맞는 코드까지 증명한다"는 말의 핵심

AI 코딩 에이전트의 다음 경쟁력은 더 많은 코드를 더 빨리 쓰는 능력만이 아닙니다. 핵심 질문은 이제 “그 코드가 정말 맞는가”로 이동하고 있습니다.

특히 계산물리학과 응용수학에서는 작은 구현 오류가 결과 전체를 바꿀 수 있습니다. 방정식, 경계조건, 수치 기법이 코드로 옮겨지는 과정에서 의미가 조금만 달라져도 잘못된 과학적 결론으로 이어질 수 있기 때문입니다. 그래서 이 분야에서 중요한 것은 단순히 실행되는 코드가 아니라, 명세와 정합성을 함께 검증할 수 있는 코드입니다.

“증명 가능한 코드”는 테스트를 통과한 코드와 다르다

증명 가능한 코드는 테스트를 많이 통과한 코드와 다릅니다. 테스트는 정해진 입력 사례에서 기대한 결과가 나오는지 확인합니다. 반면 형식 증명은 코드나 수학적 명제가 특정 명세를 만족한다는 것을 기계가 검사할 수 있는 형태로 다룹니다.

이 차이는 AI 코딩 에이전트를 평가할 때 중요합니다. AI가 그럴듯한 구현을 생성하는 것만으로는 충분하지 않습니다. 신뢰의 중심이 AI 모델의 답변이 아니라, Lean, Isabelle, Rocq 같은 형식 검증 도구와 그 도구가 확인한 증명으로 옮겨가야 합니다.

계산물리학과 응용수학용으로 논의되는 새 유형의 에이전트도 이 방향을 향합니다. 자연어 또는 수학적 설명에서 방정식과 수치 기법에 맞는 타입 올바른 DSL 코드를 생성하고, 정합성 속성을 Lean, Isabelle, Rocq에서 형식화하며, 최종적으로 C 코드로 컴파일하는 흐름입니다. 즉 “코드 생성”과 “검증 가능한 근거 생성”을 하나의 파이프라인으로 묶는 접근입니다.

MathCode가 보여주는 현재의 실용적 형태

이 흐름을 이해하는 데 도움이 되는 예가 MathCode입니다. MathCode는 자연어 수학 문제를 Lean 4 정리로 변환하고 형식 증명을 시도하는 터미널 기반 AI 코딩 보조도구입니다.¹ 수학 형식화와 증명 파이프라인은 AUTOLEAN 프로젝트를 기반으로 합니다.¹

여기서 중요한 점은 AI가 답을 한 번 생성하고 끝나는 구조가 아니라는 것입니다. 생성된 정리는 Lean으로 확인되고, 오류가 있으면 다시 고치는 반복 루프에 들어갑니다. 자동 정리 증명 연구에서도 단발성 생성보다 컴파일 오류를 보고 수정한 뒤 다시 시도하는 방식이 더 효과적이라는 결과가 보고됐습니다.² 기억 장치와 라이브러리 검색도 성능 향상에 도움이 됩니다.²

이 반복 루프가 실무에 들어오려면 속도도 중요합니다. MathCode의 지속형 Lean REPL은 Mathlib를 처음 불러오는 데 약 90초가 걸리지만, 이후 컴파일 확인을 약 0.4초로 줄입니다. 지속형 REPL을 쓰지 않으면 확인에 약 30초가 걸립니다.¹ 증명 가능한 코딩 에이전트에서 성능은 단순 생성 속도가 아니라, “검증하고 수정하는 주기”를 얼마나 짧게 만들 수 있는지에 달려 있습니다.

도입할 때 봐야 할 세 가지 기준

이런 도구를 평가할 때는 “AI가 코드를 잘 쓰는가”보다 더 구체적인 기준이 필요합니다.

첫째, 명세가 먼저 있어야 합니다.
증명 가능한 코드는 “빠른 코드”가 아니라 “무엇을 만족해야 하는지 명확한 코드”입니다. 방정식, 수치 기법, 경계조건, 보존 성질처럼 검증할 대상을 먼저 정의해야 AI 에이전트도 의미 있는 검증 흐름을 만들 수 있습니다.

둘째, 검증 결과가 축적되어야 합니다.
MathCode는 기본적으로 출력을 LeanFormalizations/ 디렉터리에 저장합니다.¹ 또한 성공적으로 증명된 정리를 TheoremLib/Stored.lean에 자동 추가해 이후 증명에서 다시 사용할 수 있습니다.¹ 대화 중 나온 가정도 Lean 형식화와 함께 저장하고 컴파일로 검사할 수 있습니다.¹ 이는 에이전트가 매번 처음부터 추론하는 대신, 검증된 지식을 라이브러리로 쌓아가는 방향을 보여줍니다.

셋째, 실행 환경과 도구체인을 확인해야 합니다.
MathCode는 macOS arm64와 Linux x86_64 환경을 요구합니다.¹ Lean이나 Lake가 없을 경우 설치 스크립트가 로컬 Lean 도구체인을 부트스트랩합니다.¹ 형식 검증 기반 도구는 모델만 붙인다고 바로 작동하지 않습니다. 증명기, 라이브러리, 컴파일러, 저장 구조까지 포함한 개발 환경으로 봐야 합니다.

개발자의 역할은 구현자에서 검증 흐름 설계자로 이동한다

이 변화의 본질은 “AI가 코드를 대신 쓴다”가 아닙니다. AI가 코드와 함께 검증 가능한 근거를 만들기 시작했다는 점입니다.

계산물리학과 응용수학에서 이 흐름은 특히 중요합니다. 앞으로 개발자는 구현 세부를 직접 작성하는 사람에 머무르지 않고, 어떤 명세를 검증할지 정하고, 어떤 정리를 재사용할지 고르며, 검증 루프가 실제 개발 속도에 맞게 돌아가도록 설계하는 역할을 더 많이 맡게 될 가능성이 큽니다.

결국 provably correct code를 위한 AI 에이전트의 가치는 “그럴듯한 코드 생성”이 아니라 “명세, 구현, 증명, 컴파일을 연결하는 신뢰 가능한 작업 흐름”에 있습니다.

¹GitHub - math-ai-org/mathcode: MathCode: A Frontier Mathematical Coding Agent

²A Minimal Agent for Automated Theorem Proving