ImandraX: una svolta nel ragionamento neurosimbolico AI e nella verifica logica automatizzata

Imandra Inc., l’azienda di intelligenza artificiale che rivoluziona il ragionamento logico automatizzato, ha annunciato il rilascio di ImandraX, l’ultima innovazione nel ragionamento neurosimbolico AI. Questo rilascio introduce capacità all’avanguardia nella automazione della prova, nella generazione di controesempi e nelle procedure decisionali, stabilendo un nuovo standard industriale per l’analisi logica guidata da AI.

Mentre i sistemi di intelligenza artificiale alimentano sempre più applicazioni critiche per la missione in settori come finanza, difesa, sanità e sistemi autonomi, la domanda di ragionamento affidabile, spiegabile e rigorosamente matematico non è mai stata così alta. ImandraX spinge i confini dell’AI integrando potenti capacità di ragionamento automatizzato con agenti AI, framework di verifica e modelli di decisione del mondo reale.

Imandra Inc.: pioniere del ragionamento logico guidato da AI

Imandra Inc. è un’azienda di intelligenza artificiale globale che sviluppa piattaforme di Reasoning-as-a-Service® per il ragionamento logico automatizzato nei settori finanziari, della difesa e della sicurezza critica. Le sue soluzioni avanzate di intelligenza artificiale includono Imandra Markets® e Imandra Connectivity®, che forniscono una rigorosa verifica formale, strumenti di automazione della progettazione e conformità per applicazioni critiche per la missione. Costruiti su avanzate tecniche di ragionamento automatizzato, Imandra consente alle aziende di applicare con fiducia insight guidati da AI logici, precisi e verificabili.
Imandra è impegnata a portare rigore e governance nel mondo degli algoritmi più critici. L’azienda ha costruito un sistema di ragionamento automatizzato su scala cloud, che consente alle organizzazioni di sfruttare la logica matematica per il ragionamento AI. Con un forte accento sullo sviluppo di intelligenza artificiale affidabile e spiegabile, la tecnologia di Imandra è utilizzata da ricercatori, aziende e agenzie governative in tutto il mondo.

Alzare la barra nel ragionamento AI

Denis Ignatovich, co-fondatore e co-amministratore delegato di Imandra Inc., ha dichiarato: “ImandraX è un passo trasformativo per rendere il ragionamento simbolico avanzato una parte fondamentale dei flussi di lavoro AI. Dotando gli agenti AI di potenti capacità di ragionamento logico automatizzato e verifica formale, stiamo spingendo i confini di ciò che i sistemi intelligenti possono raggiungere.”
Dr. Grant Passmore, co-fondatore di Imandra Inc., ha aggiunto: “ImandraX è il culmine di anni di ricerca e di implementazione nel mondo reale in alcuni dei settori più impegnativi, tra cui finanza, difesa e intelligenza artificiale. I nostri clienti e partner si affidano al ragionamento automatizzato di Imandra per garantire la sicurezza e l’affidabilità dei sistemi critici per la missione, dalle borse valori agli agenti autonomi. Con ImandraX, non stiamo solo rendendo il ragionamento rigoroso accessibile, ma stiamo rendendolo indispensabile per la prossima generazione di processi decisionali guidati da AI.”

Innovazioni chiave in ImandraX

ImandraX introduce diverse capacità innovative, tra cui:

• Breakthroughs in Proof Automation – Avanza il ragionamento logico introducendo nuove tecniche per funzioni ricorsive miste discrete e continue su dati. Questa innovazione consente il primo modello formale e la verifica dello standard IEEE P3109 per formati di punto fluttuante binario piccoli (<16 bit), essenziali per la quantizzazione e la distillazione delle reti neurali.
• Verifica della sicurezza delle reti neurali – Consente la prima verifica formale dei checker di proprietà di sicurezza delle reti neurali, sfruttando il controllo dei modelli limitati di ordine superiore e l’induzione per garantire che i modelli AI operino in modo sicuro e come previsto.
• Decomposizione dello spazio degli stati – Fornisce più del 4x di velocizzazione per le attività di decomposizione delle regioni, migliorando notevolmente l’efficienza per gli utenti del settore finanziario nella testing della connettività FIX e in altre applicazioni critiche per la missione.
• Miglioramenti dell’esperienza dello sviluppatore – Un nuovo plugin VS Code introdotto consente lo sviluppo di prove parallele, consentendo ai lavori concorrenti di essere eseguiti nel cloud di ragionamento di Imandra e semplificando il flusso di lavoro di verifica formale.
• Integrazione AI senza soluzione di continuità – ImandraX si integra senza soluzione di continuità con la nuova API Python di Imandra, consentendo un’adozione senza problemi all’interno dei framework di agenti AI, preparando il terreno per la prossima ondata di ragionamento neurosimbolico AI.

