論文の概要: Towards Autoformalization of LLM-generated Outputs for Requirement Verification

• arxiv url: http://arxiv.org/abs/2511.11829v1
• Date: Fri, 14 Nov 2025 19:45:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-18 14:36:23.330441
• Title: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• Title（参考訳）: 要件検証のためのLCM生成出力の自動形式化に向けて
• Authors: Mihir Gupte, Ramesh S,
• Abstract要約: 非公式な文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデルの出現により、新たな関心を集めている。 本稿では,LLMをベースとした簡易なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証する。 この結果から, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が有意な可能性を示唆した。
• 参考スコア（独自算出の注目度）: 0.6015898117103068
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models (LLMs). While LLMs show promise in generating structured outputs from natural language (NL), such as Gherkin Scenarios from NL feature requirements, there's currently no formal method to verify if these outputs are accurate. This paper takes a preliminary step toward addressing this gap by exploring the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements. We conducted two distinct experiments. In the first one, the autoformalizer successfully identified that two differently-worded NL requirements were logically equivalent, demonstrating the pipeline's potential for consistency checks. In the second, the autoformalizer was used to identify a logical inconsistency between a given NL requirement and an LLM-generated output, highlighting its utility as a formal verification tool. Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs, laying a crucial foundation for future, more extensive studies into this novel application.
• Abstract（参考訳）: フォーマルな文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデル(LLM)の出現により、新たな関心を集めている。 LLMは、NLの機能要件からGherkin Scenariosのような自然言語(NL)から構造化アウトプットを生成することを約束しているが、これらのアウトプットが正確かどうかを検証するための正式な方法はない。 本稿では,LLMをベースとした単純なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証することにより,このギャップに対処するための予備的なステップについて述べる。 私たちは2つの異なる実験を行った。 最初の1つでは、オートフォーマライザは、2つの異なるワードのNL要件が論理的に等価であることを認識し、パイプラインの一貫性チェックの可能性を示した。 第二に、オートフォーマライザは与えられたNL要求とLLM出力との論理的矛盾を識別するために用いられ、形式的検証ツールとしての有用性を強調した。 本研究は, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が重要な可能性を持っていることを示唆するものである。

関連論文リスト

• Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing [0.0]
  大規模言語モデル(LLM)は、自動形式化のための強力なツールとして登場した。 最近の研究により、LLMはパラフレーズ自然言語(NL)入力に敏感であることが判明した。 意味論的に類似したNL文を持つ形式的証明を生成するLLMのロバスト性を評価する。
  論文  参考訳（メタデータ） (2025-11-16T21:25:59Z)
• Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations [13.485604499678262]
  自然言語推論(NLI)における自然言語説明の役割 近年の研究では、大言語モデル(LLM)と定理証明器(TP)の相互作用が、NLI説明の有効性の検証と改善に役立つことが示されている。 本稿では,自己形式化時の意味喪失を軽減するための戦略について検討する。
  論文  参考訳（メタデータ） (2025-05-30T06:38:39Z)
• RuAG: Learned-rule-augmented Generation for Large Language Models [62.64389390179651]
  本稿では,大量のオフラインデータを解釈可能な一階述語論理規則に自動抽出する新しいフレームワーク,RuAGを提案する。 我々は,自然言語処理,時系列,意思決定,産業タスクなど,公共および民間の産業タスクに関する枠組みを評価する。
  論文  参考訳（メタデータ） (2024-11-04T00:01:34Z)
• Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving [13.485604499678262]
  本稿では,Large Language Models(LLMs)とTheorem Provers(TPs)の統合による自然言語説明の検証と改善について検討する。 本稿では, TPとLPMを統合して説明文の生成と定式化を行う, Explanation-Refiner というニューロシンボリック・フレームワークを提案する。 代わりに、TPは説明の論理的妥当性を公式に保証し、その後の改善のためのフィードバックを生成するために使用される。
  論文  参考訳（メタデータ） (2024-05-02T15:20:01Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• FaithLM: Towards Faithful Explanations for Large Language Models [60.45183469474916]
  大規模言語モデルの忠実度を評価し改善するモデルに依存しないフレームワークであるFaithLMを紹介した。 FaithLMは一貫して忠実度を高め、強い自己説明ベースラインよりも人間の合理性に整合した説明を生成する。
  論文  参考訳（メタデータ） (2024-02-07T09:09:14Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)

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

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