Gen-AX、リアルタイム音声AIの約1.8億状態を探索・検証する実践研究が「IEEE TALE 2026」に採択

～ 人間が『システムはどう振る舞うべきか』を定義し、LLMが形式化を支援するリアルタイム音声AIの開発・検証手法を国際会議で発表 ～

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　2026年10月6日
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　Gen-AX株式会社

生成AI・自律型AI（人工知能）を活用したSaaSプロダクトの開発・提供と、企業のAX（AIトランスフォーメーション）を支援するコンサルティングサービスの提供を手がけるGen-AX株式会社（ジェナックス、以下「Gen-AX」）は、リアルタイム音声AIの開発現場にLLM（大規模言語モデル）支援型の形式手法を適用した研究論文が、IEEE Education Societyの国際会議「IEEE TALE 2026」にShort Paperとして採択されたことをお知らせします。

本論文は、形式手法を専門としないエンジニアが、リアルタイム音声AIの再設計において、人間が「システムはどう振る舞うべきか」を定義し、LLMがその形式化を支援するアプローチを実践した過程を報告したものです。LLMの支援によって、エンジニアが「守るべき性質を定め、反例を見極める」といった本質的な判断に向き合いやすくなる可能性を示唆しており、本取り組みは現在も継続しています。

本論文は、2026年12月2日～4日にタイ・パタヤで開催される「IEEE TALE 2026（International Conference on Teaching, Assessment, and Learning for Engineers）」にて発表予定です。同会議は、IEEE Education Societyがアジア太平洋地域で展開する主要な国際会議シリーズで、工学・テクノロジー・STEM（科学・技術・工学・数学）教育などに関する研究者、教育関係者、産業界の実務家らが参加します。

■研究の背景 ― リアルタイム音声AIの「複雑な状態」をどう検証するか

Gen-AXでは、2026年春から、商用リアルタイム音声AIのオーケストレーター（音声AIに関わる複数の処理やイベントを連携・制御する仕組み）の再設計において、LLM支援型の形式手法の活用に取り組んできました。本研究は、実際のプロダクト開発で直面した課題と、開発現場で蓄積してきた実践知をもとに、その取り組みを研究成果としてまとめたものです。

リアルタイム音声AIは、一見すると「人が話し、AIが応答する」というシンプルな仕組みに見えます。しかし実際のシステムでは、ユーザーによる発話の割り込み、外部のAPI（Application Programming Interface）から遅れて届くイベント、Function Call（AIが外部の機能やシステムを呼び出す仕組み）の処理結果、システム側からのプロンプト追加など、複数の処理が並行して発生します。

例えば、AIが回答を生成・再生している途中でユーザーが発話し、その一方で別の処理結果やイベントが到着するといった、複雑な状態の組み合わせが生じます。こうした並行・非同期処理では、通常のテストだけでは確認が難しいタイミングの組み合わせについても考慮する必要があります。

今回の研究では、システムが満たすべき「安全性（Safety：起きてはいけないことが起きないこと）」と「活性（Liveness：起きるべきことが最終的に起きること）」を明示し、それらが成立するかをモデル上で探索する形式手法（Formal Methods：システムの仕様や振る舞いを数学的・論理的に記述し、検証する手法）を活用しました。 

さらに、形式手法を専門としないエンジニアが実際の開発現場で活用できるよう、LLMを用いて、TLA+／PlusCal（システムの状態や振る舞いを形式的に記述するための言語・記法）によるモデル記述や、TLC（TLA+で記述したモデルを検証するモデルチェッカー）の利用を支援しました。

 本論文は、この検証そのものに加えて、形式手法を専門としないエンジニアがLLMの支援を受けながら形式手法を身につけていく過程を、職場での学びとしてまとめたものです。

■設定した検証範囲で、約1.8億の到達可能状態を探索

研究では、リアルタイム音声AIオーケストレーターの通話状態、音声再生、AIの応答、Function Call、データの一時保持、割り込みなどを35個の状態変数としてモデル化しました。再設計の過程では、約9.8万状態を探索する検証などを重ね、その後、より広い範囲を対象に約1.8億状態を探索するモデルへと検証範囲を広げました。
安全性の検証では、24個の不変条件（Invariant：システムが常に満たすべき条件）を設定しました。モデルと実装のコードを照合したところ、モデルに抜けていた処理が1件と、仕様として許されている動作まで禁じていた条件が3件見つかりました。たとえば、ある条件は、先のFunction Callが続いている間に新しい応答を求めることを禁じていましたが、この重なりは仕様として許されています。モデルを修正し、この3件の条件を除いたうえで検証した結果、残る21個の不変条件はすべて、設定した検証範囲内の181,364,514個（約1.8億）の到達可能状態（モデル上で起こり得る状態）で成立し、反例（設定した条件が成立しないことを示す具体的な状態や遷移）がないことを確認しました。

また活性の検証では、43,952,071個の異なる状態を探索し、「終了処理が最終的に完了する」「受信したイベントが最終的に処理される」など、設定した4つの性質すべてについて成立することを確認しました。

■LLMを「答えを出す存在」ではなく、エンジニアの思考を支援する存在として活用

