論文の概要: Execution Time Program Verification With Tight Bounds

• arxiv url: http://arxiv.org/abs/2210.11105v1
• Date: Thu, 20 Oct 2022 09:02:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2022-10-21 14:33:29.088516
• Title: Execution Time Program Verification With Tight Bounds
• Title（参考訳）: タイト境界による実行時間プログラム検証
• Authors: Ana Carolina Silva, Manuel Barbosa and Mario Florido
• Abstract要約: 本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。 3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。 証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
• 参考スコア（独自算出の注目度）: 6.36836017515443
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.
• Abstract（参考訳）: 本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。 証明システムは3つの異なるシナリオで定義されている: 最悪の場合の実行時間の近似、正確な時間推論、償却分析による悲観的実行時間の推定。 3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作意味論に関してその健全性を証明する。 最後に、プログラムの正確性、コスト、終了の証明に必要なゴールを生成する検証条件(VC)の生成を定義する。 それらの目標は、検証のためにeasycryptツールセットに送られる。 証明システムの実用性は,ocamlで実装したサンプルプログラムに適用するために必要なモジュールによって実証される。 私たちのケーススタディは、リアルタイムおよび暗号化ソフトウェアが動機です。

関連論文リスト

• SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference [7.324314351910779]
  SpecMindは、LEMをインタラクティブで探索的な推論として扱う、ポストコンディション生成のための新しいフレームワークである。 我々の経験的評価は、SpecMindが生成後条件の正確性と完全性の両方において最先端のアプローチを著しく上回っていることを示している。
  論文  参考訳（メタデータ） (2026-02-24T07:01:17Z)
• interwhen: A Generalizable Framework for Verifiable Reasoning with Test-time Monitors [47.363850513075356]
  実験時間検証フレームワークであるInterwhenを提案し, 与えられた検証結果に対して, 推論モデルの出力が有効であることを保証する。 検証された推論は、物理的な世界にエージェントを配置するといった高度なシナリオにおいて重要な目標である。
  論文  参考訳（メタデータ） (2026-02-05T08:35:01Z)
• Can LLMs Compress (and Decompress)? Evaluating Code Understanding and Execution via Invertibility [36.41073880422337]
  RoundTripCodeEval(RTCE)は、4つの異なるコード実行推論タスクからなる包括的なベンチマークである。 ゼロショットプロンプト、実行トレースの教師付き微調整、自己回帰機構を用いて、最先端のコード-LLMを体系的に評価する。 RTCEは、既存のI/O予測、実行推論、ラウンドトリップの自然言語ベンチマークによって捉えられていない、これまで測定されていなかったいくつかの新しい洞察を表面化している。
  論文  参考訳（メタデータ） (2026-01-19T21:09:48Z)
• Chain-of-thought Reviewing and Correction for Time Series Question Answering [22.889720488678076]
  本稿では,時系列質問応答の明示的な補正機構を備えた多段階推論を行うT3LLMを提案する。 このフレームワーク内では、作業者は構造化されたプロンプトの下で段階的思考連鎖(CoT)を生成し、レビュアーは推論を検査し、誤ったステップを特定し、修正的なコメントを提供する。 複数の実世界のTSQAベンチマークの実験により、T3LLMは強力なLLMベースのベースラインに対して最先端のパフォーマンスを達成することが示された。
  論文  参考訳（メタデータ） (2025-12-27T15:54:18Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Adaptive Test-Time Reasoning via Reward-Guided Dual-Phase Search [62.1546099504045]
  本稿では、推論を計画と実行に分離する二相テストタイムスケーリングフレームワークを提案する。 具体的には、推論軌跡を分解し、各フェーズの報酬モデルを構築し、探索者が個別に計画と実行を探索、実行できるようにする。 数学的推論とコード生成ベンチマークの両方の実験により、我々の手法は計算の冗長性を低減しつつ、常に精度を向上することを示した。
  論文  参考訳（メタデータ） (2025-09-29T19:27:23Z)
• Overclocking LLM Reasoning: Monitoring and Controlling Thinking Path Lengths in LLMs [52.663816303997194]
  回答の質に影響を与える重要な要因は思考段階の長さである。 本稿では, LLM が推論の長さを理解し, 制御するメカニズムを探求し, 活用する。 以上の結果から,この「オーバークロック」手法は過度な思考を軽減し,解答精度を向上し,推論遅延を低減することが示唆された。
  論文  参考訳（メタデータ） (2025-06-08T17:54:33Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [5.783301542485619]
  エンドツーエンドのプログラム検証タスクにおいて,大規模言語モデル(LLM)を評価するために設計された新しいベンチマークを導入する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ4%未満のパス率を達成でき,多くの出力がコンパイルに失敗していることがわかった。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• C*: Unifying Programming and Verification in C [15.531046191957529]
  C* は C プログラミングのための言語設計の証明である。 プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。 C* は C を共通言語として使用することで実装と証明コード開発を統合する。
  論文  参考訳（メタデータ） (2025-04-03T03:22:22Z)
• A Case Study on Model Checking and Runtime Verification for Awkernel [0.7199733380797578]
  人間が手動で同時動作をレビューしたり、可能なすべての実行をカバーしたテストケースを書くことは難しい。 本稿では,スケジューラなどの並列ソフトウェアの開発手法を提案する。
  論文  参考訳（メタデータ） (2025-03-12T11:27:45Z)
• FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
  FIREはエビデンス検索とクレーム検証を反復的に統合する新しいフレームワークである。 大きな言語モデル(LLM)のコストを平均7.6倍、検索コストを16.5倍削減しながら、パフォーマンスが若干向上している。 これらの結果から,FIREは大規模ファクトチェック業務における適用を約束していることが明らかとなった。
  論文  参考訳（メタデータ） (2024-10-17T06:44:18Z)
• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。 Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
  論文  参考訳（メタデータ） (2024-07-11T12:51:08Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。 本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T08:26:52Z)
• Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories [9.45355418401911]
  最も一般的に使用されるアプローチは、実値の流れる$mathittime(a)$を追加して、各アクションにタイムポイントをアタッチし、結果として各状況にアタッチすることで、時間を表す。 このアプローチでは、言論の領域が有限個の対象に制限されている場合でも、与えられた式を満たす到達可能な状況が決定不能であるかどうかを確認する。
  論文  参考訳（メタデータ） (2024-02-05T16:32:12Z)
• Unlocking Temporal Question Answering for Large Language Models with Tailor-Made Reasoning Logic [84.59255070520673]
  大きな言語モデル(LLM)は、時間的推論に関わる際に課題に直面します。 本研究では,時間的質問応答タスクに特化して設計された新しいフレームワークであるTempLogicを提案する。
  論文  参考訳（メタデータ） (2023-05-24T10:57:53Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• Time-varying Gaussian Process Bandit Optimization with Non-constant Evaluation Time [93.6788993843846]
  非定常評価時間を効果的に処理できる新しい時間変化ベイズ最適化アルゴリズムを提案する。 我々の限界は、評価時間列のパターンが問題の難易度に大きな影響を与えることを決定づける。
  論文  参考訳（メタデータ） (2020-03-10T13:28:33Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。