Affrontare le sfide logiche più impegnative dell’AI

Denis Ignatovich ha affermato: “ImandraX si basa su anni di applicazioni industriali su larga scala del ragionamento automatizzato. La versione X incorpora nuovi algoritmi di ragionamento, funzionalità architettoniche innovative e un’integrazione senza soluzione di continuità con l’AI agente, compresa la libreria Langgraph.”

Le reti neurali e i modelli di decisione guidati da AI devono affrontare una serie di sfide, tra cui spiegabilità, verificabilità e sicurezza. Molti modelli AI attuali, in particolare quelli utilizzati nell’apprendimento profondo, funzionano come “scatole nere“, rendendo difficile comprendere o verificare i loro processi decisionali. Questa opacità rappresenta un rischio significativo in settori ad alto impatto come finanza, sanità e sistemi autonomi, dove le decisioni AI possono avere profonde conseguenze nel mondo reale.

Per i settori che si affidano alle reti neurali, garantire la robustezza e la sicurezza è fondamentale. Ignatovich spiega: “Le reti neurali sono sempre più utilizzate in settori critici per la sicurezza, quindi è molto importante assicurarsi che si comportino come previsto e siano robuste agli input rumorosi. La capacità di ImandraX di ragionare sulla computazione numerica e la sua infrastruttura di verifica formale generale consentono di verificare le proprietà delle reti neurali, nonché di controllare la correttezza delle prove generate da theorem prover di terze parti.”

Perché questo è importante per la finanza, la difesa e i sistemi autonomi

Settori come finanza, difesa e sistemi autonomi operano in ambienti in cui precisione, affidabilità e conformità sono fondamentali. Gli standard regolatori in questi campi sono in costante evoluzione, richiedendo soluzioni guidate da AI che soddisfino rigorosi requisiti di vigilanza. La mancata ottemperanza a questi regolamenti può portare a conseguenze legali, perdite finanziarie e rischi per la sicurezza.

Ignatovich aggiunge: “Questi settori devono rispettare rigorosi requisiti regolatori e di sicurezza, ma la loro complessità è cresciuta ben oltre ciò che gli esseri umani possono comprendere appieno. L’automazione della prova e la decomposizione dello spazio degli stati di Imandra, combinate con l’integrazione LLM, consentono agli sviluppatori e agli ingegneri di analizzare a fondo il comportamento del sistema, garantire la conformità e testare rigorosamente i sistemi guidati da AI.”

Nel mercato finanziario, gli algoritmi di intelligenza artificiale sono responsabili delle decisioni di trading in tempo reale, della rilevazione delle frodi e della gestione del rischio. Anche le minime discordanze possono avere ripercussioni massive, rendendo essenziale la verifica formale e il ragionamento automatizzato per mantenere l’integrità del sistema. Allo stesso modo, nella difesa, i sistemi autonomi devono operare all’interno di rigidi vincoli, assicurando che le decisioni guidate da AI si allineino con gli obiettivi della missione e i protocolli di sicurezza.

I sistemi autonomi, tra cui veicoli a guida autonoma e droni, dipendono da modelli di intelligenza artificiale che devono navigare in ambienti imprevedibili, garantendo al contempo la sicurezza dei passeggeri e la conformità regolatoria. Assicurarsi che questi sistemi guidati da AI si comportino in modo affidabile in tutte le condizioni possibili richiede metodologie di testing rigorose che i metodi tradizionali non possono fornire. ImandraX interviene offrendo una verifica logica automatizzata che consente un testing basato su scenari approfondito, riducendo i rischi associati all’imprevedibilità dell’AI.

Il futuro dell’intelligenza artificiale neurosimbolica e della decisione guidata da AI

Ignatovich ha sottolineato: “Vediamo gli approcci neurosimbolici come il prossimo grande passo nell’evoluzione dell’AI. I modelli statistici tradizionali, come i LLM, mancano di un ragionamento logico fondamentale. ImandraX colma questo divario, offrendo un’automazione senza precedenti per l’analisi di algoritmi complessi, una delle principali applicazioni dell’AI oggi.”