今回の研究の特徴の一つが、LLMによって生成されたモデルを無条件に正しいものとはせず、人間によるレビューを前提としている点です。

LLMが生成したモデルと実装コードを、
「モデルからコードを確認する」
「コードからモデルを確認する」
という双方向から照合するレビューを実施しました。
3回の独立したLLMセッションでは、割り込み処理、Function Call、終了処理に関して5件の差異を検出。そのうち3件ではモデルを修正し、1件は実装上の課題として報告、残る1件は実装内容と一致しないとしてエンジニアのレビューによって棄却されました。

また、実際の開発では、反例をもとに、実装上のガード条件（特定の処理や状態遷移を許可するための条件）の解除のタイミングの問題を特定して修正したほか、検証によって確認した条件をコードの型構造へ反映し、本来起きてはならない状態そのものをプログラム上で作れない設計へ変更する取り組みにもつながりました。

こうした一連の取り組みを通じて、研究や検証を研究活動だけで完結させるのではなく、実際のプロダクト設計や実装改善へ還元していることも、本研究の特徴です。

■論文概要

論文タイトル
LLM-Assisted Formal Methods as Workplace Learning: A Threshold-Concept Experience Report from Real-Time Voice-AI Orchestration
（参考訳：職場学習としてのLLM支援型形式手法 ― リアルタイム音声AIオーケストレーションにおける閾概念の経験報告）

著者
Kazuki Matsuda、Yuka Ezura、Mitsuru Takeda（Gen-AX Corp.）

採択区分
Short Paper

本論文では、リアルタイム音声AIの技術検証に加えて、形式手法を専門としないエンジニアがLLMの支援を受けながら、システムの状態や「守るべき条件」を定義し、反例を読み解いて実装へ反映していく過程を、実際の開発現場における学習・実践の観点から分析しています。記法やツールの操作をLLMが支援することで、エンジニアが「システムは本来どう振る舞うべきか」を考えることにどう集中できたか、という学びの過程です。
IEEE TALE 2026のShort Paperは、進行中の研究やパイロットを対象とする論文カテゴリーです。本論文は、完結した研究の結果ではなく、Gen-AXの開発の現場で今も続いている取り組みを、進行中の段階で報告するもので、ほかのエンジニアへの展開は始めており、学習の効果の客観的な評価は今後の課題としています。

同会議では投稿論文に3人のレビューアーによる二重匿名査読プロセスが設けられており、採択・発表された論文は、最終原稿の提出や著作権手続きなどの出版手続きを経て、IEEE Xplore（IEEEが運営する論文データベース）への収録となります。

■Gen-AX CTO 木田祐介のコメント

AIエージェントを実社会で使い続けていくためには、AIモデルそのものの性能だけでなく、複数の処理やイベントが重なる状況でも、システム全体が意図した通りに振る舞うことを、設計と検証で示す必要があります。AIが高度化するほど、人間の役割がなくなるのではなく、「AIやシステムに何をさせるべきか」を定義し、検証する人間の責任がより重要になります。今回の研究は、その責任をリアルタイム音声AIの開発現場でどう果たしてきたかの記録であり、そこで得られた知見は、実際のコードや型設計の改善へ戻しています。今後も、AIを「動かす」だけでなく、安心して業務を「任せられる」存在へ進化させるため、研究と社会実装を往復しながら技術開発を進めていきます。

■IEEE TALE 2026について

「IEEE TALE（International Conference on Teaching, Assessment, and Learning for Engineers）」は、IEEE Education Societyがアジア太平洋地域で展開する国際会議シリーズです。工学、テクノロジー、STEM（科学・技術・工学・数学）教育をはじめ、デジタル技術を活用した教育・学習・評価に関する研究や実践知が共有されます。

14回目の開催となる IEEE TALE 2026は、2026年12月2日～4日にタイ・パタヤで開催されます。2026年のテーマは「AI-Augmented Learning: Redefining the Future of Engineering & Technology Education」です。

IEEE TALE 2026公式サイト
https://tale-conference.org/2026

■今後の展望

Gen-AXでは、自律型AIオペレーター「X-Ghost」をはじめとするAIエージェントを、実際の業務で継続的に活用できるプロダクトとして社会実装するため、AIモデルそのものの性能だけに頼らず、その周辺を支えるシステムの設計、評価、品質・信頼性の向上と、それを担う人の学びに関する研究開発に取り組んでいます。

 今回の研究の対象は、社内のソフトウェアエンジニアでした。今後は、ソフトウェア開発を専門としない業務担当者にも対象を広げ、業務の中にある条件の分かれ目や状態の移り変わりを捉える力を、AIの支援のもとでどう育てられるかを研究していきます。こうした、業務担当者自身が業務の仕組みを設計・改善していく考え方は、従来から「エンドユーザー開発」として研究されてきました。Gen-AXでは、こうした知見も踏まえながら、顧客企業自身によるAIオペレーターの応対設計・改善の内製化を支えていきます。

今後も、実際のプロダクト開発で得られた課題を研究へつなげ、その成果を再びプロダクトへ還元するサイクルを通じて、企業が安心してAIに業務を任せられる環境の実現を目指します。

■Gen-AX 会社概要