論文の概要: Faithful Autoformalization of Natural Language Assertions
- arxiv url: http://arxiv.org/abs/2607.13303v2
- Date: Thu, 16 Jul 2026 21:38:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-20 13:50:44.29549
- Title: Faithful Autoformalization of Natural Language Assertions
- Title（参考訳）: 自然言語挿入の忠実な自己形式化
- Abstract要約: Monty: アサーションのための自動形式化フレームワークを紹介します。
本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。
提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
- 参考スコア（独自算出の注目度）: 2.8921494813790094
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.
- Abstract（参考訳）: ソフトウェアテストと検証には形式的な契約が不可欠ですが、それらを書くことは労働集約的であり、エラーを起こします。
自然言語仕様から実行可能なアサーションを合成し、非公式な開発者意図と形式的な実行可能な仕様とのギャップを埋める。
自然言語におけるアサーションの妥当性とあいまいさの期待の課題に対処するアサーションのための自動形式化フレームワークであるMontyを提示する。
提案手法は,新しい適合度スコアと,形式化されたアサーションに対するコードテストから得られた妥当性スコアを用いて,形式化をフィルタリングすることに基づいている。
我々は,22のコレクション型Javaクラスから派生した541個のアサーション生成タスクに対するアプローチを評価し,LLMを用いてアサーションを経時的に翻訳する場合よりも,より信頼性の高い(平均20ポイントの精度向上)基盤真理を生成することを示す。
関連論文リスト
- Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
論文 参考訳（メタデータ） (2026-06-30T00:27:53Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - Neuroforger: certified violation witnesses for smart contracts verification via LLMs [0.0]
近年の大規模言語モデル(LLM)では、スマートコントラクトが特定のプロパティを尊重するかどうかを予測できる推論機能が組み込まれている。
抽象型でSolidityを拡張する新しい形式仕様言語を導入する。
LLMと型チェックと具体的な実行を組み合わせたワークフローを設計し、違反証人を生成し検証する。
論文 参考訳（メタデータ） (2026-05-29T14:54:51Z) - 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) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Do What? Teaching Vision-Language-Action Models to Reject the Impossible [53.40183895299108]
VLA(Vision-Language-Action)モデルは、さまざまなロボットタスクにおいて強力なパフォーマンスを示している。
Instruct-Verify-and-Act(IVA)を提案する。
実験の結果,IVAはベースラインよりも97.56%の精度で虚偽の前提検出精度を向上させることがわかった。
論文 参考訳（メタデータ） (2025-08-22T10:54:33Z) - 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) - Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。
QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
論文 参考訳（メタデータ） (2024-10-09T22:53:48Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。
まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。
ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z) - SAGA: Summarization-Guided Assert Statement Generation [34.51502565985728]
本稿では,アサート文の自動生成のための新しい要約誘導手法を提案する。
我々は、事前訓練された言語モデルを参照アーキテクチャとして利用し、アサート文生成のタスクでそれを微調整する。
論文 参考訳（メタデータ） (2023-05-24T07:03:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。