論文の概要: Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations

• arxiv url: http://arxiv.org/abs/2604.12747v1
• Date: Tue, 14 Apr 2026 13:58:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-15 19:11:32.473093
• Title: Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
• Title（参考訳）: VERIFAI2026論文の短いバージョン -- 融合形式推論の学習:契約合成, 人工物再利用, セマンティック基礎
• Authors: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan,
• Abstract要約: 本稿では,機械学習技術と形式検証を統合したLIFR(Learning-Infused Formal Reasoning)という研究ビジョンを概説する。 このフレームワークは、自然言語要求からの自動コントラクト合成、グラフマッチングと学習ベースの埋め込みを用いた検証アーティファクトのセマンティックリユース、および統一プログラミング理論(UTP)と制度理論に基づく数学的に基礎付けられたセマンティック基盤の3つの相補的な研究方向に焦点を当てている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Artificial intelligence systems have achieved remarkable capability in natural language processing, perception and decision-making tasks. However, their behaviour often remains opaque and difficult to verify, limiting their applicability in safety-critical systems. Formal methods provide mathematically rigorous mechanisms for specifying and verifying system behaviour, yet the creation and maintenance of formal specifications remains labour intensive and difficult to scale. This paper outlines a research vision called Learning-Infused Formal Reasoning (LIFR), which integrates machine learning techniques with formal verification workflows. The framework focuses on three complementary research directions: automated contract synthesis from natural language requirements, semantic reuse of verification artifacts using graph matching and learning-based embeddings, and mathematically grounded semantic foundations based on the Unifying Theories of Programming (UTP) and the Theory of Institutions. Together these research threads aim to transform verification from isolated correctness proofs into a cumulative knowledge-driven process where specifications, contracts and proofs can be synthesised, aligned and reused across systems.
• Abstract（参考訳）: 人工知能システムは自然言語処理、知覚、意思決定のタスクにおいて顕著な能力を達成した。 しかし、それらの行動はしばしば不透明で検証が難しいままであり、安全クリティカルなシステムにおける適用性を制限している。 形式的手法は、システムの振る舞いを特定し検証するための数学的に厳密なメカニズムを提供するが、形式的仕様の作成と保守は、労働集約的でスケールが難しいままである。 本稿では,機械学習技術と形式的検証ワークフローを統合するLIFR(Learning-Infused Formal Reasoning)という研究ビジョンを概説する。 このフレームワークは、自然言語要求からの自動コントラクト合成、グラフマッチングと学習ベースの埋め込みを用いた検証アーティファクトのセマンティックリユース、および統一プログラミング理論(UTP)と制度理論に基づく数学的に基礎付けられたセマンティック基盤の3つの相補的な研究方向に焦点を当てている。 これらの研究スレッドは、独立した正当性証明から、仕様、契約、証明をシステム間で合成、調整、再利用できる累積的知識駆動プロセスに変換することを目的としている。

関連論文リスト

• Leveraging LLM Parametric Knowledge for Fact Checking without Retrieval [60.25608870901428]
  信頼性は、大規模言語モデル(LLM)上に構築されたエージェントAIシステムの中核研究課題である 本研究では,任意の自然言語クレームの検証に焦点をあて,検索なしで事実チェックを行うタスクを提案する。
  論文  参考訳（メタデータ） (2026-03-05T18:42:51Z)
• Ontology-to-tools compilation for executable semantic constraint enforcement in LLM agents [0.0]
  本稿では,大規模言語モデル(LLM)と形式的ドメイン知識意味論を結合する原理実証機構を提案する。 オントロジー仕様は、LLMベースのエージェントが知識グラフインスタンスの作成と修正に使用する実行可能なツールツールにコンパイルされる。 本稿では, LLM インタフェースの有効性, マニュアルスキーマの削減, エンジニアリングの促進, フォーマルな知識を生成システムに組み込むための一般的なパラダイムの確立について述べる。
  論文  参考訳（メタデータ） (2026-02-03T12:03:26Z)
• Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics [0.0]
  ビジョンペーパーは、人工知能との交点における形式的手法に関する長期的な研究課題を記述している。 これは、自動化されたコントラクト合成、セマンティックアーティファクトの再利用、洗練に基づく理論の統合に基づく、次世代の形式的手法に関する先見的な視点を推し進めている。
  論文  参考訳（メタデータ） (2026-02-02T22:39:02Z)
• Fundamentals of Building Autonomous LLM Agents [64.39018305018904]
  本稿では,大規模言語モデル(LLM)を用いたエージェントのアーキテクチャと実装手法について概説する。 この研究は、複雑なタスクを自動化し、人間の能力でパフォーマンスのギャップを埋めることのできる「アジェンティック」なLLMを開発するためのパターンを探求することを目的としている。
  論文  参考訳（メタデータ） (2025-10-10T10:32:39Z)
• 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)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• Igniting Language Intelligence: The Hitchhiker's Guide From Chain-of-Thought Reasoning to Language Agents [80.5213198675411]
  大規模言語モデル(LLM)は言語知能の分野を劇的に拡張した。 LLMは興味をそそるチェーン・オブ・シークレット(CoT)推論技術を活用し、答えを導き出す途中の中間ステップを定式化しなければならない。 最近の研究は、自律言語エージェントの開発を促進するためにCoT推論手法を拡張している。
  論文  参考訳（メタデータ） (2023-11-20T14:30:55Z)

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

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