Fugu-MT 論文翻訳(概要): ProofStudio: Five Proof Assistants in the Browser

論文の概要: ProofStudio: Five Proof Assistants in the Browser

arxiv url: http://arxiv.org/abs/2611.05540v1
Date: Tue, 03 Nov 2026 19:32:16 GMT
ステータス: 翻訳完了
システム内更新日: 2026-11-06 03:25:57.826651
Title: ProofStudio: Five Proof Assistants in the Browser
Title（参考訳）: ProofStudio:ブラウザの5つの証明アシスタント
Abstract要約: AI支援による証明自動化の最近の進歩は、ソフトウェア検証と数学における証明アシスタントの使用を拡張している。本稿では,Isabelle/HOL,Lean,Rocq,HOL4,HOL Lightを統合したブラウザベースの環境であるProofStudioを紹介する。
参考スコア（独自算出の注目度）: 1.8275108630751837
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Recent advances in AI-assisted proof automation are extending the use of proof assistants in software verification and mathematics. However, greater proof automation does not remove users' responsibility to assess whether formal statements capture their intended requirements, making education in formal specification and reasoning essential. To lower the installation and learning barriers associated with mature proof assistants, we present ProofStudio, a browser-based environment integrating Isabelle/HOL, Lean, Rocq, HOL4, and HOL Light with corresponding worked examples, preconfigured proof search, and contextual AI assistance. With ProofStudio, users can explore formal specifications and proofs across five systems without local installation, inspecting native prover feedback and experimenting with automation through a common interface.
Abstract（参考訳）: AI支援による証明自動化の最近の進歩は、ソフトウェア検証と数学における証明アシスタントの使用を拡張している。しかし、より大規模な証明自動化は、形式的なステートメントが意図した要件を捉え、正式な仕様で教育を行い、推論が不可欠であるかどうかを評価することに対するユーザの責任を排除しない。成熟した証明アシスタントに関連するインストールと学習障壁を低減するため、Isabelle/HOL、Lean、Rocq、HOL4、HOL Lightを統合したブラウザベースの環境であるProofStudioを紹介します。 ProofStudioを使用すると、ユーザーはローカルインストールなしで5つのシステムにまたがる正式な仕様や証明を探り、ネイティブの証明者フィードバックを検査し、共通のインターフェースを通じて自動化を試すことができる。

関連論文リスト

VeriCUA: Verification as Agentic Exploration for Computer-Using Agents [95.35011917414766]
コンピュータ利用エージェントの構築とスケーリングには、信頼性の高いタスク補完検証が必要である。エージェント探索による検証のためのプラットフォームに依存しないフレームワークであるVeriCUAを提案する。
論文参考訳（メタデータ） (2026-10-29T17:45:26Z)
Synthesizing Proofs Using Proof Sharding and Exploration [0.0]
ProofSaXは、大規模な検証タスクをシャード化し、各シャードに対する証明検索空間を独立に探索し、正当性証明を合成する自動ツールである。 ProofSaXは103の証明補完タスクのうち86で最後の証明アノテーションを見つけることができ、実行時間は1分から2時間である。
論文参考訳（メタデータ） (2026-09-22T20:07:09Z)
Evaluating LLM-Generated ACSL Annotations for Formal Verification [0.0]
本稿では,ACSL 仕様を人的・学習的支援なしに自動生成・検証できる形式分析ツールの規模を実証的に評価する。 5つのACSL生成システムを比較する:ルールベースのPythonスクリプト、Frama-CのRTEプラグイン、3つの大きな言語モデル。生成された仕様はすべて、複数のSMTソルバを動力とするFrama-C WPプラグインを使用して、同一条件下で検証される。
論文参考訳（メタデータ） (2026-02-14T19:18:34Z)
Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文参考訳（メタデータ） (2026-02-02T17:42:53Z)
Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles [3.4742046772246837]
110 Dafnyプログラムの実験では、Claude Opus 4.5 と GPT-5.2 を組み合わせたマルチモデルアプローチが、少なくとも8回の修正イテレーションで98.2%のプログラムに対して正しいアノテーションを生成した。ロジスティック回帰分析では、証明-ヘルパーアノテーションが現在のLLMの難易度に不相応に寄与していることが示された。
論文参考訳（メタデータ） (2026-01-19T08:56:43Z)
What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文参考訳（メタデータ） (2025-08-01T22:16:30Z)
Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文参考訳（メタデータ） (2024-10-21T08:15:45Z)
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
論文参考訳（メタデータ） (2024-04-18T22:54:08Z)
Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。 GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
論文参考訳（メタデータ） (2024-01-15T13:08:38Z)
ProofBuddy: A Proof Assistant for Learning and Monitoring [0.0]
証明能力(Proof competence)、すなわち、(数学的な)証明を書き、チェックする能力は、コンピュータ科学において重要なスキルである。主な問題は、形式言語の正しい使用と証明、特に学生自身の証明が完璧で正しいかどうかの確認である。多くの著者は、証明能力を教えるのに証明アシスタントを使うことを提案したが、その方法の有効性は明らかではない。デンマーク工科大学でProofBuddyのユーザビリティに関する予備的な研究を行った。
論文参考訳（メタデータ） (2023-08-14T07:08:55Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。