Imandra gives AI the
power of reasoning

Large Language Models (LLMs) use Imandra to build mental models and reason about them, unlocking the incredible potential of generative AI for industries where correctness and compliance matter.

NEW:Python library is out!

Our brand new Imandra Core Python library is now available - check it out!

Language Memory Reasoning

Get your LLM to express its thoughts in logic, then tap into automated logical reasoning to:

  • Eliminate hallucinations by making reasoning explicit and explainable
  • Gain trust and demonstrate compliance by formally verifying arguments and results
  • Scale reasoning to unseen depths with auditable logical inference
Get your LLM to express its thoughts in logic!

Watch our explainer video

Lots of exciting announcements soon,
stay in touch:

Python library for
Imandra Core is live!

  • Step 1
    Install Python library from PIP3

    > pip install imandra
  • Step 2
    Install the imandra-cli client, create an account and agree to the community guidelines

    > imandra-cli auth login
  • Step 3
    Start up Python and import Imandra libs (check out examples below)

    > python
    # Python 3.9.5 (default, May 18 2021, 12:31:01)
    # [Clang 10.0.0] :: Anaconda, Inc. on darwin
    # Type “help”, “copyright”, “credits” or “license” for more information

    > import imandra

Examples

import imandra

# Start imandra session using context manager
with imandra.session() as s:

  # Defining a function
  s.eval("let f x = if x > 0 then if x * x < 0 then x else x + 1 else x")

  # Verifying some of its properties / solving constraints
  verify_result = s.verify("fun x -> x > 0 ==> f x > 0")
  instance_result = s.instance("fun x -> f x = 43")

  # Run a Region Decomposition
  decomposition = s.decompose("f")

  print(verify_result)
  print(instance_result)

  # Iterate over regions and print region constraints and invariants
  for n, region in enumerate(decomposition.regions):
    print("-"*10 + " Region", n, "-"*10 + "
    Constraints")
    for c in region.constraints_pp:
      print("  ", c)
      print("Invariant:", "
      ", region.invariant_pp)

For more please check out our documentation pages.

Imandra Docs

Automated Reasoning is the logical complement to LLMs

  • Imandra empowers LLMs with automated logical reasoning at scale, turning opaque models into transparent ones, empowering users and developers to see assumptions and conclusions involved in responses with precise auditable reasoning.
  • Traditionally, these types of techniques were reserved to highly specialized teams of PhDs at places like NASA. Thanks to recent advances, Imandra is highly automated and scaled to most difficult industrial applications.
Automated reasoning is the logical complement to LLMs

The Imandra
Reasoning as a Service® Platform

Imandra is not your typical AI system!

Unlike the approaches of statistical AI (e.g. ChatGPT),
Imandra:

    • relies on automated logical reasoning,
    • converts input into mathematical logic,
    • backs every answer or feedback with a sequence of logical steps that may be audited by an independent tool.
  • Traditionally, these types of techniques were reserved to highly specialized teams of PhDs at places like NASA. Thanks to recent advances, Imandra is highly automated and scaled to most difficult industrial applications.
  • Imandra is already used today by leading financial firms to design, implement and calibrate complex financial systems, including national stock and derivatives exchanges. Outside of finance, our clients include US Air Force and DARPA.

Learn the Technical Details on our Imandra Core Page.

Imandra Core
Imandra Core Process

OCaml and Imandra Modeling Language (IML)

The input language to Imandra is OCaml, a powerful open source functional programming language. For its pure subset, we've created a formal semantics. We call this the Imandra Modeling Language (IML). Imandra's reasoning engine translates IML into mathematical logic and reasons about it.

As long as you can describe something logically or computationally, you can encode and reason about it in Imandra.

Whether it's a a computer program, a cap table, a spreadsheet, case law, a legal argument, financial regulations, a blueprint, tax code, a scheduling problem, ... all of these can be described and reasoned about in Imandra.

https://ocaml.org

Imandra Feature Spotlight:
Region Decomposition

  • What is it?
    Region Decomposition is a key and novel feature of Imandra for explaining the behavior of complex software and algorithms, and exhaustively identifying their edge cases.
  • Why is it novel?
    We have “lifted” a well-established mathematical technique (Cylindrical Algebraic Decomposition or CAD) to algorithms at large, and made significant investments into making it scale to industrial applications.
  • What’s the big deal?
    Regions are fundamental for explanations and generalizations. If a goal is false and Imandra computes a counterexample, it can be generalized into a region which explains why. Explainable generalizations are critical for the convergence of LLMs to correct results, closing off large regions of the search space instead of only eliminating single points.
Region Decomposition Diagram

Other select
features

  • Formal Verification

    • Lower software costs and fix defects early
    • Deliver error-free software
    • Gain deep understanding of algorithm behavior
  • Optimization

    • Optimize software designs along key dimensions
    • Calibrate optimal system modifications
    • Derive actionable intelligence for users of your system
  • Constraint Solving

    • Rich computational modeling language with higher-order, recursive and nonlinear functions
    • Solve complex planning problems
    • Embed in mobile and autonomous systems for robust decision making
  • Symbolic Reasoning

    • Decompose system state spaces and elucidate edge cases
    • Obtain exact symbolic descriptions of possible system behaviors
    • Understand with precision what can possibly go wrong
  • Rule Synthesis

    • Automatically discover key system properties and invariants
    • Learn specifications from data
    • Derive complex transformations and API adapters from analyzing logs
  • Custom Plug-ins

    Extend Imandra's reasoning engine through domain-specific plugins

Learn more and
start your Imandra Journey

Let's talkTalk
to an Expert

Schedule
a contact

Not sure
if we can help?

We'd be happy to discuss your project to suggest the best solution.

Schedule
a case analysis