Introduction to Askalot¶
Askalot is an AI-powered survey platform with mathematical validation, designed to eliminate the cognitive overhead of maintaining logical coherence in complex questionnaires. The platform combines domain-specific language design with formal verification to ensure survey quality.
Platform Overview¶
Askalot consists of four integrated services, each handling a distinct phase of the survey lifecycle:
Armiger - Questionnaire Design¶
AI-assisted questionnaire authoring with SMT-based validation
Armiger provides a browser-based development environment for creating questionnaires using QML (Questionnaire Markup Language). The service features:
- AI-powered generation: Let AI create questionnaires from requirements while QML handles logical consistency
- Real-time validation: SMT solver checks for logical contradictions as you type
- Syntax highlighting: Full QML language support with auto-completion
- Mathematical verification: Automatic reachability, consistency, and cycle detection
Armiger orchestrates multiple code-server instances, providing each user with a dedicated VS Code environment pre-configured for QML development.
SirWay - Survey Execution¶
Lazy-evaluation survey engine with dynamic form generation
SirWay executes validated questionnaires with respondents. The platform features:
- Lazy evaluation: Questions are evaluated on-demand based on current state
- Dynamic flow control: Conditional branching without pre-computing all paths
- Contradiction-free: Mathematical guarantees prevent impossible situations
- Flow visualization: Interactive Mermaid diagrams show survey paths
SirWay ensures that respondents never encounter logically inconsistent questions or dead ends, using the formal semantics defined in QML.
Targetor - Campaign Management¶
Audience targeting and campaign orchestration
Targetor manages survey distribution and tracks campaign progress. The service features:
- User database import: Load respondent lists from external sources
- Demographic targeting: Select audiences based on demographic factors
- Campaign tracking: Monitor completion rates and response quality
- Launch management: Schedule and control survey deployment
Targetor enables representative sampling by targeting specific demographic profiles, ensuring survey results accurately reflect the intended population.
Balansor - Statistical Analysis¶
Data correction and export
Balansor processes collected survey responses for analysis. The service features:
- Response rebalancing: Adjust weights to correct sampling bias
- Post-stratification: Align sample demographics with population parameters
- Data cleaning: Identify and handle inconsistencies
- Multi-format export: Output to CSV, SPSS, R, and other formats
Balansor ensures that survey results are statistically representative and ready for analysis.
QML: Domain-Specific Language for Surveys¶
QML (Questionnaire Markup Language) is a YAML-based language specifically designed for AI-assisted questionnaire creation. The language design philosophy:
AI-Friendly Design¶
QML was designed with AI code generation in mind:
- Declarative syntax: Describe what questions to ask, not how to manage control flow
- Mathematical semantics: All logic expressed as first-order formulas suitable for SMT solving
- Validation separation: AI generates content; SMT solver ensures logical coherence
- Cognitive offloading: Survey designers focus on questions, not dependency management
This separation of concerns allows AI to generate complex questionnaires without the cognitive burden of simultaneously:
- Generating semantically meaningful questions
- Tracking conditional dependencies between questions
- Ensuring logical consistency across all paths
- Maintaining correct question ordering and flow
- Avoiding contradictions and unreachable dead ends
Mathematical Foundation¶
QML questionnaires are backed by rigorous mathematical foundations:
Formal semantics: Every questionnaire is a mathematical object with well-defined properties
- Items have preconditions and postconditions - Boolean predicates determining when questions are asked and what answers are valid
- All outcomes are integers or integer vectors/matrices
- Logical consistency is verified using Z3 SMT solver
Automated validation: The system automatically checks:
- Reachability: Can every question be reached?
- Consistency: Are validation rules satisfiable?
- Acyclicity: Do dependencies form cycles?
- Global satisfiability: Does at least one valid completion path exist?
These checks happen automatically during questionnaire design, catching logical errors before deployment.
See: Questionnaire Analysis for mathematical details.
How It Works Together¶
The four services form an integrated workflow:
graph LR
A[Armiger<br/>Design with AI] --> B[Targetor<br/>Build Campaign]
B --> C[SirWay<br/>Execute Survey]
C --> D[Balansor<br/>Analyze Results]
style A fill:#e1f5ff
style B fill:#fff4e1
style C fill:#e8f5e9
style D fill:#f3e5f5- Design in Armiger: AI generates QML questionnaire, SMT validates logical consistency
- Campaign in Targetor: Import target audience, configure demographic parameters
- Execute in SirWay: Respondents complete surveys with guaranteed logical coherence
- Analyze in Balansor: Rebalance responses, correct sampling bias, export results
Key Benefits¶
For Survey Designers¶
- AI assistance: Generate questionnaires from natural language descriptions
- Error prevention: Mathematical validation catches logical flaws automatically
- No manual dependency tracking: System handles question order and conditional logic
- Confidence: Know that deployed surveys are logically sound
For Respondents¶
- Smooth experience: Never encounter contradictory questions
- Relevant questions: Only see questions that apply to their situation
- No dead ends: Guaranteed to complete surveys that are reachable
- Dynamic adaptation: Survey adapts based on previous answers
For Analysts¶
- Quality data: Logical validation ensures response consistency
- Representative samples: Targetor enables demographic balancing
- Statistical correction: Balansor adjusts for sampling bias
- Standard formats: Export to familiar analysis tools
Formal Verification in Practice¶
Traditional survey platforms require designers to manually ensure:
- Questions appear in the correct order
- Conditional logic doesn't create contradictions
- All questions are reachable
- Validation rules are mutually consistent
Askalot automates all of this through mathematical verification. Here's a simple questionnaire example:
flowchart TD
q_age["q_age: What is your age?"]
q_consent["q_consent: Do you consent to participate?"]
q_children["q_children: How many children do you have?"]
q_household["q_household: How many people live in your household?"]
q_end["q_end: Thank you for participating!"]
q_age e1@==> q_consent
q_consent e2@==> q_household
q_household e3@==> q_children
q_children e4@==> q_end
%% BEGIN_PRECONDITIONS
q_consent ---- q_consent_precond_0(["q_age.outcome >= 18"])
q_consent_precond_0 -..-> q_age
q_children ---- q_children_precond_0(["q_household.outcome > 1"])
q_children_precond_0 -..-> q_household
%% END_PRECONDITIONS
%% BEGIN_POSTCONDITIONS
q_children ---- q_children_postcond_0{{"q_children.outcome < q_household.outcome"}}
%% END_POSTCONDITIONS
%% BEGIN_ITEM_STYLING
q_age:::always
q_consent:::conditional
q_household:::always
q_children:::conditional
q_end:::always
%% END_ITEM_STYLING
%% BEGIN_CONDITION_STYLING
q_consent_precond_0:::precondition
q_children_precond_0:::precondition
q_children_postcond_0:::postcondition
%% END_CONDITION_STYLING
classDef default fill:#F9F9F9,stroke:#333,stroke-width:2px
classDef always fill:#00CC00,stroke:#000,stroke-width:2px
classDef conditional fill:#FFCC00,stroke:#000,stroke-width:2px
classDef precondition fill:#F5F5DC,stroke:#000,stroke-width:1px
classDef postcondition fill:#E6F0FF,stroke:#000,stroke-width:1px
e1@{ animate: true }
e2@{ animate: true }
e3@{ animate: true }
e4@{ animate: true }The SMT solver automatically verifies:
- Reachability: Green nodes (ALWAYS reachable), yellow nodes (CONDITIONAL on preconditions)
- Preconditions: Rounded nodes show when questions appear (e.g., consent only if age ≥ 18)
- Postconditions: Curly nodes validate answers (e.g., children < household size)
- Consistency: All constraints are simultaneously satisfiable
This happens instantly during design in Armiger, not after deployment when problems are discovered by confused respondents.
Getting Started¶
Ready to create mathematically verified surveys?
→ Quick Start Guide - Complete workflow walkthrough
→ Creating Surveys - Detailed QML guide
→ Theory - Mathematical foundations
Architecture¶
Each service is independently deployable and communicates through well-defined APIs:
- Armiger: Manages code-server instances, load-balances across development environments
- SirWay: Evaluates questionnaires on-the-fly using lazy evaluation semantics
- Targetor: Orchestrates campaigns, tracks demographics and completion rates
- Balansor: Processes response data, applies statistical corrections
All services share a common authentication system and data repository, enabling seamless workflow integration.