<<<<<<< HEAD

InvariantAI

=======

InvariantAI

🛡️ Invariant AI — Constraint-Aware Risk Prediction with Formal Verification

A trustworthy ML system that combines machine learning with Lean 4 formal verification to ensure every prediction is safe, valid, and mathematically guaranteed.

---

📌 Table of Contents

• Project Overview
• Problem Statement
• Solution Architecture
• Formal Specification
• Lean 4 Integration & Correctness Guarantees
• ML Pipeline
• Constraint Validation & Rule Engine
• Real-World Relevance
• System Flow
• Tech Stack
• Getting Started
• Example Output
• Creativity: Applying Lean in Autonomy
• Future Work
• Team

---

📖 Project Overview

Invariant AI is a constraint-aware risk prediction system that solves a critical gap in modern AI: ML models can produce statistically plausible but logically invalid outputs.

This system wraps a standard ML risk scorer with:

1. Domain constraint validation — rule-based checks that catch invalid predictions before they propagate
2. Lean 4 formal verification — mathematical proof that every returned prediction satisfies defined invariants (e.g., 0 ≤ risk ≤ 1)
3. Automatic correction — invalid predictions are corrected and re-verified, not silently passed through

The result is a pipeline where every output comes with a formal proof of correctness — transforming a black-box model into a trustworthy, auditable AI system.

---

❗ Problem Statement

Standard ML pipelines have no mechanism to guarantee that outputs satisfy domain constraints:

• A risk model might return risk = 1.4 — mathematically impossible in a [0, 1] bounded score
• A model might assign high risk to inputs with logically impossible combinations of flags
• There is no way to prove a prediction is valid — only to test it on samples

In high-stakes domains (healthcare, finance, autonomous systems), this is not acceptable.

Invariant AI solves this by making correctness a first-class output — not an afterthought.

---

🏗️ Solution Architecture

User Input (age, risk_flags, ...)
│
▼
┌──────────────────────┐
│ ML Risk Scorer │ ← Trained model generates raw risk score
└──────────┬───────────┘
│
▼
┌──────────────────────┐
│ Constraint Engine │ ← Rule-based validation & auto-correction
│ (Domain Rules) │ enforces: 0 ≤ risk ≤ 1, flag consistency, etc.
└──────────┬───────────┘
│
▼
┌──────────────────────┐
│ Lean 4 Verifier │ ← Formal proof that prediction satisfies invariants
│ (Formal Proofs) │ returns: verified_score + proof object
└──────────┬───────────┘
│
▼
✅ Verified Prediction + Formal Proof Certificate

---

🔬 Lean 4 Integration & Correctness Guarantees

Why Lean 4?

Lean 4 is a dependently-typed theorem prover and programming language. Unlike runtime assertions, Lean proofs are:

• Static — verified at compile time, not at runtime
• Compositional — complex invariants built from simpler proven lemmas
• Machine-checkable — the Lean kernel independently checks every proof

🧩 What I Have Implemented

🏗️ Solution Architecture

 ┌────────────────────────────┐
│ User Input │
│ (age, risk flag, etc.) │
└────────────┬──────────────┘
│
▼
┌────────────────────────────┐
│ ML Risk Model │
│ (Logistic Regression) │
│ → raw risk score (p) │
└────────────┬──────────────┘
│
▼
┌────────────────────────────┐
│ Constraint Validator │
│ - Check 0 ≤ p ≤ 1 │
│ - Check flag rules │
└────────────┬──────────────┘
│
(if violation detected)
│
▼
┌────────────────────────────┐
│ Correction Engine │
│ - Adjust risk value │
│ - Enforce domain rules │
└────────────┬──────────────┘
│
▼
┌────────────────────────────┐
│ Lean 4 Verifier │
│ Formal Proof Generation │
│ (0 ≤ p ≤ 1 is proven) │
└────────────┬──────────────┘
│
▼
┌────────────────────────────┐
│ Final Verified Output │
│ - Risk Score │
│ - Validation Status │
│ - Proof Certificate │
└────────────────────────────┘

🔍 Key Components

• ML Model → Generates initial prediction (may be imperfect)
• Validator → Detects logical inconsistencies
• Correction Layer → Fixes invalid outputs instead of rejecting
• Lean Verifier → Ensures mathematical correctness
• Final Output → Fully validated + provable result

---

🤖 1. Machine Learning Pipeline

• Built a risk prediction model using Python (scikit-learn / boosting models)
• Uses features like:
  • age
  • risk flags (critical, chronic, history)
• Produces a raw risk score from the model

---

Input Features

Feature	Type	Description
age	Integer	Age of the individual
flag	Binary (0/1)	High-risk indicator

Model

• Algorithm: Logistic Regression
• Output: Probability score in [0, 1]

