# 안트로피가 "AI 를 활용한 수학적 증명" 기법을 개발하여 "버그 없는 소프트웨어" 구현을 목표로 함

> https://bookfactory.kr/board/news/23560
> 게시판: 뉴스
> 작성자: tachikoma43
> 작성일: 2026-10-24T05:08:56.634Z

---

AI 성능의 향상으로 인해 다양한 소프트웨어의 버그가 대량으로 발견되고 있으며, PHP 긴급 업데이트와 같이 큰 영향을 미치는 사례도 나타나고 있습니다. 이러한 가운데 AI 기업 Anthropic이 "소프트웨어의 버그가 없는 것을 형식 검증으로 증명한다"는 방법을 연구 중임을 공개했습니다. LLMs 는 훨씬 더 큰 규모에서 형식 소프트웨어 검증이 가능하게 하고 있습니다 \ Anthropic https://www.anthropic.com/research/formal-verification 형식 검증은 소프트웨어 코드를 수학적 방법으로 표현하여 버그가 없음을 증명하는 방법입니다. 형식 검증이라는 아이디어 자체는 새로운 것이 아니지만, 실제 증명 작업에는 많은 노력이 필요하기 때문에 "항공기 탑재 항공전자 장비 코드"와 같이 치명적인 영향을 미칠 수 있는 시스템에서만 사용되어 왔습니다. Anthropic은 연구 조직 Theorem과 협력하여 Claude 를 사용하여 형식 검증을 수행하는 방법을 개발하고, 123 개의 오픈소스 라이브러리를 대상으로 형식 검증을 수행했습니다. 증명 과정에서 발견된 버그를 Claude 로 수정을 반복한 결과, "프로그램이 RISC-V 아키텍처 CPU 와 Linux 를 탑재한 머신에서 메모리 사용 가능량을 고정된 상태로 싱글 스레드 정적 바이너리로 실행될 때 버그로 인한クラッシュ가 발생하지 않는다는 것"을 수학적으로 증명할 수 있었다는 사실이 밝혀졌습니다.

형식적 검증 실행에는 1 억 토큰 이상을 소비하므로 비용 측면에서 과제가 존재합니다. 그러나 Anthropic 은 "모델 성능 향상과 함께 처리 토큰 수가 감소한다", "다른 소프트웨어에서도 유사한 증명 과정을 거칠 수 있으며, 증명 내용을 재사용함으로써 처리 토큰 수를 줄일 수 있다"는 등의 이유로 비용 문제는 점차 완화될 것으로 예상하고 있습니다. 아래 그래프는 36 건의 형식적 검증 실행 시 토큰 사용량 추이를 보여주며, Claude Opus 5.5 가 Claude Opus 5 보다 적은 토큰 수로 성과를 거두는 것을 알 수 있습니다.

Anthropic 에 따르면, 형식적 검증은 'RISC-V 에서 버그가 발생하지 않는 것을 증명할 수는 있으나, ARM 또는 x86 에서 버그가 발생할 수 있다'거나, '실제 사용 환경에서 버그가 존재하지 않음을 증명하려면 프로그램이 작동하는 모든 머신 구성을 포괄적으로 모델링해야 한다'는 등의 한계가 존재한다는 것입니다. 그럼에도 불구하고 Anthropic 은 'LLM 을 활용한 형식적 검증 방법론에 대한 이해가 깊어지고 모델이 개선될수록 이러한 제약은 극복 가능해진다'는 전망을 제시하고 있습니다. 또한, Theorem 은 LLM 을 활용한 형식적 검증 방법을 OSS 프로젝트에 무료로 제공하고 있습니다. 자세한 내용은 다음 링크를 통해 확인하실 수 있습니다. OSS Verify | Theorem https://theorem.dev/oss-verify/또한, 형식적 검증에 사용된 기술도 무료로 공개되었습니다. oss-verify/.claude/skills/add-project/SKILL.md at main · theorem-labs/oss-verify · GitHub https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md

[원문 보기](https://gigazine.net/news/20261023-anthropic-formal-verification/) | 출처: Gigazine