Ph.D. Candidate at JAIST

Seungil Yang

Formal Relational Verification for Privacy, Utility, and AI Governance

I study how privacy disclosure, utility preservation, and governance constraints can be modeled and verified before deployment using relational logic, model checking, and system-level reasoning.

My research program frames privacy as relational reachability and utility as meaningful distinguishability, revealing structural incompatibilities between the two through formal verification.

Relational Privacy Utility Verification Pareto Cliff Formal Verification AI Governance LLM / RAG Privacy Alloy / Model Checking

View Publications Research Program Contact

About

I am a Ph.D. candidate at JAIST working on Relational Privacy — a research program that studies privacy, utility, and governance through formal relational verification.

My work models identity disclosure as a reachability problem over data transformations, attacker inference, and system interactions.

More recently, I extend this framework toward LLM and RAG systems, where disclosure may emerge through interactions among retrieval, memory, external knowledge, and generation.

Research Axes

Relational Privacy

Privacy as relational reachability across transformations and inference processes.

Utility Verification

Utility as preservation of meaningful distinguishability between records.

AI Governance

Governance-aware verification for privacy, disclosure, and compliance constraints.

LLM / RAG Systems

Compositional privacy analysis for retrieval, generation, memory, and contextual interactions.

Research Program

ABZ 2026

Accepted · Springer LNCS

Establishes privacy as relational reachability using Alloy-based formal verification.

JISA Extension

In Preparation

Extends relational privacy toward utility verification through meaningful distinguishability and Pareto Cliff analysis.

Ph.D. Thesis

Ongoing Research Program

Integrates privacy, utility, and governance-aware verification into a unified relational framework.

AIME 2027

Planned Validation Study

Empirical validation of Pareto Cliff phenomena using real-world clinical and healthcare datasets.

Future Directions

Long-term Research Vision

Extending relational verification toward trustworthy AI, RAG privacy, and governance-aware AI systems.

Research Interests

My research aims to establish formal foundations for privacy, utility, and governance in data-driven systems.

Rather than treating privacy as statistical masking, I study privacy as a structural property of systems: whether identifiable states become reachable through transformations and inference.

This perspective enables design-time verification of disclosure risks and provides a rigorous alternative to purely heuristic or empirical approaches.

Methodology

I use Alloy and relational logic to formally model data transformations, attacker assumptions, utility constraints, and system interactions.

By composing de-identification transformations with re-identification relations, I verify whether disclosure is logically reachable.

My recent work introduces:

Utility as meaningful distinguishability
AssumptionSpec vs AttackerContract separation
Pareto Cliff as structural incompatibility
Governance-aware verification

Education

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

Mar 2023 – Present · Expected Sep 2026 · Transdisciplinary Sciences / Information Science

Research on formal relational verification of privacy, utility, and governance in data and AI systems.

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

Apr 2020 – Feb 2023 · Transdisciplinary Sciences / Information Science

Studied formal methods, model checking, and information science.

M.Div. — Biola University

Jun 2012 – May 2018 · La Mirada, California, USA · Intercultural Studies

Graduate-level study in intercultural studies and multicultural education.

JAIST 박사과정

양승일

프라이버시, 유용성, AI 거버넌스를 위한 관계적 형식 검증

저는 관계 논리, 모델 체킹, 시스템 수준 추론을 바탕으로, 프라이버시 유출, 유용성 보존, 거버넌스 제약이 시스템 배포 이전 단계에서 어떻게 검증될 수 있는지를 연구하고 있습니다.

저의 연구는 프라이버시를 관계적 도달 가능성 (relational reachability), 유용성을 의미 있는 구별 가능성 (meaningful distinguishability) 으로 정의하며, 두 요소 사이의 구조적 충돌을 형식 검증을 통해 분석하는 것을 목표로 합니다.

Relational Privacy Utility Verification Pareto Cliff Formal Verification AI Governance LLM / RAG Privacy Alloy / Model Checking

논문 보기 연구 흐름 연락하기

소개

저는 JAIST 박사과정에 재학 중이며, Relational Privacy 라는 연구 방향 아래 프라이버시, 유용성, 거버넌스를 관계적 형식 검증을 통해 연구하고 있습니다.

제 연구는 데이터 변환, 공격자 추론, 시스템 상호작용을 통해 개인정보 유출이 어떻게 발생 가능한지를 관계적 도달 가능성 문제로 모델링합니다.

최근에는 이러한 프레임워크를 LLM 및 RAG 시스템으로 확장하고 있으며, retrieval, memory, external knowledge, generation 간 상호작용에서 발생하는 새로운 disclosure path를 연구하고 있습니다.

연구 축

Relational Privacy

데이터 변환과 추론 과정에서의 관계적 도달 가능성으로 프라이버시를 정의합니다.

Utility Verification

의미 있는 구별 가능성의 보존을 유용성으로 정의합니다.

AI Governance

거버넌스와 disclosure 제약을 형식적으로 검증합니다.

LLM / RAG Systems

검색, 생성, 메모리, 문맥 상호작용에 대한 조합적 프라이버시 분석을 연구합니다.

연구 흐름

ABZ 2026

Accepted · Springer LNCS

Establishes privacy as relational reachability using Alloy-based formal verification.

JISA Extension

In Preparation

Extends relational privacy toward utility verification through meaningful distinguishability and Pareto Cliff analysis.

Ph.D. Thesis

Ongoing Research Program

Integrates privacy, utility, and governance-aware verification into a unified relational framework.

AIME 2027

Planned Validation Study

Empirical validation of Pareto Cliff phenomena using real-world clinical and healthcare datasets.

