전 Axiom Math, Kimi 연구원들이联手창업, AI로 칩 검증 난제 돌파

동찰 Beating AI 속보, 칩 설계에서 가장 두려운 것 중 하나는 제조 후에야 논리 오류를 발견하는 것입니다. 문제가 발생하면 재설계와 재테이프아웃이 필요해 막대한 비용을 치러야 할 수 있습니다. 칩 검증은 제조 전에 이러한 숨겨진 오류를 최대한 찾아내는 것을 목표로 합니다.

전통적인 칩 검증은 주로 시뮬레이션 테스트에 의존하지만, 칩 내부의 동작 상태 조합은 천문학적인 수에 달할 수 있어 하나하나 테스트하는 것은 불가능합니다. 형식 검증은 수학적 방법을 활용해 칩이 규정된 조건에서 항상 특정 규칙을 준수함을 증명합니다. 예를 들어, 원래 동시에 켜져서는 안 되는 두 회로가 특정 특수 조작으로 인해 함께 켜져서는 안 된다는 것입니다.

이 방법은 이미 오래전부터 존재했지만, 복잡한 칩의 수학적 증명은 매우 어렵습니다. 많은 문제는 전문가가 수작업으로 처리해야 하며, 기존 도구는 계산 규모가 너무 커서 결론을 내지 못할 수도 있습니다.

레이펑망 보도에 따르면, Axiom Math 전 형식 검증 책임자 장쥐젠과 월지암면에서 AI 수학을 연구한 류쥔치가 베이징 유리수과기(有理数科技)를 창업하여 AI를 활용해 더 많은 칩 형식 증명 작업을 자동으로 완수하고 있습니다. 회사는 시드 라운드 투자를 완료했습니다.

두 사람 모두 강력한 수학적 증명 배경을 가지고 있습니다. 장쥐젠은 Mathlib와 AxiomProver 개발에 참여했습니다. 류쥔치는 Numina-Lean-Agent의 핵심 저자로, 이 시스템은 2025년 퍼트남 수학 경시대회 전 12문제를 성공적으로 증명하고 Lean 도구를 통해 증명 과정을 검증했습니다.

현재 유리수는 기술 프로토타입을 완성하여 십수만 줄의 RTL 코드가 관련된 칩 프로젝트에서 기존 EDA 도구로는 판정할 수 없는 일부 단언을 검증했습니다. 팀은 칩 고객과 협력하여 이 역량을 상용화된 검증 서비스로 만들기 위해 시도하고 있습니다.