כתבה
arXiv cs.AI ·
פיתוח שרת רוקו להוכחות מכוניות: תכנון כלי חדש להוכחות זולות ב-Rocq ו-Lean
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
במאמר זה, המחברים מציגים שרת חדש להוכחות מכוניות ב-Rocq ו-Lean, שפותח באמצעות תכנון כלי חדש. השרת, שנקרא ROCQ-MCP-EVOLVE, משפר את היעילות של הוכחות בשני הפרוברים. המחברים מציגים גם תוצאות של ניסויים שהוכיחו את יעילות השרת.
תקציר מקורי באנגליתarXiv:2609.39544v3 Announce Type: replace Abstract: Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the cost of these interactions. Today, these interfaces are adapted from tools designed for humans and not optimized for agents. We propose an evolutionary method where a frontier model incrementally proposes new features and only keeps the ones that improve the overall performance of smaller models. We demonstrate the effectiveness of our method by growing, on a curated set of mathematical problems, ROCQ-MCP-EVOLVE, a new MCP server for the Rocq pr
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית