論文の概要: OpenProver: Agentic and Interactive Theorem Proving with Lean 4
- arxiv url: http://arxiv.org/abs/2607.09217v1
- Date: Fri, 10 Jul 2026 09:07:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.814052
- Title: OpenProver: Agentic and Interactive Theorem Proving with Lean 4
- Title（参考訳）: OpenProver: リーン4で証明したエージェント的かつインタラクティブな理論
- Abstract要約: OpenProverは、自動定理証明のためのオープンソースのシステムである。
OpenProverは、Aletheiaのような最近のATPエージェントシステムにインスパイアされたPlanner-Worker-Verifierアーキテクチャを統合している。
インタラクティブモードでは、OpenProverは、確立された人間-AIシナジーによって動機付けられた証明探索プロセスを監視し、操作することができる。
- 参考スコア（独自算出の注目度）: 0.5647577824219207
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems such as Aletheia. A Planner agent maintains a compact Whiteboard scratchpad and an unbounded Repository of intermediate findings, and decomposes mathematical work into parallel Workers. OpenProver is fully open-source, offers reproducible evaluation through automatic formal verification of generated proofs, and provides an interactive terminal interface for human-guided proof search. In interactive mode, OpenProver allows the human operator to monitor and steer the proof search process, motivated by the established human-AI synergy in interactive code generation. To showcase the potential for quantitative ablation experiments enabled by automatic formal verification, we evaluate OpenProver on ProofNet and compare it with a simple baseline. OpenProver is publicly available at https://github.com/kripner/OpenProver.
- Abstract（参考訳）: 本稿では,LLM駆動型自動定理証明(ATP)のためのオープンソースシステムであるOpenProverについて述べる。
OpenProverは、Aletheiaのような最近のATPエージェントシステムにインスパイアされたPlanner-Worker-Verifierアーキテクチャを統合している。
Plannerエージェントは、コンパクトなホワイトボードスクラッチパッドと中間結果の非有界リポジトリを保持し、数学的作業を並列ワーカーに分解する。
OpenProverは完全にオープンソースで、生成した証明の自動形式検証を通じて再現可能な評価を提供し、ヒューマンガイドによる証明検索のための対話型端末インタフェースを提供する。
対話的なモードでは、OpenProverは、対話的なコード生成において、確立された人間-AIシナジーによって動機付けられた証明探索プロセスを監視し、操作することができる。
自動形式検証による定量的アブレーション実験の可能性を示すため,ProofNet上でOpenProverを評価し,簡単なベースラインと比較した。
OpenProverはhttps://github.com/kripner/OpenProver.comで公開されている。
関連論文リスト
- OpenAI4S: Code as Action, Science as Sessions [57.428071188574]
我々は、emphCode as Action, Science as Sessionsという原則に基づいて構築されたオープンソースの科学研究エージェントOpenAI4Sを紹介する。
OpenAI4Sは、永続化コンピューティングランタイムとリサーチセッション管理オーケストレーションを組み合わせることで、構造化されたツールコールによって処理される。
再合成, 分子タンパク質結合体設計, タンパク質変異, 触媒スクリーニング, ミネラルスペクトロスコピーを含む36種類の研究シナリオにおけるOpenAI4Sの評価を行った。
論文 参考訳（メタデータ） (2026-09-14T06:16:59Z) - PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
PRIMAは、複数時間にわたる協調型マルチエージェント研究システムとして運用されている。
主なコントリビューションは、生存可能な障害モードのための3つの運用パターンである。
グラフ同型ケーススタディは、生成されたアーティファクトのアーキテクチャ的クレームを根拠にしている。
論文 参考訳（メタデータ） (2026-05-23T23:27:46Z) - OpenComputer: Verifiable Software Worlds for Computer-Use Agents [50.93029275079928]
OpenComputerは、コンピュータ利用エージェントの検証可能なソフトウェア世界を構築するための検証済みのフレームワークである。
OpenComputerは現在の形式で、ブラウザ、オフィスツール、クリエイティブソフトウェア、開発環境、ファイルマネージャ、通信アプリケーションにまたがる、33のデスクトップアプリケーションと1,000の最終的なタスクをカバーしている。
論文 参考訳（メタデータ） (2026-05-19T12:40:29Z) - OmniVL-Guard Pro: A Tool-Augmented Agent for Omnibus Vision-Language Forensics [63.13200245209719]
ツール拡張エージェントである textbf OmniVL-Guard Pro を提案する。
高品質なツール推論トラジェクトリを生成するために,textbfTree-Structured Self-Evolving Tool Trajectory Generationを導入する。
また,回答が正しいが推論が歪んだ場合に対して,プロセスレベルの監督を行うためのtextbfChecker-Guided Agentic Reinforcement Learningを提案する。
論文 参考訳（メタデータ） (2026-05-16T12:26:04Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - Cognitive Kernel-Pro: A Framework for Deep Research Agents and Agent Foundation Models Training [67.895981259683]
汎用AIエージェントは、次世代人工知能の基礎となるフレームワークとして、ますます認識されている。
現在のエージェントシステムはクローズドソースか、さまざまな有料APIやプロプライエタリなツールに大きく依存している。
我々は,完全オープンソースかつ(最大限に)フリーなマルチモジュールエージェントフレームワークであるCognitive Kernel-Proを提案する。
論文 参考訳（メタデータ） (2025-08-01T08:11:31Z) - Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。
GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
論文 参考訳（メタデータ） (2025-07-25T17:29:19Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - OpenR: An Open Source Framework for Advanced Reasoning with Large Language Models [61.14336781917986]
大規模言語モデル(LLM)の推論能力を高めるためのオープンソースのフレームワークであるOpenRを紹介する。
OpenRは、データ取得、強化学習トレーニング、非自己回帰デコーディングを凝集性ソフトウェアプラットフォームに統合する。
私たちの研究は、OpenAIのo1モデルのコア技術と強化学習を探求する、オープンソースのフレームワークを初めて提供するものです。
論文 参考訳（メタデータ） (2024-10-12T23:42:16Z) - OpenOmni: A Collaborative Open Source Tool for Building Future-Ready Multimodal Conversational Agents [11.928422245125985]
Open Omniはオープンソースのエンドツーエンドパイプラインベンチマークツールである。
音声テキスト、感情検出、検索拡張生成、大規模言語モデルなどの高度な技術を統合している。
ローカルとクラウドのデプロイメントをサポートし、データのプライバシを確保し、レイテンシと精度のベンチマークをサポートする。
論文 参考訳（メタデータ） (2024-08-06T09:02:53Z) - CREPO: An Open Repository to Benchmark Credal Network Algorithms [78.79752265884109]
クレダルネットワークは、確率質量関数の集合であるクレダルに基づく不正確な確率的グラフィカルモデルである。
CREMAと呼ばれるJavaライブラリが最近リリースされ、クレダルネットワークをモデル化し、処理し、クエリする。
我々は,これらのモデル上での推論タスクの正確な結果とともに,合成クレダルネットワークのオープンリポジトリであるcrrepoを提案する。
論文 参考訳（メタデータ） (2021-05-10T07:31:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。