AI-powered policy verification system that converts documents into formal Z3 logic for automated compliance checking.
This system automatically generates policies from documents, compiles them to formal Z3 constraints, and provides mathematically verified validation of user queries with mandatory variable handling.
Key Features:
- 📄 Document-to-Policy: Upload PDFs, generate policies automatically
- 🔧 Policy Editor: Edit variables (mandatory/optional), rules, constraints
- ⚡ Z3 Verification: Formal mathematical validation
- 🧠 Smart Variables: LLM-based variable extraction with defaults
- 📊 Comprehensive Testing: All edge cases covered
- Python 3.9+
- Docker and Docker Compose
- OpenAI API key
Option 1: Using Published Docker Image (Recommended)
git clone <repository>
cd automated_reasoning_check
# Create .env file from template
cp .env.example .env
# Edit .env and add your OpenAI API key
# Use published Docker image - edit docker-compose.yml:
# Uncomment: image: ishantkohar/anchor-backend
# Comment: image: anchor-backend
# Fix upload permissions
chmod 777 uploads
# Start services
docker-compose up -d
# API: http://localhost:9066/docs
# UI: Create test env and run streamlit
python -m venv test_env
source test_env/bin/activate
pip install -r requirements.txt
streamlit run streamlit_ui/app.pyOption 2: Build Locally
git clone <repository>
cd automated_reasoning_check
# Create .env file from template
cp .env.example .env
# Edit .env and add your OpenAI API key
# For GPT-5 users: Edit app/core/config.py and change reasoning_effort from "low" to "high" for better results
# Build local image (ensure docker-compose.yml uses: image: anchor-backend)
docker build --network=host -t anchor-backend .
# Fix upload permissions
chmod 777 uploads
# Start services
docker-compose up -d
# API: http://localhost:9066/docs
# UI: Create test env and run streamlit
python -m venv test_env
source test_env/bin/activate
pip install streamlit
streamlit run streamlit_ui/app.pypython -m venv test_env
source test_env/bin/activate
pip install -r requirements.txt
# Start OpenAI proxy (if needed)
python openai_proxy.py
# Run application
python -m uvicorn app.main:app --host 0.0.0.0 --port 9066 --reloadcurl -X POST "http://localhost:9066/api/v1/documents/upload" \
-F "file=@policy.pdf" -F "domain=hr"# Make variable mandatory
curl -X PATCH "http://localhost:9066/api/v1/policies/{id}/variables/{name}" \
-H "Content-Type: application/json" \
-d '{"is_mandatory": true, "default_value": null}'curl -X POST "http://localhost:9066/api/v1/policies/{id}/compile"curl -X POST "http://localhost:9066/api/v1/policies/{id}/verify" \
-H "Content-Type: application/json" \
-d '{
"question": "Can a full-time employee take 15 days leave?",
"answer": "Yes"
}'Document Upload → Policy Generation → Variable/Rule Editing → Z3 Compilation → Verification
- Document Processor: PDF/text parsing
- Policy Generator: LLM-based policy creation
- Variable Extractor: Smart variable extraction with mandatory/optional handling
- Rule Compiler: Convert rules to Z3 formal logic
- Verification Engine: Mathematical validation with explanations
automated_reasoning_check/
├── app/ # FastAPI application
│ ├── main.py # Application entry point
│ ├── api/ # REST API endpoints
│ │ ├── documents.py # Document upload & management
│ │ ├── policies.py # Policy CRUD operations
│ │ ├── compilation.py # Z3 compilation service
│ │ ├── verification.py # Policy verification
│ │ ├── clarifying_questions.py
│ │ ├── policy_validation.py
│ │ └── health.py # Health checks
│ ├── services/ # Core business logic
│ │ ├── document_processor.py
│ │ ├── policy_generator.py # LLM policy generation
│ │ ├── variable_extractor.py # Smart variable extraction
│ │ ├── rule_compiler.py # Z3 constraint compilation
│ │ ├── verification.py # Mathematical verification
│ │ ├── clarifying_questions.py
│ │ └── context_manager.py
│ ├── models/ # Data models
│ │ ├── database.py # SQLAlchemy models
│ │ └── schemas.py # Pydantic schemas
│ └── core/ # Configuration
│ ├── config.py # App configuration
│ └── database.py # Database setup
├── streamlit_ui/ # Interactive UI
│ └── app.py # Streamlit interface
├── tests/ # Test & debug scripts
│ ├── test_complete_system.py
│ ├── test_mandatory_variables.py
│ ├── test_policy_editing.py
│ ├── rule_compiler_implementation.py
│ └── debug_*.py
├── uploads/ # Document storage
├── test_env/ # Virtual environment
├── requirements.txt # Python dependencies
├── docker-compose.yml # Container orchestration
├── Dockerfile # Application container
├── openai_proxy.py # OpenAI API proxy
└── README.md
Transform your policy documents into intelligent, verifiable systems. The system takes PDF documents from the data/ folder and generates structured policies with formal validation logic.
data/hr_policy.pdf: Employee leave policies, vacation rules, approval workflowsdata/operations_policy.pdf: Equipment usage, safety protocols, authorization requirementsdata/legal_policy.pdf: Compliance rules, regulatory requirements, audit procedures
Each input document becomes a structured policy containing:
- Variables: Mandatory/optional fields (employee_type, requested_days, etc.)
- Rules: Formal Z3 logic conditions (
employee_type == "full_time" AND requested_days <= 10) - Validation Logic: Automatic compliance checking with detailed explanations
- Examples: Test scenarios with expected outcomes
{
"policy_name": "Employee Vacation Policy",
"variables": [
{
"name": "employee_type",
"type": "enum",
"possible_values": ["full_time", "part_time"],
"is_mandatory": true
}
],
"rules": [
{
"condition": "employee_type == 'full_time' AND requested_days <= 15",
"conclusion": "valid",
"description": "Full-time employees can take up to 15 days vacation"
}
]
}Screenshots and detailed examples coming soon - placeholder for visual demonstrations of the policy generation process.
Comprehensive Policy Validation System:
- ✅ Complete Variable Validation: Handles all mandatory variables → returns
valid - ✅ Smart Clarification Requests: Detects missing mandatory variables → requests
needs_clarification - ✅ Detailed Violation Explanations: Identifies policy violations → returns
invalidwith specific reasons - ✅ Intelligent Default Handling: Automatically applies default values for optional variables
- ✅ Complex Rule Processing: Supports nested conditions and multi-variable rule interactions
Input Query:
Question: "Can a full-time employee take 10 days vacation with 3 weeks notice?"
Answer: "Yes, the employee is full-time and provided adequate notice."
System Output:
{
"result": "valid",
"explanation": "✅ All policy rules are satisfied. The scenario is valid according to the policy."
}Input Query:
Question: "Can I take some vacation time?"
Answer: "I need time off for personal reasons."
System Output:
{
"result": "needs_clarification",
"explanation": "❓ Missing required information for: employee_type, requested_days",
"suggestions": ["What is your employment type (full-time/part-time)?", "How many days are you requesting?"]
}Input Query:
Question: "Can I take 20 days vacation tomorrow?"
Answer: "I need immediate time off."
System Output:
{
"result": "invalid",
"explanation": "❌ The scenario violates the following policy rules:\n\n• advance_notice_rule: Regular vacation needs 2+ weeks advance notice\n• duration_limit_rule: Maximum 15 consecutive days allowed"
}Interactive API documentation: http://localhost:9066/docs
Key Endpoints:
POST /api/v1/documents/upload- Upload policy documentsGET /api/v1/policies/- List all policiesPATCH /api/v1/policies/{id}/variables/{name}- Edit variablesPOST /api/v1/policies/{id}/compile- Compile policy to Z3POST /api/v1/policies/{id}/verify- Verify scenarios
- Never commit API keys or secrets to version control
- Use environment variables for all sensitive configuration
- Copy
.env.exampleto.envand configure your secrets there - Keep dependencies updated to get security patches
- Use strong database passwords in production environments
See SECURITY.md for detailed security guidelines.
Common Issues:
- Database connection → Check PostgreSQL container:
docker-compose logs postgres - Missing API key → Set
OPENAI_API_KEYin.env - Z3 installation → Verify:
python -c "import z3" - Upload directory not writable → Fix permissions:
chmod 777 uploads/or restart containers after creating uploads directory
Logs:
docker-compose logs # All services
docker-compose logs app # Application onlyWe welcome contributions! Please see CHANGELOG.md for version history.
This project is licensed under the MIT License - see the LICENSE file for details.