形式言語 – arXiv最新論文の紹介

MuSLR: Multimodal Symbolic Logical Reasoning

MuSLR: Multimodal Symbolic Logical Reasoning [133.9]
マルチモーダルな論理的推論は、自律運転や診断などの高度な応用において重要である。形式論理規則を基礎としたマルチモーダルな記号論理的推論のための最初のベンチマーク Mu SLR を導入する。我々は,GPT-4.1のChain-of-Thought性能を14.13%向上させるモジュール型フレームワークであるLogiCAMを提案する。
論文参考訳（メタデータ） (Tue, 30 Sep 2025 06:42:20 GMT)
Multimodal symbolic logical reasoningを対象とするベンチマークMuSLRの構築。またベースラインとしてモジュラー構成のLogiCAMを提案している。現在のフロンティアなモデルでも難しいベンチマークのよう。
改善のための「First, integrating dedicated symbolic modules is essential: the LogiCAM outperforms base VLMs precisely because it extracts multimodalities based on logic and embeds explicit symbolic reasoning steps. Second, existing VLMs struggle to align and fuse visual and textual information when performing formal logic; Future work should explore tighter multimodal integration, such as cross-modal architectures trained with logic-grounded objectives, to bridge this gap.」という指摘が興味深く、現行モデルは形式的な処理に苦労しているように見える。
リポジトリはMuSLR: Multimodal Symbolic Logical Reasoning

VerifyLLM: LLM-Based Pre-Execution Task Plan Verification for Robots [45.0]
本研究では,シミュレータや実環境で実行する前に,タスクプランを自動的に検証するアーキテクチャを提案する。このモジュールは、Large Language Modelsの推論機能を使用して、論理的一貫性を評価し、計画の潜在的なギャップを特定する。我々は,タスク計画の信頼性と効率の向上に寄与し,自律システムにおける堅牢な事前実行検証の必要性に対処する。
論文参考訳（メタデータ） (Mon, 07 Jul 2025 15:31:36 GMT)
タスク計画の検証のため「In this paper, we propose an architecture for automatically verifying high-level task plans before their execution in simulator or real-world environments. Leveraging Large Language Models (LLMs), our approach consists of two key steps: first, the conversion of natural language instructions into Linear Temporal Logic (LTL), followed by a comprehensive analysis of action sequences.」と形式言語を併用するアプローチの提案。
リポジトリはVerifyLLM: LLM-Based Pre-Execution Task Plan Verification for Robots

Formalizing UML State Machines for Automated Verification — A Survey [15.0]
モデリング言語(UML)は、動的システムのモデリングの標準である。本稿では、設計段階でモデルチェックを行う目的でUMLステートマシンセマンティクスの形式化に関する1997年から2021年までの既存の研究を包括的に調査する。
論文参考訳（メタデータ） (Wed, 24 Jul 2024 12:15:31 GMT)
UMLについて形式検証を軸に調査したサーベイ
本サーベイにも関係するがLLMを用いて自然言語で書かれた使用を形式言語に変換、形式検証に持ち込むようなアプローチは興味深いと思っている（研究はされている）

ProMoAI: Process Modeling with Generative AI [45.1]
ProMoAIは、LLM(Large Language Models)を利用して、テキスト記述からプロセスモデルを自動的に生成する新しいツールである。また、高度なプロンプトエンジニアリング、エラーハンドリング、コード生成技術も組み込まれている。
論文参考訳（メタデータ） (Thu, 7 Mar 2024 08:48:04 GMT)
LLMを使ったプロセスモデリング。計画作成がLLMでできる以上、実現できることに不思議はないが、Process Modelingのハードルが下がるのであれば面白いと思う。
リポジトリはProMoAI/app.py at main · humam-kourani/ProMoAI (github.com)。デモサイトもあるProMoAI · Streamlit。

Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents [42.4]
大規模言語モデル(LLM)により、AIエージェントは複雑なタスクを解決するためのマルチステッププランを自動的に生成し実行することができる。しかし、現在のLLMベースのエージェントは、しばしば無効または実行不可能な計画を生成する。本稿では,自然言語の表現性と形式言語の精度を統合することで,LLMをベースとしたエージェントのための新しいフォーマルLLM’フレームワークを提案する。
論文参考訳（メタデータ） (Sun, 4 Feb 2024 22:16:48 GMT)
LLMを用いたAIエージェントと形式言語の融合。「another important problem to explore in the future is LLM plan verification based on formal language.」と書かれている通り形式検証に持ち込めると面白いと思う。
リポジトリはagiresearch/Formal-LLM: Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents (github.com)

Structured Chain-of-Thought Prompting for Few-Shot Generation of Content-Grounded QA Conversations [13.1]
本稿では,構造化チェーン・オブ・シークレット (SCoT) を用いて,コンテントグラウンドによる質問応答会話を生成する手法を提案する。実験の結果,SCoTによる幻覚の緩和は,文書の接地に対するエージェント忠実度を最大16.8%向上させることがわかった。
論文参考訳（メタデータ） (Mon, 19 Feb 2024 01:49:53 GMT)
「At the core of our proposal is a structured breakdown of the complex task into a number of states in a state machine, so that actions corresponding to various subtasks, e g , content reading and utterance generation, can be executed in their own dedicated states.」
上記FormalLLMと組み合わさらないかなと思わなくもない。