Future Directions

Long-term Research Vision

Extending relational verification toward trustworthy AI, RAG privacy, and governance-aware AI systems.

연구 관심

저의 연구는 데이터 기반 시스템에서의 프라이버시, 유용성, 거버넌스를 위한 형식적 토대를 구축하는 것을 목표로 합니다.

저는 프라이버시를 단순한 통계적 masking이 아니라, 데이터 변환과 추론 과정을 통해 식별 가능한 상태가 도달 가능한지 여부라는 구조적 속성으로 바라봅니다.

이러한 관점은 시스템 배포 이전 단계에서 disclosure risk를 검증 가능하게 하며, 단순 경험적 접근을 넘어서는 논리적 보증을 제공합니다.

방법론

저는 Alloy와 관계 논리를 사용하여 데이터 변환, 공격자 가정, 유용성 제약, 시스템 상호작용을 형식적으로 모델링합니다.

비식별화 변환과 재식별 관계를 조합하여, 개인정보 유출이 논리적으로 도달 가능한지를 검증합니다.

최근 연구에서는 다음 개념들을 제안하고 있습니다:

유용성 = meaningful distinguishability
AssumptionSpec vs AttackerContract 분리
Pareto Cliff = 구조적 불가능성
Governance-aware verification

학력

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

2023년 3월 – 현재 · 2026년 9월 졸업 예정 · 융합과학 / 정보과학

데이터 및 AI 시스템에서의 프라이버시, 유용성, 거버넌스를 위한 관계적 형식 검증을 연구하고 있습니다.

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

2020년 4월 – 2023년 2월 · 융합과학 / 정보과학

형식기법, 모델 체킹, 정보과학을 중심으로 연구했습니다.

M.Div. — Biola University

2012년 6월 – 2018년 5월 · 미국 캘리포니아 La Mirada · Intercultural Studies

Graduate-level study in intercultural studies and multicultural education.

JAIST 博士後期課程

ヤン・スンイル

プライバシー・有用性・AIガバナンスのための関係的形式検証

私は、関係論理、モデル検査、システムレベル推論を用いて、プライバシー漏えい、有用性保存、ガバナンス制約がシステム公開前にどのように検証可能かを研究しています。

現在の研究では、プライバシーを relational reachability （関係的到達可能性）として、有用性を meaningful distinguishability （意味的区別可能性）として定式化し、両者の構造的衝突を形式的に分析することを目指しています。

Relational Privacy Utility Verification Pareto Cliff Formal Verification AI Governance LLM / RAG Privacy Alloy / Model Checking

論文を見る研究ロードマップ連絡する

概要

私はJAIST博士後期課程に所属し、 Relational Privacy という研究方向のもとで、プライバシー、有用性、ガバナンスを関係的形式検証によって研究しています。

私の研究は、データ変換、攻撃者推論、システム相互作用によって、個人情報漏えいがどのように発生可能かを、関係的到達可能性問題としてモデル化します。

最近では、この枠組みを LLMおよびRAGシステムへ拡張し、 retrieval、 memory、 external knowledge、 generation の相互作用から生じる新しい disclosure path を研究しています。

研究軸

Relational Privacy

データ変換と推論過程における関係的到達可能性としてプライバシーを定義します。

Utility Verification

意味的区別可能性の保存を有用性として定義します。

AI Governance

ガバナンスおよび disclosure 制約を形式的に検証します。

LLM / RAG Systems

検索、生成、メモリ、文脈相互作用に対する compositional privacy analysis を研究します。

研究ロードマップ

ABZ 2026

Accepted · Springer LNCS

Establishes privacy as relational reachability using Alloy-based formal verification.

JISA Extension

In Preparation

Extends relational privacy toward utility verification through meaningful distinguishability and Pareto Cliff analysis.

Ph.D. Thesis

Ongoing Research Program

Integrates privacy, utility, and governance-aware verification into a unified relational framework.

AIME 2027

Planned Validation Study

Empirical validation of Pareto Cliff phenomena using real-world clinical and healthcare datasets.

Future Directions

Long-term Research Vision

Extending relational verification toward trustworthy AI, RAG privacy, and governance-aware AI systems.

研究関心

私の研究は、データ駆動型システムにおけるプライバシー、有用性、ガバナンスのための形式的基盤を構築することを目的としています。

私はプライバシーを、単なる統計的 masking としてではなく、データ変換および推論過程を通じて、識別可能状態へ到達できるかどうかという構造的性質として捉えています。

この観点により、システム公開前に disclosure risk を検証可能にし、単なる経験的評価を超えた論理的保証を提供します。

方法論

Alloy と関係論理を用いて、データ変換、攻撃者仮定、 utility constraints、システム相互作用を形式的にモデル化します。

非識別化変換と再識別関係を組み合わせることで、個人情報漏えいが論理的に到達可能かどうかを検証します。

最近の研究では、以下の概念を提案しています。

Utility = meaningful distinguishability
AssumptionSpec と AttackerContract の分離
Pareto Cliff = structural impossibility
Governance-aware verification

学歴

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

2023年3月 – 現在 · 2026年9月修了予定 · 融合科学 / 情報科学

データおよびAIシステムにおけるプライバシー・有用性・ガバナンスのための関係的形式検証を研究しています。

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

2020年4月 – 2023年2月 · 融合科学 / 情報科学

形式手法、モデル検査、情報科学を中心に研究しました。

M.Div. — Biola University

2012年6月 – 2018年5月 · La Mirada, California, USA · Intercultural Studies

異文化研究および多文化教育学を中心とした大学院課程を修了しました。