[Paper] RocqSmith: 자동 최적화가 더 나은 Proof Agents를 만들 수 있을까?

Source: arXiv - 2602.05762v1

Overview

The paper RocqSmith: Can Automatic Optimization Forge Better Proof Agents? investigates whether modern AI‑driven optimizer frameworks—originally built for reinforcement‑learning agents or large language models—can be repurposed to improve automated theorem provers that work inside the Coq proof assistant. By treating a Coq proof‑generation bot as an “agent” and letting off‑the‑shelf optimizers tune its prompts, knowledge base, and control flow, the authors ask: can we replace painstaking hand‑crafting with a fully automatic pipeline?

Korean Translation

Overview

논문 *RocqSmith: Can Automatic Optimization Forge Better Proof Agents?*는 현대 AI 기반 최적화 프레임워크—원래는 강화 학습 에이전트나 대형 언어 모델을 위해 설계된 것—를 Coq 증명 보조기 안에서 동작하는 자동 정리 증명기에 적용하여 개선할 수 있는지를 조사한다. Coq 증명 생성 봇을 “에이전트”로 간주하고, 기존 최적화 도구가 프롬프트, 지식 베이스, 제어 흐름을 조정하도록 함으로써, 저자들은 손수 정교하게 설계하는 과정을 완전 자동 파이프라인으로 대체할 수 있는가를 질문한다.

주요 기여

• 옵티마이저 패밀리 벤치마킹 – 저자들은 여러 일반 옵티마이저 스위트(예: 베이지안 최적화, 진화 전략, few‑shot 부트스트래핑)를 Coq 증명‑생성 에이전트 튜닝 작업에 적용한다.
• 세밀한 “에이전트” 파라미터 연구 – 그들은 증명 에이전트에 중요한 세 가지 레버(프롬프트 설계, 컨텍스트 지식 주입, 제어 전략 선택)를 식별하고 이를 옵티마이저에 노출한다.
• 실제 Coq 라이브러리를 통한 실증 평가 – 표준 라이브러리, MathComp, Verified Software Toolchain의 일부를 포함한 다양한 Coq 개발 세트에서 실험을 수행하여 현실적인 성능 모습을 제공한다.
• 단순한 few‑shot 부트스트래핑이 더 복잡한 옵티마이저보다 우수함을 발견 – 베이지안 및 진화 방법의 정교함에도 불구하고, 경량의 few‑shot 프롬프트 접근법이 일관되게 가장 큰 향상을 제공한다.
• 오픈소스 툴링 – 이 논문은 RocqSmith 프레임워크를 공개한다. 이는 플러그‑앤‑플레이 래퍼로, 연구자들이 최소한의 코드 변경으로 어떤 옵티마이저든 Coq 증명 에이전트에 연결할 수 있게 한다.

방법론

1. Base Proof Agent – 저자들은 정리 명제를 받아 Coq 전술 시퀀스를 반환하는 대형 언어 모델(LLM) 위에 구축된 기본 Coq 증명 생성 시스템에서 시작한다.
2. Parameter Space Definition
   • Prompt Templates: 문구, 예시 순서, 그리고 “chain‑of‑thought” 힌트의 변형.
   • Contextual Knowledge: 배경으로 제공되는 가져온 보조정리, 정의, 혹은 이전에 증명된 정리들.
   • Control Strategies: 생성되는 후보 전술 시퀀스의 수, 언제 백업 증명자를 호출할지, 실패한 시도들을 어떻게 가지치기할지.
3. Optimizers Tested
   • Bayesian Optimization (BO) – 성능 표면을 모델링하고 유망한 구성들을 선택한다.
   • Evolutionary Strategies (ES) – 변이와 선택을 통해 구성들의 집단을 진화시킨다.
   • Few‑Shot Bootstrapping (FSB) – 이전 실행에서 발견된 성공적인 증명 조각을 프롬프트에 반복적으로 추가한다(자기 플레이 형태).
4. Evaluation Protocol – 각 옵티마이저마다 시스템은 500개의 정리로 구성된 보류 테스트 세트에서 실행된다. 성공은 proof completion rate (완전히 증명된 정리 비율)와 average tactic count (효율성)으로 측정한다.
5. Baseline Comparison – 결과는 이전 연구에서 제시된 손수 튜닝된 최신 Coq 증명 에이전트(“engineered” 베이스라인)와 비교된다.

