Gen-AX、リアルタイム音声AIの形式手法研究が国際会議「IEEE TALE」に採択

CATEGORY: テクノロジー

Gen-AX株式会社は、リアルタイム音声AIの開発現場にLLM支援型の形式手法を適用した研究論文が、IEEE Education Societyの国際会議「IEEE TALE 2026」にShort Paperとして採択されたことを発表しました。

本論文は、形式手法を専門としないエンジニアがリアルタイム音声AIの再設計において、システムの振る舞いを定義し、LLMが形式化を支援するアプローチを実践した過程を報告したものです。2026年12月2日～4日にタイ・パタヤで開催される同会議にて発表が予定されています。

研究の背景とLLM支援型形式手法の活用

リアルタイム音声AIシステムでは、発話の割り込みや外部APIからの遅延イベント、Function Callの処理結果など、複数の並行・非同期処理が発生します。こうした通常のテストでは確認が難しい複雑な状態の組み合わせに対し、同社は2026年春から、商用リアルタイム音声AIのオーケストレーター再設計において形式手法を活用してきました。

開発現場では、システムが満たすべき「安全性」と「活性」を検証するため、LLMを用いてTLA+／PlusCalによるモデル記述やモデルチェッカー「TLC」の利用を支援しました。これにより、専門外のエンジニアがLLMの支援を受けながら形式手法を習得し、実践していくプロセスを職場学習の観点からまとめています。

約1.8億の到達可能状態を探索した検証結果

研究では、リアルタイム音声AIオーケストレーターの通話状態や音声再生、AI応答などの要素を35個の状態変数としてモデル化しました。

安全性の検証においては24個の不変条件を設定し、モデル修正を経て最終的に21個の不変条件について、検証範囲内となる181,364,514個（約1.8億）の到達可能状態で成立することを確認しました。また、活性の検証でも43,952,071個の異なる状態を探索し、「終了処理が最終的に完了する」といった設定した4つの性質すべてが成立することを確認しています。

人間によるレビューを前提としたプロダクト改善への還元

今回の取り組みでは、LLMが生成したモデルをそのまま受け入れるのではなく、人間によるコードとの双方向レビューを実施しました。3回の独立したLLMセッションを通じて割り込み処理やFunction Callなどに関する5件の差異を検出し、モデルの修正や実装上の課題特定、レビューによる棄却などの判断を行っています。

得られた反例をもとに実装上のガード条件の解除タイミングを修正したほか、検証条件をコードの型構造へ反映して不適切な状態を防ぐ設計変更を行うなど、研究成果を実際のプロダクト開発へ還元しています。

採択された論文の概要

採択された論文の詳細は以下の通りです。

• 論文タイトル: 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

発表された論文は、出版手続きを経て論文データベース「IEEE Xplore」へ収録される予定です。

Gen-AX株式会社の概要

• 社名: Gen-AX株式会社
• 所在地: 東京都港区海岸1-7-1
• 代表者: 代表取締役社長 CEO 砂金信一郎
• 事業内容: 生成AI、自律型AIを活用したSaaS事業および専門コンサルティングサービスの提供
• 株主: ソフトバンク株式会社 100%
• 公式サイト: https://www.gen-ax.co.jp/

本記事はGen-AX株式会社の発表をもとに作成しました。