論文の概要: What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
- arxiv url: http://arxiv.org/abs/2508.02733v1
- Date: Fri, 01 Aug 2025 22:16:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-06 18:18:55.589507
- Title: What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
- Title（参考訳）: 証明とは何か? 専門家によるF*とVerusの証明過程の分析
- Abstract要約: 我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
- 参考スコア（独自算出の注目度）: 2.8003002159083237
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements. Despite their powerful capabilities, POPLs present a steep learning curve and have not yet been adopted by the broader software community. The lack of understanding about the proof-development process and how expert proof developers interact with POPLs has hindered the advancement of effective proof engineering and the development of proof-synthesis models/tools. In this work, we conduct a user study, involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages, F* and Verus. Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process. We identify three distinct strategies and multiple informal practices that are not captured final code snapshots, yet are predictive of task outcomes. We translate these findings into concrete design guidance for AI proof assistants: bias toward early specification drafting, explicit sub-goal decomposition, bounded active errors, and disciplined verifier interaction. We also present a case study of an F* proof agent grounded in these recommendations, and demonstrate improved performance over baseline LLMs
- Abstract（参考訳）: Proof-oriented programming languages (POPL) は、開発者が正式な正当性証明と共にコードを書くことを許可し、コードが特定の要件に準拠することを正式な保証を提供する。
強力な能力にもかかわらず、POPLは学習曲線が急激であり、まだ幅広いソフトウェアコミュニティで採用されていない。
実証開発プロセスに関する理解の欠如と、POPLと開発者がどのように相互作用するかの専門家による証明工学の進歩と証明合成モデル/ツールの開発を妨げている。
本研究では,F*とVerusという2つの言語で作業する8人の専門家による詳細なソースコードテレメトリの収集と解析を行う。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
3つの異なる戦略と複数の非公式なプラクティスを特定し、最終的なコードスナップショットをキャプチャしていないが、タスクの結果を予測する。
これらの知見を,初期仕様の草案作成へのバイアス,明示的なサブゴール分解,有界能動誤差,規律付き検証者相互作用といった,AI証明アシスタントのための具体的な設計指針に翻訳する。
また,これらの勧告に基づくF*証明エージェントの事例研究を行い,ベースラインLLMの性能向上を実証した。
関連論文リスト
- Show Me The Money: An Exercise in Proof-Driven Software Understanding [1.678913049066618]
我々は、StellarブロックチェーンのSDEX注文ブックを実装するコアアルゴリズムの形式解析に重点を置いている。
コードの変更を既存の不変量に対して簡単にチェックできるように、アーティファクトを生成します。
この研究は、定理証明とモデル検査の戦略的組み合わせが、レガシーシステムに堅牢な保証を提供するための道を提供することを示す。
論文 参考訳（メタデータ） (2026-07-17T20:39:40Z) - DPrivBench: Benchmarking LLMs' Reasoning for Differential Privacy [50.73304874527716]
差分プライバシー(DP)は、データプライバシーを保護する幅広いアプリケーションを持っているが、DPアルゴリズムの設計と検証には専門家レベルの推論が必要である。
DPrivBenchは、各インスタンスが、ある関数やアルゴリズムが指定されたDP保証を満たすかどうかを問うベンチマークである。
実験によると、最強のモデルは教科書の仕組みをうまく扱えるが、全てのモデルは高度なアルゴリズムに苦しむ。
論文 参考訳（メタデータ） (2026-04-17T09:03:11Z) - Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。
ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。
タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
論文 参考訳（メタデータ） (2026-04-07T01:19:41Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。
本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
論文 参考訳（メタデータ） (2025-05-20T15:13:32Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。
本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
論文 参考訳（メタデータ） (2024-12-11T19:17:28Z) - Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。
証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
論文 参考訳（メタデータ） (2024-10-30T18:00:04Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。
AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
論文 参考訳（メタデータ） (2024-06-26T14:47:28Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。