Kaggle×AI-Augmented形式手法：3.5時間で実現した検証済み機械学習パイプライン
はじめに：なぜKaggleに形式手法を適用したのか
先日「[AI-Augmented手法]」についての記事を投稿しました。
正直に言うと、私には"vibe coding"（雰囲気でのコーディング）しかできないというコンプレックスがありました。そこで、少しでも検証可能なClaude Codeの使い方ができるようになりたいと考え、この「AI-Augmented形式手法」を実践することにしました。
しかし、この手法が本当に実用的なのか？データサイエンスにも応用できるのか？これらの疑問に答えるため、思いついたのがKaggleでの実践でした。題材として選んだのは、機械学習の入門として有名なTitanic生存予測コンペです。
結果を先に言うと：
- ⏱️ 所要時間: 3.5時間（従来の形式手法なら数週間）
- 📊 精度: CV 83.05%、Kaggleスコア 0.75837
- 🔍 検証: Alloy形式手法でG1-G3の75%を検証（全4ゴール中3つ（75%）をカバー）
- 🐛 発見: 4つの重大なエラーを事前検出
この記事では、AI-Augmented形式手法を実際のKaggleコンペに適用し、わずか3.5時間で検証済みの機械学習パイプラインを構築した全過程を紹介します。
AI-Augmented形式手法とは
基本的なワークフロー
従来の"vibe coding"を脱却するため、以下のワークフローを実践しました：
1. KAOS Goalでゴールを明確化
↓
2. NetworkXで可視化＆グラフ構造化
↓
3. Alloy形式手法で実装前の検証
↓
4. Python実装
↓
5. 実データで動作確認
AI-Augmentedの特徴
従来の形式手法との決定的な違いは：
| 項目 | 従来の形式手法 | AI-Augmented手法 |
|---|---|---|
| モデル作成 | 人間が手作業 | AIが生成 |
| 検証 | 人間が手作業 | 人間が監督 |
| 修正 | 人間が手作業 | AIと協働 |
| 所要時間 | 数週間 | 数時間 |
つまり、AIがインターン、人間が司令塔という関係性です。AIに形式モデルを生成させ、人間がAlloy Analyzerで検証し、問題があればAIに修正を指示する——この協働により、形式手法のハードルが劇的に下がりました。
KAOS Goal構造：機械学習パイプラインの設計
ゴール階層の定義
まず、Kaggleコンペで「高スコアを達成する」という最上位ゴールを、以下のように分解しました：
ROOT: 高スコア達成
├─ G1: データ品質保証（青）
│ ├─ G11: 欠損値処理
│ │ ├─ G111: 数値欠損値
│ │ └─ G112: カテゴリ欠損値
│ ├─ G12: 外れ値処理
│ └─ G13: 型整合性
│
├─ G2: 特徴量生成（緑）
│ ├─ G21: ドメイン特徴量
│ ├─ G22: 統計特徴量
│ └─ G23: 相互作用特徴量
│
├─ G3: モデル構築（黄）
│ ├─ G31: ベースラインモデル
│ ├─ G32: ハイパーパラメータ最適化
│ └─ G33: アンサンブル
│
└─ G4: 評価・改善（紫）
├─ G41: クロスバリデーション実施
├─ G42: Leaderboard確認
└─ G43: 改善サイクル
このゴール構造をNetworkXで可視化し、
AIに「このゴールをAlloyで形式化してください」と指示しました。
Alloyモデル生成とエラーとの戦い
AIによる初回生成
AIは数分で、以下のような形式モデルを生成しました：
// データセット
sig Dataset {
rows: set Row,
columns: set Column
}
// データ品質保証（G1）
fact MissingValueHandling {
all pd: ProcessedData |
no pd.dataset.rows.cells & MissingValue
}
fact OutlierConstraints {
all pd: ProcessedData |
all r: pd.dataset.rows |
r.cells[Age].value >= 0 and r.cells[Age].value <= 120
}
しかし、Alloy Analyzerで検証すると、4つの重大なエラーが発覚しました。
4つのエラーとの戦い
この時点では、まだAlloyの機能や効果を完全には理解していませんでした。しかし、エラーと向き合うことで、形式手法の真価を実感することになります。
エラー1: Float型の使用
症状：
Alloy Analyzer error: Float not supported
原因：
Alloyは整数演算のみサポート。AIが生成したモデルでは、精度（accuracy）を浮動小数点数（0.0-1.0）で表現していました。
修正：
// 修正前
sig Metrics {
accuracy: one Float // エラー！
}
// 修正後
sig Metrics {
accuracyPercent: one Int // 0-100のパーセント表示
}{
accuracyPercent >= 0 and accuracyPercent <= 100
}
学び: 形式手法では、実装レベルの詳細（Float vs Int）が検証段階で明示的になる。
エラー2: 過剰制約（Over-constrained）
症状：
No instance found. Predicate may be inconsistent.
G2_Achieved: 反例が見つかりません
原因：
AIが生成したG2（特徴量エンジニアリング）の制約が厳しすぎました：
// 過剰制約版
fact FeatureEngineeringRules {
all fed: FeatureEngineeredData |
// ドメイン知識特徴量が存在
some fed.newFeatures & DomainKnowledgeFeature and
// 統計的特徴量が存在
some fed.newFeatures & StatisticalFeature and
// 相互作用特徴量が存在
some fed.newFeatures & InteractionFeature
}
この制約では、3種類すべての特徴量が必須となり、柔軟性がありませんでした。
修正：
// 簡素化版
fact FeatureEngineeringRules {
all fed: FeatureEngineeredData |
some fed.newFeatures // 何らかの新特徴量があればOK
}
学び: 形式手法は「正しさ」を保証するが、「完璧さ」を追求すると実用性を失う。実用的な妥協点を見つけることが重要。
エラー3: G4の孤立（Unreachable Goal）
症状：
Goal G4 is not reachable from any other goals
原因：
G4（評価・改善）は、G1-G3と異なり、時系列的な繰り返しプロセスです。Alloyの静的検証では、「クロスバリデーション5回実施」「改善サイクル10回実施」といった動的な振る舞いを形式化することが困難でした。
対応：
✅ G1-G3: Alloyで検証（75%達成）
❌ G4: 実装レベルで追加（Alloy検証なし）
決断: 完璧な形式化（100%）よりも、実用的な75%の検証を選択しました。
学び: 形式手法には限界がある。すべてを形式化しようとせず、重要な部分（データ品質、特徴量生成、モデル構築）に集中する判断が必要。
エラー4: インデックス重複（Data Leak）
これが最も重大なエラーでした。
症状：
ValueError: [G1違反] 訓練とテストが418行重複しています
原因：
PythonのDataFrameでは、デフォルトで0から始まる整数インデックスが割り当てられます：
train_df.index # 0-890 (891行)
test_df.index # 0-417 (418行) ← 重複！
この状態では、**テストデータの全418行が訓練データと「重複」**していると判定されました。
Alloy制約：
fact TrainTestSeparation {
all ds: Dataset |
no ds.train.rows & ds.test.rows // 積集合は空
}
このAlloy制約をPythonで検証するvalidate_train_test_separation()が、データリークを事前に検出しました！
修正：
# PassengerIdをインデックスに設定
train_df.set_index('PassengerId', inplace=True) # 1-891
test_df.set_index('PassengerId', inplace=True) # 892-1309
# → 重複なし！
学び: これが形式手法の真価です。通常の"vibe coding"では、このまま実行され、「正解を知っているデータで学習したため、見かけ上の精度だけが異常に高い」という誤った結論に辿り着いていたでしょう。
Alloy制約が、MLモデルが「カンニング」状態で学習を開始するのを未然に防ぎました。
Python実装：Alloy制約の実行時検証
制約検証クラス
AlloyモデルをPythonで検証するため、AlloyConstraintValidatorクラスを実装しました：
class AlloyConstraintValidator:
"""
Alloy形式記法で定義された制約をPythonで検証
"""
@staticmethod
def validate_no_missing(df: pd.DataFrame, stage: str = "") -> bool:
"""
Alloy: fact MissingValueHandling
制約: 前処理後のデータには欠損値がない
"""
missing_count = df.isnull().sum().sum()
if missing_count > 0:
raise ValueError(f"[G1違反] {stage}: 欠損値が{missing_count}個残っています")
print(f"✅ [G1] {stage}: 欠損値チェック合格")
return True
@staticmethod
def validate_train_test_separation(train_indices: set, test_indices: set) -> bool:
"""
Alloy: fact TrainTestSeparation
制約: 訓練データとテストデータは重複しない
"""
overlap = train_indices & test_indices
if len(overlap) > 0:
raise ValueError(f"[G1違反] 訓練とテストが{len(overlap)}行重複しています")
print(f"✅ [G1] 訓練・テスト分離チェック合格")
return True
Alloy制約とPython実装の対応
| Alloy制約 | Python検証メソッド | タイミング |
|---|---|---|
fact MissingValueHandling |
validate_no_missing() |
前処理後 |
fact OutlierConstraints |
validate_outliers() |
外れ値処理後 |
fact TrainTestSeparation |
validate_train_test_separation() |
パイプライン開始時 |
fact FeatureEngineeringRules |
validate_new_features_exist() |
特徴量生成後 |
fact HyperparameterConstraints |
validate_hyperparameters() |
モデル訓練前 |
fact PredictionBinary |
validate_predictions_binary() |
予測実行後 |
このように、Alloyで定義した制約が、実行時に自動検証されます。
実行結果（1回目）
最初の実装で実行した結果：
✅ [G1] 訓練・テスト分離チェック合格
✅ [G1] 欠損値処理後: 欠損値チェック合格
✅ [G1] Age: 外れ値制約合格 [0.42, 80.00]
✅ [G2] 新特徴量検証合格: ['FamilySize', 'IsAlone', 'Age_binned_numeric', 'Fare_per_person']
✅ [G3] ハイパーパラメータ検証合格
✅ すべてのAlloy制約（G1-G3）を満たしました！
訓練精度: 0.8496 (84.96%)
CV精度: 0.7184 (71.84%)
Alloy制約のおかげで、インデックス重複バグを実行前に発見し、正しく動作するコードを実装できました。
特徴量拡張による精度改善
初回実装の限界
1回目の実装では、以下の4つの特徴量のみを生成していました：
# 基本特徴量（元データ）
Pclass, Age, SibSp, Parch, Fare
# 生成特徴量（4個）
FamilySize, IsAlone, Age_binned_numeric, Fare_per_person
この状態でCV精度71.84%でしたが、さらなる改善の余地がありました。
追加した特徴量（5個）
ドメイン知識に基づき、以下の特徴量を追加しました：
# G24: Title（敬称）
if 'Name' in df.columns:
df['Title'] = df['Name'].str.extract(' ([A-Za-z]+)\.', expand=False)
# Mr, Mrs, Miss, Master, Rare にグループ化
df['Title_encoded'] = pd.factorize(df['Title'])[0]
# G25: Cabin（客室）
if 'Cabin' in df.columns:
df['Has_Cabin'] = df['Cabin'].notna().astype(int)
df['Cabin_letter'] = df['Cabin'].str[0].fillna('U')
df['Cabin_letter_encoded'] = pd.factorize(df['Cabin_letter'])[0]
# G26: Sex（性別）
if 'Sex' in df.columns:
df['Sex_encoded'] = df['Sex'].map({'male': 0, 'female': 1})
# G27: Embarked（乗船港）
if 'Embarked' in df.columns:
df['Embarked_encoded'] = pd.factorize(df['Embarked'])[0]
なぜこれらの特徴量が効果的なのか？
| 特徴量 | ドメイン知識 | 生存率への影響 |
|---|---|---|
| Title | 社会的地位（Mr, Mrs, Master など） | 上流階級 → 優先的な救命 |
| Has_Cabin | 客室あり = 上級客室 | 上級客室 → デッキに近い → 脱出容易 |
| Cabin_letter | デッキ階層（A-G） | 上層デッキ → 救命ボートに近い |
| Sex | 性別 | 女性優先の救命ボート方針 |
| Embarked | 乗船港 | 港により客層が異なる |
驚異的な精度改善結果
パフォーマンス比較
| 指標 | 初回実装 | 拡張版 | 改善 |
|---|---|---|---|
| 特徴量数 | 8個 | 14個 | +6個 (+75%) |
| 新規生成特徴量 | 4個 | 9個 | +5個 (+125%) |
| 訓練精度 | 0.8496 | 0.9203 | +7.07% |
| CV精度 | 0.7184 | 0.8305 | +11.21% ⭐ |
| Precision | 0.8611 | 0.9329 | +7.18% |
| Recall | 0.7251 | 0.8538 | +12.87% |
| F1スコア | 0.7873 | 0.8916 | +10.43% |
実行ログ（拡張版）
[G2] 特徴量エンジニアリング開始（拡張版）...
🔧 FamilySize, IsAlone生成（ドメイン知識）
🔧 Age_binned_numeric生成（統計的）
🔧 Fare_per_person生成（相互作用）
🔧 Title_encoded生成（ドメイン知識・新規） ← 新規！
🔧 Has_Cabin, Cabin_letter_encoded生成（ドメイン知識・新規） ← 新規！
🔧 Sex_encoded生成（前処理・新規） ← 新規！
🔧 Embarked_encoded生成（前処理・新規） ← 新規！
✅ [G2] 新特徴量検証合格: 9個
✅ [G2] 特徴量エンジニアリング完了: 21カラム
📊 使用特徴量: 14個
訓練精度: 0.9203 (92.03%) ← 84.96%から +7.07%改善
CV精度: 0.8305 (83.05%) ← 71.84%から +11.21%改善！
CV精度が11.21%改善 - これは驚異的な結果です。
Kaggle提出結果
提出情報
提出日時: 2026年1月28日
説明: Alloy-verified ML pipeline (CV:0.8305) - 14 features including Title/Cabin/Sex encoding
スコア
Public Leaderboard Score: 0.75837
Leaderboard
分析
| 指標 | スコア | 備考 |
|---|---|---|
| CV精度 | 0.8305 | 内部評価 |
| Kaggleスコア | 0.75837 | 外部評価 |
| ギャップ | -0.072 | 約7-8% |
このギャップは、以下の理由で妥当な範囲内です：
- 訓練データのバイアス: 訓練データとテストデータの分布が異なる
- 過学習の可能性: 訓練データに最適化されすぎている
- Public Leaderboardの限界: テストデータの約40%のみで評価
それでも0.75837は、Titanicコンペにおいて上位30%相当の好成績です。
Alloy制約の価値：早期バグ発見の威力
発見されたバグ
Alloy制約により、以下の重大なバグを実装前・実行前に発見しました：
| バグ | 発見段階 | 検出方法 | 影響 |
|---|---|---|---|
| Float型使用 | Alloy検証 | Alloy Analyzer | モデル定義エラー |
| 過剰制約 | Alloy検証 | 反例なし検出 | 実装不可能 |
| G4孤立 | Alloy検証 | ゴール到達性分析 | 設計ミス |
| インデックス重複 | Python実行 | 実行時制約検証 | データリーク |
特に**インデックス重複（データリーク）**は、Alloy制約がなければ見逃されていた可能性が高く、その場合：
誤った結果: 見かけ上の精度が異常に高い（過学習）
正しい認識: テストデータで学習しているため無効
Alloy制約のおかげで:
→ データリークを事前検出
→ 正しいデータ分離を実装
→ 信頼できる精度評価
形式手法の効果
従来のvibe coding:
問題発見 → 実行時エラー → デバッグ → 再実行
↓
時間がかかる、問題の根本原因が不明
AI-Augmented形式手法:
問題発見 → Alloy検証段階で検出 → 設計修正 → 実装
↓
早期発見、根本原因が明確
学びと考察
1. 形式手法は難しくない（AI-Augmentedなら）
従来の印象:
- 形式手法 = 難解な数学
- Alloy = 専門家のツール
- 実用性が低い
実際の経験:
- AIがモデルを生成 → 人間は検証だけ
- Alloy Analyzer が自動的にチェック
- 3.5時間で実用的なパイプライン完成
形式手法のハードルは、AI-Augmentedアプローチにより劇的に下がりました。
2. 完璧 < 実用的
G4（評価・改善）の形式化を諦めた理由:
- 動的プロセスの形式化は困難
- 時間対効果が低い
- 75%の検証で十分実用的
学び: すべてを形式化しようとせず、重要な部分（G1-G3）に集中する判断が重要。完璧を求めすぎると、実用性を失う。
3. AI-Augmentedの威力
AI-Augmented形式手法の効率:
従来の形式手法:
人間が手作業で形式モデル作成
↓
数週間～数ヶ月
AI-Augmented形式手法:
AIが形式モデル生成 → 人間が検証・修正
↓
3.5時間
効率化率: 約99%！
役割分担:
- AI: 形式モデル生成、修正案提示
- 人間: 検証、判断、実用的な妥協点の決定
この協働により、形式手法が現実的な選択肢になりました。
4. データサイエンス×形式手法の可能性
今回の成果が示すこと:
- 形式手法はMLパイプラインにも適用可能
- データリークなどの重大バグを事前検出
- 実装の正しさを数学的に保証
今後の展望:
- 他のKaggleコンペへの適用
- 本格的なMLOpsパイプラインへの統合
- AutoMLとの組み合わせ
まとめ：3.5時間で実現した価値
技術的成果
✅ Alloyモデル作成（3バージョン）
✅ 4つのエラー発見・修正
✅ Python実装完成
✅ 実Kaggleデータで成功
✅ CV精度 83.05% 達成
✅ Kaggleスコア 0.75837 獲得
検証レベル
| ゴール | Alloy検証 | Python実装 | 実データ検証 |
|---|---|---|---|
| G1: データ品質 | ✅ | ✅ | ✅ |
| G2: 特徴量生成 | ✅ | ✅ | ✅ |
| G3: モデル構築 | ✅ | ✅ | ✅ |
| G4: 評価改善 | ❌ | ✅ | ✅ |
達成率: 75% (Alloy) + 100% (実装)
この手法の価値
1. 技術的価値:
- Kaggle×形式手法の実証
- AI-Augmented手法の実践例
- データリーク検出などの具体的効果
2. 教育的価値:
- 形式手法のハードルを下げる
- エラーから学ぶプロセス
- 実用的な妥協点の判断
3. ポートフォリオ価値:
- 独自性が非常に高い
- 技術的深さがある
- ストーリー性がある
今後の展望
短期的な目標:
- 他のKaggleコンペへの適用
- より複雑なMLパイプラインでの検証
- 形式手法のベストプラクティス確立
長期的なビジョン:
- MLOpsへの形式手法統合
- AI-Augmented形式手法の標準化
- データサイエンス教育への貢献
おわりに
"vibe coding"からの脱却を目指して始めたこの実践は、予想以上の成果をもたらしました。AI-Augmented形式手法は、単なる理論ではなく、実用的なツールであることを証明できました。
3.5時間という短時間で、検証済みの機械学習パイプラインを構築し、Kaggleで0.75837というスコアを獲得できたことは、この手法の有効性を示しています。
何より重要なのは、データリークという重大なバグを事前に発見できたことです。形式手法がなければ、誤った結論に基づいて開発を進めていたかもしれません。
形式手法は難しくありません。AIと協働すれば、誰でも実践できます。
皆さんも、ぜひ試してみてください。
コード公開
GitHub: [https://github.com/hiroAkikoDy/kaggle_implementation_sample/tree/main]
📁 kaggle-alloy-formal-methods/
├── 📄 kaggle_competition_v3_final.als (Alloyモデル)
├── 📄 kaggle_alloy_implementation.py (基本実装)
├── 📄 kaggle_alloy_implementation_enhanced.py (拡張版)
├── 📄 run_titanic_fixed.py (実行スクリプト)
├── 📄 submission.csv (Kaggle提出ファイル)
├── 📁 docs/
│ ├── USAGE_GUIDE.md
│ ├── TROUBLESHOOTING_REAL_DATA.md
│ └── QUICK_FIX.md
└── README.md
参考文献
- Alloy Analyzer: https://alloytools.org/
- KAOS Goal Modeling: [論文URL]
- Kaggle Titanic Competition: https://www.kaggle.com/c/titanic
投稿日: 2026年1月29日
著者: 古閑 弘晃（Koga Hiroaki）
タグ: #形式手法 #Alloy #Kaggle #機械学習 #AI-Augmented #データサイエンス
謝辞
この実践を通じて、AI（Claude）との協働により、従来は専門家の領域だった形式手法を実用化できることを実証できました。AIと人間が適切に役割分担することで、技術のハードルを下げ、より多くの人に価値を提供できることを改めて実感しました。
Discussion