fromsklearn.linear_modelimportLogisticRegressionmodel=LogisticRegression()
model.fit(X_train, y_train)
risk=model.predict_proba(X_input)[:, 1][0]
------### ✅ Constraint Engine```markdownThesystemenforceslogicalconstraintsonpredictions:
```pythondefcorrect_prediction(age, risk, flag):
ifage>60andrisk<0.2:
risk=0.2ifflag==1andrisk<0.5:
risk=0.5returnmax(0, min(risk, 1))
## ⚙️ Constraint Validation & Rule EngineTheconstraintenginesitsbetweentheMLmodelandtheLeanverifier. It:
1.**Validates**therawscoreagainstalldomaininvariants2.**Corrects**violationsusingdomain-awarelogic (notclipping)
3.**Logs**everycorrectionforauditability## 🌍 Real-World Relevance### Where This Matters|Domain|RiskWithoutInvariantAI|WithInvariantAI||--------|--------------------------|-------------------||**Healthcare**|Modeloutputs`risk = 1.3` → patientovertreated|Proofthatscore ∈ [0,1] beforeclinicaluse||**Finance**|Creditriskscoreviolatesregulatorybounds|FormallyverifiedcompliancewithBaselIIIconstraints||**AutonomousVehicles**|Safetyclassifieroutputsinconsistentwithsensorflags|Leanproofofconsistencybeforeactuation||**Insurance**|Premiumcalculationviolatesactuarialinvariants|Audit-readyproofcertificateperprediction|### Regulatory Alignment-**EUAIAct (2024)**: Emphasizestransparencyandreliability — thissystemimprovestrustviavalidationandproof-**FDASaMDGuidelines**: Supportsboundedandpredictableoutputs-**ISO26262 (Automotive)**: Alignswiththeideaofverifyingsafety-criticaloutputs## 🔄 System Flow1.Usersubmitsinput → {age: 67, flag: 1}
2.MLModelgeneratesrawscore → 0.323.ConstraintEnginechecks:
✗ flag=1butscore=0.32<0.5 → CORRECTION → score=0.50
✓ 0 ≤ 0.50 ≤ 1 → PASS4.LeanVerifierreceivesscore=0.50:
theorem: 0 ≤ 0.50 ∧ 0.50 ≤ 1 → PROVED ✅
5.Responsereturned:
{
"risk": 0.50,
"valid": true,
"corrected": true,
"proof": "✔ Lean Proof: 0.50 satisfies 0 ≤ p ≤ 1"
}

---

🛠️ Tech Stack

🛠️ Tech Stack

Layer	Technology
ML Model	Python, scikit-learn (Logistic Regression)
Constraint Engine	Python (custom rules)
Formal Verifier	Lean 4
UI	Streamlit
Integration	Python ↔ Lean subprocess

---

🚀 Getting Started

Prerequisites

# Install Lean 4
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Install Python dependencies
pip3 install -r requirements.txt

Run the System

# Start the API
uvicorn main:app --reload
# Example request
curl -X POST http://localhost:8000/predict \
-H "Content-Type: application/json" \
-d '{"age": 67, "flag_critical": true, "flag_chronic": false}'

Run Lean Verification Tests

cd lean/
lake build
lake test

---

📊 Example Output

cd invariantai lake env lean --run Invariantai/Check.lean 70

✔ Example output:

✔ Lean Proof: 0.7 satisfies 0 ≤ p ≤ 1

📊 Example Output

{
"risk": 0.50,
"valid": true,
"corrected": true,
"message": "Constraint applied",
"proof": "✔ Proof: 0.50 satisfies 0 ≤ p ≤ 1"
}

---

💡 Creativity: Applying Lean in Autonomy

Most ML systems treat formal verification as a post-hoc audit tool. Invariant AI treats it as a live gatekeeper.

Key creative contributions:

• Proof-as-output: The system doesn't just predict — it produces a proof certificate alongside every result. This is a new paradigm for ML APIs.
• Constraint-aware correction: Instead of rejecting invalid predictions (which breaks pipelines), the system corrects them and re-verifies — making it robust in production.
• Lean as a runtime component: Lean is invoked in the request/response loop, not just at test time. This is an unusual and powerful application of a theorem prover.
• Composable invariants: Complex domain rules are broken into simple Lean lemmas that compose — this mirrors how formal methods work in safety-critical hardware design, now applied to AI.

---

🔮 Future Work

• End-to-end Lean proof — eliminate the Python/Lean bridge and run the full pipeline in Lean 4 natively
• Proof caching — cache proofs for repeated input patterns to reduce latency
• LLM-assisted spec generation — use an LLM to auto-generate Lean invariants from natural language domain descriptions
• Multi-model ensemble verification — verify that ensemble disagreements don't violate consistency invariants
• Dashboard — real-time monitoring of correction rates, proof success rates, and invariant violation frequency

---

👥 Team

Name	Role
Priyashree Panda	ML Engineer + Lean Verifier

---

📄 License

MIT License — see LICENSE for details.

---

"A prediction without a proof is just a guess. Invariant AI makes every guess provable."

---

📜 Origin

This project was built during the LeanLang for Verified Autonomy Hackathon (April 17–18 + online through May 1, 2026) at the Indian Institute of Science (IISc), Bangalore.

The goal of the hackathon was to explore how formal methods (Lean 4) can be integrated with real-world systems to improve reliability, safety, and trust in AI.

Invariant AI was developed as a practical system combining:

• Machine Learning (risk prediction)
• Constraint validation (domain rules)
• Lean 4 formal verification (proof of correctness)

---

🙏 Acknowledgments

This project was made possible by:

• Emergence AI — Hackathon sponsor
• Emergence India Labs — Event organizer and research direction
• Indian Institute of Science (IISc), Bangalore — Academic partner, mentorship, and technical guidance

---

🔗 Links

• Hackathon Page: https://east.emergence.ai/hackathon-april2026.html
• Emergence India Labs: https://east.emergence.ai
• Emergence AI: https://www.emergence.ai

---

🌟 Project Significance

This project demonstrates a new paradigm:

👉 AI systems that don’t just predict — but prove their correctness

By integrating Lean 4 into the ML pipeline, this system ensures:

• Predictions are always within valid bounds
• Logical constraints are enforced
• Outputs are accompanied by formal proofs

This approach moves AI systems closer to being:

• Trustworthy
• Auditable
• Safe for real-world deployment

---

🚀 Built for Verified AI Systems of the Future