論文の概要: Validating Autoformalized Specifications via Contrapuntal Languages

• arxiv url: http://arxiv.org/abs/2610.30059v1
• Date: Wed, 21 Oct 2026 17:19:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-23 09:50:43.262947
• Title: Validating Autoformalized Specifications via Contrapuntal Languages
• Title（参考訳）: 並行言語による自動仕様の検証
• Abstract要約: 本稿では,サンプル種子仕様の断片を基本仕様言語上での合成糖として再利用する合成アルゴリズムを提案する。 GPT-5.4 mini と Qwen3.6-Flash を用いて,HumanEval+ と LiveCodeBench で検討を行った。
• 参考スコア（独自算出の注目度）: 5.88947114030542
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications can make AI-generated code mechanically checkable. Because user intent is typically expressed in natural language rather than formal logic, specifications must first be derived from it, e.g., via LLM-based autoformalization. Yet autoformalized specifications are themselves untrusted, so a key challenge is validating whether they capture user intent without relying on a costly oracle such as human review. In this oracle-free setting, a natural strategy is to vote among model outputs, but because model errors are often correlated, agreement among outputs may reflect shared mistakes rather than correctness. Our key insight is that these errors can be decorrelated through representational diversity. We achieve this diversity with contrapuntal languages: pairs of task-specific formal languages, each designed to express the intended specification, yet admitting no structure-preserving translation between them. An LLM formalizes the intent independently in each language, and we accept a specification only if a solver proves the two formalizations equivalent. To construct such languages, we present a synthesis algorithm that reuses fragments of sampled seed specifications as syntactic sugar over a base specification language. We implement the approach for first-order logic specifications and evaluate it on HumanEval+ and LiveCodeBench using GPT-5.4 mini and Qwen3.6-Flash with and without thinking. Over the strongest baseline, our method increases the proportion of accepted specifications that are correct, i.e., complete and sound, by 12.0% on HumanEval+ and 42.9% on LiveCodeBench. The accepted specifications judged complete reject 98.6% of buggy program variants on HumanEval+ and 96.2% on LiveCodeBench, compared with 92.8% and 78.3% for the strongest baseline.
• Abstract（参考訳）: 正式な仕様は、AI生成したコードを機械的にチェックできるようにする。 ユーザインテントは通常、形式論理ではなく自然言語で表現されるため、仕様はLLMベースのオートフォーマル化を通じて、まずそれから導出されなければならない。 しかし、自己形式化された仕様自体が信頼できないため、重要な課題は、人間のレビューのような高価なオラクルに頼ることなく、ユーザの意図を捉えているかどうかを検証することである。 このオラクルフリーな環境では、自然な戦略はモデル出力間で投票することであるが、モデルエラーはしばしば相関しているため、アウトプット間の合意は正確さよりも共有ミスを反映する可能性がある。 私たちのキーとなる洞察は、これらのエラーは表現の多様性によって非相関化できるということです。 タスク固有の形式言語ペアは、それぞれが意図した仕様を表現するように設計されていますが、それらの間の構造保存翻訳は認めていません。 LLMは各言語で独立に意図を定式化し、解決者が2つの形式化を同等に証明した場合のみ仕様を受理する。 このような言語を構築するために,サンプルシード仕様の断片を基本仕様言語上の構文糖として再利用する合成アルゴリズムを提案する。 我々は,GPT-5.4 mini と Qwen3.6-Flash を用いて,一階述語論理仕様のアプローチを実装し,HumanEval+ と LiveCodeBench で検討した。 最強のベースラインでは,HumanEval+では12.0%,LiveCodeBenchでは42.9%,完全および音の許容仕様の割合が増加する。 承認された仕様では、HumanEval+で98.6%、LiveCodeBenchで96.2%、最強のベースラインで92.8%、78.3%が完全に拒否された。

関連論文リスト

• SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications [28.546702829415207]
  自然言語命令を機械解釈可能な形式仕様に変換することで、ロボットと自律システムは、その動作を計画し、推論し、正式に検証することができる。 既存の翻訳モデルは、通常、結果が信頼できないり、ユーザの意図を捉えなかったりしても、すべての入力に対して仕様を生成する。 選択的共形予測に着想を得て,形式仕様を生成するだけでなく,いつ信頼できるかを判断する選択翻訳フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-08-05T22:17:09Z)
• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  Monty: アサーションのための自動形式化フレームワークを紹介します。 本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。 提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
  論文  参考訳（メタデータ） (2026-07-14T22:12:14Z)
• Weave of Formal Thought [51.56484100374058]
  WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。 本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。 Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
  論文  参考訳（メタデータ） (2026-06-24T15:58:11Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• Synthesizing Precise Protocol Specs from Natural Language for Effective Test Generation [42.582977261473324]
  AutoSPECは平均92.8%のクライアントと80.2%のサーバメッセージタイプを回復し、81.5%のメッセージ受信を現実世界のシステムで行う。 プロトタイプは, 広く用いられている5種類のアプローチの実現可能性を示した。 インターネットベースのプロトコル。
  論文  参考訳（メタデータ） (2025-11-22T08:39:52Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)
• Reducing language context confusion for end-to-end code-switching automatic speech recognition [50.89821865949395]
  本稿では,E2E符号スイッチングASRモデルの多言語コンテキストの混同を低減するための言語関連アテンション機構を提案する。 複数の言語のそれぞれの注意を計算することにより、豊かな単言語データから言語知識を効率的に伝達することができる。
  論文  参考訳（メタデータ） (2022-01-28T14:39:29Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  原文から第一パス文法仕様を抽出する自動フレームワークを開発する。 我々は、世界の多くの言語の文法の中核にあるモルフォシンタクティックな現象である合意を記述する規則の抽出に焦点をあてる。 我々のフレームワークはUniversal Dependenciesプロジェクトに含まれるすべての言語に適用され、有望な結果が得られます。
  論文  参考訳（メタデータ） (2020-10-02T18:31:45Z)

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

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