결과 및 발견

• Few‑Shot Bootstrapping은 지속적으로 더 무거운 BO와 ES 방법보다 뛰어난 성과를 보였으며, 성공률과 효율성 모두에서 가장 큰 향상을 제공했습니다.
• 자동 최적화기 중 어느 것도 수동으로 설계된 증명 에이전트의 절대적인 성능에 도달하지 못했으며, 수동 에이전트는 여전히 완료율에서 약 5 % 정도의 우위를 유지했습니다.
• 최적화기에서 생성된 프롬프트 템플릿은 간결하고 예시가 풍부한 형태로 수렴하는 경향이 있었으며, 이는 정리 증명 커뮤니티의 경험적 모범 사례를 확인시켜줍니다.
• 맥락 지식 선택이 더 민감한 것으로 나타났습니다: BO와 ES는 때때로 관련 없는 보조정리를 에이전트에 과다하게 제공하여 성능을 저하시켰지만, FSB는 가장 유용한 사실만을 표출하도록 학습했습니다.

Practical Implications

• Rapid Prototyping for New Domains – 개발자는 이제 일반적인 옵티마이저를 Coq 기반 검증 파이프라인에 끼워 넣고, 수동 프롬프트 엔지니어링에 몇 주가 걸리던 작업을 몇 시간 안에 “충분히 좋은” 증명 에이전트로 만들 수 있습니다.
• Continuous Improvement in CI – RocqSmith 래퍼를 지속적 통합(CI) 워크플로에 통합할 수 있습니다: 새로운 라이브러리가 추가될 때마다 옵티마이저가 자동으로 프롬프트와 컨텍스트를 정제하여 증명 자동화를 최신 상태로 유지합니다.
• Lower Barrier for Formal Methods Adoption – Coq 전술에 대한 깊은 전문 지식이 없는 팀도 소수 샷 부트스트래핑 루프를 활용해 사용 가능한 증명 스크립트를 생성할 수 있어, 안전‑중요 소프트웨어, 암호 프로토콜, 하드웨어 설계 검증을 가속화합니다.
• Template for Other Proof Assistants – 비록 이번 연구가 Coq에 초점을 맞추었지만, 동일한 옵티마이저‑에이전트 패턴을 Lean, Isabelle, Agda 등 다른 증명 보조 도구에 적용할 수 있어, 범용적이고 자체 최적화되는 증명 보조 도구로 나아가는 길을 엽니다.
• Cost‑Effective Use of LLMs – 불필요한 컨텍스트를 자동으로 제거하고 생성되는 전술 후보 수를 제한함으로써, 상용 LLM 제공자의 API 호출량을 감소시켜 실질적인 비용 절감을 실현합니다.

제한 사항 및 향후 연구

• 핸드‑튜닝된 에이전트와의 성능 격차 – 가장 뛰어난 자동 최적화기조차 전문가가 만든 시스템에 미치지 못하며, 세밀한 도메인 지식(예: 맞춤형 전술 결합자)을 자동으로 포착하기 어렵다는 것을 보여준다.
• 최적화 루프의 확장성 – 베이지안 및 진화적 방법은 많은 평가 실행을 필요로 했으며, 각 증명 시도가 비용이 많이 드는 LLM 추론을 포함할 때 비용이 크게 증가할 수 있다.
• 벤치마크를 넘어선 일반화 – 테스트 스위트는 다양하지만 여전히 선별된 정리 집합을 나타낸다; 고도로 특화된 라이브러리를 가진 실제 코드베이스는 다른 동작을 보일 수 있다.
• 향후 방향 – 저자들은 여러 증명 도우미에 걸친 메타‑러닝, few‑shot 부트스트래핑과 LLM의 그래디언트 기반 미세조정을 결합한 하이브리드 접근법, 그리고 Coq 자체의 증명 검색 메커니즘과의 긴밀한 통합을 탐구하여 성능 격차를 메우는 것을 제안한다.

저자

• Andrei Kozyrev
• Nikita Khramov
• Denis Lochmelis
• Valerio Morelli
• Gleb Solovev
• Anton Podkopaev

논문 정보

• arXiv ID: 2602.05762v1
• 카테고리: cs.AI, cs.LG, cs.LO, cs.SE
• 출판일: 2026년 2월 5일
• PDF: PDF 다운로드