sahibzada-allahyar/Formal-Verification-RSI

해결하는 문제

AI가 작성한 증명은 유효해 보이지만 실제로는 가짜인 경우가 많습니다. Lean과 같은 도구는 sorry를 경고와 함께 수락하고, Dafny는 assume {:axiom} false를 오류 0으로 처리하며, 인스턴스 섀도잉을 통해 정리의 텍스트를 바이트 단위로 동일하게 유지하면서 의미를 바꿀 수 있습니다. 기존의 벤치마크 검사는 이러한 부정행위를 놓칩니다. Millennium Harness는 파일이 컴파일되는지 확인하는 것뿐만 아니라, 동결된 사양이 원래 의미를 유지하고 에스케이프 해치 없이 증명되었는지 검증함으로써 이러한 격차를 해소합니다. 레드팀이 테스트한 96개의 부정행위를 모두 거부하고 25개의 정직한 솔루션을 모두 수락했습니다.

작동 방식

Lean – 이 하네스는 문장과 테스트를 동결한 다음, 정교화 후 컴파일된 환경을 검사합니다. 문장의 동일성을 확인하고, 공리를 화이트리스트와 비교하며, 동결된 선언에 도달하는 인스턴스/표기법을 감시하고, 컴파일된 코드 교체(implemented_by/extern)를 감지하며, 정교화 시 코드 실행을 방지하고, 커널 검증을 다시 실행합니다.

Dafny – 동결된 사양이 자체적으로 변경 없이 해결될 것을 요구하며, assume, {:axiom}, ensures가 있는 본문 없는 보조 정리, 허용되지 않는 속성 및 캡처된 사양 헬퍼를 거부한 다음 dafny audit 및 컴파일 검사를 실행합니다.

에이전트 루프 – AI 에이전트(OpenCode 또는 Claude Code)와 함께 사용할 경우, 에이전트가 중지된 후 게이트가 실행됩니다. 판정이 PROVED가 아니면 실패 피드백이 다음 프롬프트가 되므로, 에이전트는 증명이 진정으로 인증될 때까지 계속 시도해야 합니다.

재귀적 자기 개선 – Millennium RSI는 하네스 자체를 데이터(전략 및 보조 정리 라이브러리)로 취급합니다. 제안된 보조 정리는 자체적으로 컴파일되고, 금지된 구문을 사용하지 않으며, Lean의 표준 공리에만 의존하는 경우에만 승인됩니다. 자식 하네스는 변경되지 않은 문장에 대한 증명만 점수를 매기므로, 보상을 조작( sorry 숨기기, 정리 편집, ≤ 재정의 등)해도 아무런 이득이 없습니다.

대상 사용자

• 기계 검증된 수학이나 형식 검증된 코드를 생성하는 AI 시스템을 구축하는 연구원 및 엔지니어.
• 조작할 수 없는 보상이 필요한 재귀적 자기 개선을 연구하는 팀.
• 공개된 AI 작성 증명의 정확성을 감사하는 모든 사람.

주요 특징

• 0/96 레드팀 부정행위 수락 – 모든 가짜 증명 거부, 25개의 정직한 솔루션 모두 수락.
• 4,219개의 공개된 AI 솔루션 감사 – Lean 및 Dafny에서 확인된 69개의 가짜 증명을 모두 거부했으며, 120개의 수락된 파일에 대한 무작위 감사에서 오탐률 0.2%, 누락 0건을 기록.
• 에이전트 연구 – 93개의 작업에서 OpenCode + GLM-5.3 Flash를 사용했을 때, 정직한 증명 비율이 41%(표준 종료 코드 보상)에서 하네스 사용 시 56%로 상승.
• 독성 방지 라이브러리 – 모든 보조 정리는 승인 전 커널 검증을 거치므로 라이브러리가 조용히 손상될 수 없음.
• 불변의 보상 – 자식은 변경되지 않은 문장에 대한 보류된 증명을 더 많이 인증할 때만 개선됨.
• 내장된 절제(Ablation) – --reward exit0는 일반적인 종료 코드 기준으로 동일한 루프를 실행하여 수락된 증명 중 얼마나 많은 것이 가짜인지 측정.
• MIT 라이선스 – 오픈 소스 및 독립형, Python 3.10+ 및 고정된 Lean/Dafny 툴체인 사용.