論文の概要: Cost-Driven Synthesis of Sound Abstract Interpreters

• arxiv url: http://arxiv.org/abs/2511.13663v1
• Date: Mon, 17 Nov 2025 18:16:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-18 18:52:09.66907
• Title: Cost-Driven Synthesis of Sound Abstract Interpreters
• Title（参考訳）: 音響抽象解釈器のコスト駆動合成
• Authors: Qiuhan Gu, Avaljot Singh, Gagandeep Singh,
• Abstract要約: 我々は,現代のLLMが,音や非自明な抽象的インタプリタを合成することで,この負担を軽減することができるかどうかを検討する。 我々は,LLMベースの生成を統語的・意味的検証と定量的なコスト誘導フィードバック機構で統合する統合フレームワークを開発した。
• 参考スコア（独自算出の注目度）: 8.132068058484505
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Constructing abstract interpreters that provide global soundness guarantees remains a major obstacle in abstract interpretation. We investigate whether modern LLMs can reduce this burden by leveraging them to synthesize sound, non-trivial abstract interpreters across multiple abstract domains in the setting of neural network verification. We formulate synthesis as a constrained optimization problem and introduce a novel mathematically grounded cost function for measuring unsoundness under strict syntactic and semantic constraints. Based on this formulation, we develop a unified framework that unifies LLM-based generation with syntactic and semantic validation and a quantitative cost-guided feedback mechanism. Empirical results demonstrate that our framework not only matches the quality of handcrafted transformers, but more importantly, discovers sound, high-precision transformers for complex nonlinear operators that are absent from existing literature.
• Abstract（参考訳）: グローバルな音質保証を提供する抽象的解釈を構成することは、抽象的解釈において大きな障害である。 ニューラルネットワーク検証の設定において,複数の抽象領域にまたがる音響的,非自明な抽象的インタプリタを合成することで,現代のLLMがこの負担を軽減することができるかどうかを検討する。 制約付き最適化問題として合成を定式化し、厳密な構文的・意味的制約の下で不協和性を測定するための数学的基礎的なコスト関数を導入する。 この定式化に基づいて,LLMベースの生成を統語的・意味的検証と定量的なコスト誘導フィードバック機構で統合する統合フレームワークを開発した。 実験結果から,本フレームワークは手作り変圧器の品質に適合するだけでなく,既存の文献にはない複素非線形演算子に対して,音質,高精度な変圧器を発見することが示唆された。

関連論文リスト

• LLMSynthor: Macro-Aligned Micro-Records Synthesis with Large Language Models [20.767947974005168]
  LLM Synthorは、ターゲットのマクロ統計と一致した現実的なマイクロレコードを生成するマクロ認識シミュレータである。 合成データセットを反復的に構築し、合成アグリゲーションとターゲットアグリゲーションの差を最小限に抑える。 強力な現実主義、統計的忠実さ、実用性を実現し、経済学、社会科学、都市研究に広く応用されている。
  論文  参考訳（メタデータ） (2025-05-20T13:35:38Z)
• Provably Transformers Harness Multi-Concept Word Semantics for Efficient In-Context Learning [53.685764040547625]
  トランスフォーマーベースの大規模言語モデル(LLM)は、卓越した創造力と出現能力を示している。 この研究は、トランスフォーマーが単語のマルチコンセプトセマンティクスをどのように活用し、強力なICLと優れたアウト・オブ・ディストリビューションICL能力を実現するかを示すための数学的解析を提供する。
  論文  参考訳（メタデータ） (2024-11-04T15:54:32Z)
• Adapting LLMs for Efficient Context Processing through Soft Prompt Compression [1.1550486371582305]
  本稿では,大規模言語モデルを合理化された文脈処理のために戦略的に調整する,革新的なフレームワークを提案する。 我々の手法はSoftPromptCompと呼ばれ、動的に生成されたソフトプロンプトで自然言語をアマルガメイトし、簡潔でセマンティックに頑健な文脈の描写をフォージする。 我々は,我々のフレームワークが計算オーバーヘッドを著しく減らし,LLMの有効性を様々なベンチマークで向上させることを実証した。
  論文  参考訳（メタデータ） (2024-04-07T15:44:20Z)
• Multi-Fact Correction in Abstractive Text Summarization [98.27031108197944]
  Span-Factは、質問応答モデルから学んだ知識を活用して、スパン選択によるシステム生成サマリーの補正を行う2つの事実補正モデルのスイートである。 我々のモデルは、ソースコードのセマンティック一貫性を確保するために、反復的または自動回帰的にエンティティを置き換えるために、シングルまたはマルチマスキング戦略を採用している。 実験の結果,自動測定と人的評価の両面において,要約品質を犠牲にすることなく,システム生成要約の事実整合性を大幅に向上させることができた。
  論文  参考訳（メタデータ） (2020-10-06T02:51:02Z)

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

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