Condizioni di servizio
1. Cosa fa il servizio
Lei presenta un reclamo e uno standard. Lo facciamo passare attraverso un pannello di modelli AI che si seleziona, più un modello arbitro che regola i criteri di accettazione, e cerchiamo di formalizzare il risultato in Lean 4 contro Mathlib. L'output è una trascrizione, una serie di sentenze, un verdetto, e dove è stata tentata la formalizzazione, il risultato Lean.
2. Che cosa l'uscita è e non è
L'output è generato da modelli di AI di terze parti e non è un consiglio. Non è legale, medico, finanziario, ingegneristico o consulenza professionale di qualsiasi tipo, e nessun rapporto professionale viene creato utilizzando questo servizio.
L'arbitro che decide un criterio soddisfatto è una dichiarazione circa le prove in quella corrispondenza. Non è una garanzia di correttezza. I modelli AI fanno errori, le fonti di lettura errata, e possono fabbricare citazioni nonostante le istruzioni di non. È necessario verificare indipendentemente qualsiasi cosa si intende fare affidamento su, in particolare prima di pubblicarlo, di presentarlo o di agire su di esso. Si tratta di uno strumento per il lavoro di prova di pressione, non un sostituto per la revisione umana qualificata.
Una formalizzazione Lean riuscita significa che il kernel Lean ha accettato una prova della dichiarazione che era stata formalizzata, contro la versione di Mathlib in uso in quel momento. Non significa che la dichiarazione sia una traduzione fedele di ciò che hai chiesto, e scegliere una dichiarazione formale che non dice ciò che intendevi è il modo più comune in cui un risultato formale inganna. Leggere la dichiarazione formale, non solo il verdetto.
3. Il contenuto
Mantenete la proprietà dei crediti che inviate e dell'output prodotto per voi. Ci concedete solo la licenza necessaria per gestire il servizio: per elaborare la vostra presentazione, trasmetterla ai fornitori di modelli selezionati e memorizzare la partita risultante in modo da potervi ritornare.
Le corrispondenze sono private per impostazione predefinita. Se si contrassegna una corrispondenza pubblica, diventa visibile a chiunque abbia il link e può apparire nella nostra galleria pubblica. Non pubblicare una corrispondenza contenente nulla di riservato.
Non inviare dati personali su altri, materiale riservato non hai il diritto di condividere o contenuti illegali.
4. Crediti e fatturazione
Il credito è prepagato e viene consumato come partite eseguite. Ogni partita ha un limite di spesa impostato; raggiungendolo si interrompe la partita piuttosto che continuare a spendere. I saldi non sono trasferibili e, salvo quanto previsto dalla legge, non sono rimborsabili una volta consumato. Il credito non utilizzato è rimborsabile su richiesta.
Se si collega la propria chiave di inferenza, si paga direttamente il fornitore e noi fatturano nessun costo per-token. Passato il previsto indennità gratuita una tassa infrastruttura si applica per coprire l'esecuzione del pannello, strumenti e stoccaggio.
Possiamo cambiare i prezzi con preavviso. Le modifiche non si applicano mai al credito già acquistato.
5. Uso accettabile
Non utilizzare il servizio per generare contenuti che danneggiano gli altri, per cercare di estrarre i nostri suggerimenti o istruzioni di sistema, per aggirare i limiti di spesa o di tasso, o per rivendere l'accesso senza un accordo scritto. Lo strumento di esecuzione del codice è per verificare le richieste; non usarlo per attaccare qualsiasi sistema.
6. Disponibilità
Dipendiamo da fornitori di modelli di terze parti. I fornitori scendono, cambiano modelli e li deprecano. Una corrispondenza interrotta per qualsiasi motivo è sospesa e riutilizzabile; non ci facciamo pagare per lavori che non sono avvenuti. Non garantiamo disponibilità ininterrotta, e un modello che hai usato prima potrebbe diventare non disponibile.
7. Responsabilità
Nella misura massima consentita dalla legge, il servizio viene prestato come senza garanzie di alcun tipo. La nostra responsabilità totale per qualsiasi reclamo è limitata all'importo che ci hai pagato nei tre mesi precedenti la richiesta. Non siamo responsabili per perdite indirette o conseguenti, incluse eventuali perdite derivanti dalla dipendenza dal modello di output.
8. Denuncia
L'utente può chiudere il proprio account in qualsiasi momento; noi rimborseremo il credito non utilizzato. Possiamo sospendere i conti che violano questi termini o che mettono il servizio a rischio.
9. Modifiche, lingua e contatto
Possiamo aggiornare questi termini; modifiche materiali saranno annunciate sul sito.
Le traduzioni di questa pagina sono fornite per comodità e sono prodotte in macchina. Se una traduzione e la versione inglese differiscono, la versione inglese governa.
Domande: Contattaci.