각 과제에서 코딩 에이전트는 40분 동안 오픈소스 Rust 애플리케이션의 보안 관련 코드가 정해진 성질을 만족한다는 것을 증명해야 한다. i5h 벤치마크는 이 과정을 보여 주며, 아직 측정이 끝나지 않았다.
이 벤치마크는 기존 애플리케이션의 접근 제어, 입력 검증, 파싱 로직을 i5h로 옮긴 뒤 에이전트가 Lean 4 증명을 만들 수 있는지 살핀다. Rust와 Lean 4를 함께 보는 개발자라면 과제별 코드와 증명 결과를 확인할 수 있다.
i5h는 어떤 프레임워크인가?
i5h는 애플리케이션 로직의 정확성을 Lean 4로 증명할 수 있는 Rust 웹 프레임워크다. 애플리케이션 로직과 상태 변경은 Rust의 일부 하위집합으로 작성하며, 웹 요청 처리는 axum으로 제공하고 PostgreSQL 트랜잭션을 사용한다. Aeneas가 해당 Rust 코드를 Lean 4 정의로 변환하므로, Lean 코드는 실행되는 코드이지 별도로 만든 모형이 아니다.
과제는 어떻게 만들고 채점하나?
과제의 출발점은 특정 커밋으로 고정한 오픈소스 애플리케이션의 접근 제어, 입력 검증 또는 파싱 코드다. 이를 함수 단위로 i5h에 옮긴다. 문자열은 바이트 슬라이스(byte slice)로, 반복자(iterator)는 반복문으로 바꾸며, 변경 사항은 포팅 과정의 차이 기록 파일에 남긴다.
Aeneas가 포팅한 코드를 Lean 4로 추출하고, 사람이 작성한 명세가 원하는 성질을 정리해 정리(theorem)로 만든다. 에이전트는 포팅된 Rust 코드와 추출된 Lean 코드, 명세를 받는다. 네트워크는 사용할 수 없고 i5h Lean 라이브러리와 관련 기술 안내는 제공된다. 작업 시간은 40분이며, 에이전트가 일찍 멈추면 한 번 재개한다.
증명은 빌드되어야 하고, 정리의 명제는 바뀌지 않아야 한다. 허용되는 공리는 propext, Classical.choice, Quot.sound뿐이다. 에이전트에게는 제공하지 않는 벤치마크 자체의 기준 증명도 있다. 각 과제 페이지에서는 모델이 작성해 채점에 통과한 증명을 볼 수 있다.
별도로 차등 테스트(differential test)를 한다. 원본 코드와 i5h 포팅 코드는 같은 무작위 입력을 받아 같은 결과를 내야 한다. 의도적으로 변경한 포팅 코드는 이 테스트에서 실패해야 한다.
결과를 볼 때 무엇을 확인해야 하나?
애플리케이션별 화면에는 공백 줄과 주석, 속성을 제외한 원본 및 포팅 코드 줄 수와, 적어도 한 모델이 증명한 성질 수가 표시된다. 과제 목록에서는 모델별 풀이 여부를 확인할 수 있다.
모델 비교 화면은 시도한 과제 중 해결한 비율을 보여 주며, 모델마다 실행한 과제가 같지는 않다. 과제 수는 막대 옆에 표시한다. 풀이 시간과 비용은 해당 모델이 해결한 과제만 계산한다. Rust 코드 줄당 비용은 그 성질이 다루는 연산의 원본 코드 줄 수를 기준으로, 해결한 과제에 사용한 정가 기준 지출을 나눈 값이다.
현재 결과는 중간 집계다. 모든 모델이 모든 과제를 수행한 것은 아니며, 수치는 바뀔 수 있다. 원문은 현재 모델별 실제 점수와 비용 수치를 제시하지 않는다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요