論文の概要: Show Me The Money: An Exercise in Proof-Driven Software Understanding
- arxiv url: http://arxiv.org/abs/2607.16499v1
- Date: Fri, 17 Jul 2026 20:39:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.168502
- Title: Show Me The Money: An Exercise in Proof-Driven Software Understanding
- Title（参考訳）: お金を見せろ - テスト駆動ソフトウェア理解のエクササイズ
- Abstract要約: 我々は、StellarブロックチェーンのSDEX注文ブックを実装するコアアルゴリズムの形式解析に重点を置いている。
コードの変更を既存の不変量に対して簡単にチェックできるように、アーティファクトを生成します。
この研究は、定理証明とモデル検査の戦略的組み合わせが、レガシーシステムに堅牢な保証を提供するための道を提供することを示す。
- 参考スコア（独自算出の注目度）: 1.678913049066618
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
- Abstract（参考訳）: 本稿では、成熟したセキュリティクリティカルなインフラストラクチャの証明駆動型ソフトウェア理解に関するケーススタディを示す。
フォーマルなメソッドは伝統的に設計段階で適用されますが、成熟した産業用C++コードベースにフォーマルな推論を適用した経験を示します。
我々は、StellarブロックチェーンのSDEX注文ブックを実装するコアアルゴリズムの形式解析に重点を置いている。
大規模言語モデル(LLM)、プロトタイプ検証システム(PVS)、SeaHornを組み合わせることで、プロダクションコードベースのコア特性を証明できます。
提案手法では,例外位置の到達性に関する文書の矛盾も確認した。
しかし、最も重要なことは、コードの変更を既存の不変量に対して簡単にチェックできるように、アーティファクトを生成します。
この研究は、定理証明とモデル検査の戦略的組み合わせが、レガシーシステムに堅牢な保証を提供するための道を提供することを示す。
関連論文リスト
- Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
この研究では、非公式な定理における主要なボトルネックを洞察の欠如として証明する。
我々は,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行うことを可能にする新しいフレームワークを提案する。
問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。
論文 参考訳（メタデータ） (2026-04-17T17:36:21Z) - Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training [2.62112541805429]
Reasoning Coreは、コア形式ドメイン間で検証可能なシンボリック推論データを手続き的に生成するスケーラブルなスイートである。
各タスクは厳密な検証のための外部解決器と組み合わせられ、カリキュラム設計のための継続的な難易度制御が認められる。
実験によると、Reasoning Coreのデータを事前トレーニングに混ぜることによって、下流の推論が改善され、保存されたり、わずかに改善された言語モデリングの品質が向上する。
論文 参考訳（メタデータ） (2026-03-02T18:59:29Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Constant-Size Cryptographic Evidence Structures for Regulated AI Workflows [0.0]
本稿では,規制環境におけるAIの正当性検証のための暗号証拠構造について紹介する。
それぞれのエビデンス項目は、(i)ワークフローイベントとコンフィギュレーションへの強いバインドを提供するように設計された、固定サイズの暗号化フィールドの固定サイズであり、(ii)一定のサイズのストレージとイベント毎の検証コストをサポートし、(iii)ハッシュチェーンとMerkleベースの監査をクリーンに構成する。
論文 参考訳（メタデータ） (2025-11-21T10:28:07Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。
本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。
我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
論文 参考訳（メタデータ） (2025-10-01T16:06:40Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。
LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。
我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
論文 参考訳（メタデータ） (2025-04-23T18:04:38Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。