論文の概要: RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
- arxiv url: http://arxiv.org/abs/2505.22846v1
- Date: Wed, 28 May 2025 20:26:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-30 18:14:07.527764
- Title: RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
- Title（参考訳）: RocqStar: Rocq生成のための類似性駆動型検索とエージェントシステムを活用する
- Authors: Nikita Khramov, Andrei Kozyrev, Gleb Solovev, Anton Podkopaev,
- Abstract要約: 我々は、Rocq証明を生成するために、徹底した前提選択の重要性を強調した。
本稿では,自己注意型埋め込みモデルを用いた検索手法を提案する。
設計手法の評価では, 発電機の性能が28%向上した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Interactive Theorem Proving was repeatedly shown to be fruitful combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation and illuminates potential avenues for improvement. We highlight the importance of thorough premise selection for generating Rocq proofs and propose a novel approach, leveraging retrieval via a self-attentive embedder model. The evaluation of the designed approach shows up to 28% relative increase of the generator's performance. We tackle the problem of writing Rocq proofs using a multi-stage agentic system, tailored for formal verification, and demonstrate its high effectiveness. We conduct an ablation study and show the use of multi-agent debate on the planning stage of proof synthesis.
- Abstract（参考訳）: インタラクティブな定理証明は、ジェネレーティブ・人工知能(Generative Artificial Intelligence)と組み合わさって実りあることが繰り返し示された。
本稿では、Rocq生成に対する複数のアプローチを評価し、改善のための潜在的な道筋を照らす。
本稿では,Rocq証明を生成するための前提条件選択の重要性を強調し,自己注意型埋め込みモデルによる検索を活用する新しい手法を提案する。
設計手法の評価では, 発電機の性能が28%向上した。
多段エージェントシステムを用いたRocq証明の書込み問題に対処し,その有効性を実証する。
我々はアブレーション研究を行い、証明合成の計画段階におけるマルチエージェントの議論の活用を示す。
関連論文リスト
- Chain-of-Retrieval Augmented Generation [72.06205327186069]
本稿では,o1-like RAGモデルを学習し,最終回答を生成する前に段階的に関連情報を抽出・推論する手法を提案する。
提案手法であるCoRAGは,進化状態に基づいて動的にクエリを再構成する。
論文 参考訳（メタデータ） (2025-01-24T09:12:52Z) - RAGEval: Scenario Specific RAG Evaluation Dataset Generation Framework [66.93260816493553]
本稿では,様々なシナリオにまたがってRAGシステムを評価するためのフレームワークであるRAGvalを紹介する。
事実の正確性に焦点をあてて,完全性,幻覚,不適切性の3つの新しい指標を提案する。
実験結果から, RAGEvalは, 生成した試料の明瞭度, 安全性, 適合性, 豊かさにおいて, ゼロショット法とワンショット法より優れていた。
論文 参考訳（メタデータ） (2024-08-02T13:35:11Z) - An Empirical Study of Retrieval Augmented Generation with Chain-of-Thought [8.195946489216967]
本稿では,RAFT(Retrieval Augmented Fine-Tuning)法の有効性について述べる。
RAFT法を複数のデータセットにまたがって評価し,その性能を様々な推論タスクで解析した。
論文 参考訳（メタデータ） (2024-07-22T11:55:14Z) - Non-autoregressive Generative Models for Reranking Recommendation [9.854541524740549]
推薦システムでは、項目間のリスト内相関をモデル化することで、リランクが重要な役割を果たす。
本研究では, 効率と効率性を高めるために, 提案するレコメンデーション(NAR4Rec)の再評価のための非自己回帰生成モデルを提案する。
NAR4Recは、毎日3億人のアクティブユーザーがいる人気ビデオアプリKuaishouに完全にデプロイされている。
論文 参考訳（メタデータ） (2024-02-10T03:21:13Z) - CCA: Collaborative Competitive Agents for Image Editing [55.500493143796405]
本稿では,CCA(Collaborative Competitive Agents)の新たな生成モデルを提案する。
複数のLarge Language Models (LLM) ベースのエージェントを使って複雑なタスクを実行する。
この論文の主な貢献は、制御可能な中間ステップと反復最適化を備えたマルチエージェントベースの生成モデルの導入である。
論文 参考訳（メタデータ） (2024-01-23T11:46:28Z) - UnitedQA: A Hybrid Approach for Open Domain Question Answering [70.54286377610953]
最近の訓練済みのニューラル言語モデルに基づいて,抽出的および生成的読取能力を高めるために,新しい手法を適用した。
私たちのアプローチは、それぞれNaturalQuestionsとTriviaQAと正確な一致で、以前の最先端のモデルを3.3と2.7ポイント上回る。
論文 参考訳（メタデータ） (2021-01-01T06:36:16Z) - SARG: A Novel Semi Autoregressive Generator for Multi-turn Incomplete
Utterance Restoration [9.394277095571942]
本稿では,マルチターン対話システムにおける不完全な発話復元について検討する。
本稿では,高い効率と柔軟性を有する新しい半自己回帰発電機(SARG)を提案する。
論文 参考訳（メタデータ） (2020-08-04T11:52:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。