Theorem.chat ਬਾਰੇ
Theorem.chat ਇੱਕ ਗਣਿਤਿਕ ਦਾਅਵੇ ਨੂੰ ਲੈਂਦਾ ਹੈ ਅਤੇ ਇਸ ਨੂੰ ਹੱਲ ਕਰਨ ਦੀ ਕੋਸ਼ਿਸ਼ ਕਰਦਾ ਹੈ । ਤੁਸੀਂ ਦਾਅਵੇ ਨੂੰ ਦੱਸਦੇ ਹੋ, ਅਤੇ ਸਟੈਂਡਰਡ ਨੂੰ ਜੋ ਕਿ ਇਸ ਨੂੰ ਪੂਰਾ ਕਰਨਾ ਚਾਹੀਦਾ ਹੈ । AI ਮਾਡਲਾਂ ਦਾ ਇੱਕ ਪੈਨਲ - ਜਿੰਨੇ ਤੁਸੀਂ ਚਾਹੁੰਦੇ ਹੋ, ਕਿਸੇ ਵੀ ਵੇਚਣ ਵਾਲੇ ਤੋਂ - ਇਸ ਉੱਤੇ ਹਮਲਾ ਕਰਦਾ ਹੈ, ਅਤੇ ਇੱਕ ਹੋਰ ਮਾਡਲ ਰਿਫਰੇਸਰ । ਫਿਰ ਆਰਗੂਮੈਂਟ Mathlib ਦੇ ਵਿਰੁੱਧ Lean 4 ਵਿੱਚ ਫਾਰਮੈਲੀਜ਼ਡ ਹੁੰਦਾ ਹੈ, ਅਤੇ ਲੀਨ ਕਰਨਲ ਫੈਸਲਾ ਕਰਦਾ ਹੈ ਕਿ ਕੀ ਇਹ ਸਾਬਤ ਕੀਤਾ ਗਿਆ ਹੈ । ਆਖਰੀ ਪੜਾਅ ਉਤਪਾਦ ਹੈ ।
ਇੱਕ ਕਰਨਲ ਕਿਉਂ, ਅਤੇ ਹੋਰ ਮਾਡਲ ਨਹੀਂ
ਇੱਕ ਮਾਡਲ ਨੂੰ ਇੱਕ ਸਖਤ ਸਵਾਲ ਪੁੱਛੋ ਅਤੇ ਤੁਹਾਨੂੰ ਇੱਕ ਸਹੀ ਜਾਂ ਗਲਤ ਜਵਾਬ ਮਿਲੇਗਾ । ਕਈ ਸਵਾਲ ਪੁੱਛੋ ਅਤੇ ਉਹ ਅਕਸਰ ਸਹਿਮਤ ਹੋ ਜਾਂਦੇ ਹਨ, ਜੋ ਕਿ ਸਬੂਤ ਵਾਂਗ ਲੱਗਦਾ ਹੈ ਅਤੇ ਨਹੀਂ ਹੈ: ਮਾਡਲ ਟਰੇਨਿੰਗ ਡਾਟਾ ਸਾਂਝਾ ਕਰਦੇ ਹਨ ਅਤੇ ਬਲਿਡ ਸਪਾਟ ਸਾਂਝੇ ਕਰਦੇ ਹਨ । ਪਹਿਲੇ ਮਾਡਲ ਦੀ ਜਾਂਚ ਕਰਨ ਵਾਲਾ ਦੂਜਾ ਮਾਡਲ ਵੀ ਇੱਕੋ ਜਿਹੇ ਕਿਸਮ ਦਾ ਜੱਜ ਹੈ, ਅਤੇ ਇਸ ਬਾਰੇ ਗੱਲ ਕੀਤੀ ਜਾ ਸਕਦੀ ਹੈ । ਲੀਨ ਕਰਨਲ ਨਹੀਂ ਕਰ ਸਕਦਾ ਹੈ । ਇਹ ਜਾਂ ਤਾਂ ਐਕਸੀਓਮ ਅਤੇ Mathlib ਤੋਂ ਸਟੇਟਮੈਂਟ ਪ੍ਰਾਪਤ ਕਰਦਾ ਹੈ, ਜਾਂ ਨਹੀਂ, ਅਤੇ ਭਰੋਸੇ ਦਾ ਨਤੀਜੇ ਉੱਤੇ ਕੋਈ ਪ੍ਰਭਾਵ ਨਹੀਂ ਹੁੰਦਾ ਹੈ ।
ਇੱਕ ਫਾਰਮੈਟ ਪ੍ਰਮਾਣ ਨੂੰ ਫਰਜ਼ੀ ਬਣਾਉਣ ਲਈ ਆਮ ਢੰਗਾਂ ਦੀ ਜਾਂਚ ਕੀਤੀ ਜਾਂਦੀ ਹੈ ਅਤੇ ਮਨਜ਼ੂਰ ਨਹੀਂ ਕੀਤਾ ਜਾਂਦਾ ਹੈ । ਇੱਕ ਪ੍ਰਮਾਣ, ਜੋ ਕਿ sorry ਨਾਲ ਇੱਕ ਖਾਲੀ ਥਾਂ ਛੱਡਦਾ ਹੈ, ਇੱਕ ਜੋ ਕਿ native_decide ਨੂੰ ਕਾਰਨਲ ਨੂੰ ਭਰੋਸੇ ਉੱਤੇ ਇੱਕ ਗਣਨਾ ਕਰਨ ਲਈ ਮਜਬੂਰ ਕਰਦਾ ਹੈ, ਜਾਂ ਇੱਕ ਜੋ ਕਿ ਇੱਕ ਨਵਾਂ ਐਕਸੀਓਮ ਚੁੱਪ ਚਾਪ ਪੇਸ਼ ਕਰਦਾ ਹੈ, ਨੂੰ ਪਛਾਣਿਆ ਜਾਂਦਾ ਹੈ ਅਤੇ ਸਫਲਤਾ ਦੇ ਰੂਪ ਵਿੱਚ ਗਿਣਨ ਦੀ ਬਜਾਏ ਮਨਜ਼ੂਰ ਨਹੀਂ ਕੀਤਾ ਜਾਂਦਾ ਹੈ ।
ਪੈਨਲ ਅਸਲ ਵਿੱਚ ਕੀ ਕਰ ਸਕਦਾ ਹੈ
ਦਲੀਲ ਦੇਣ ਦਾ ਸਸਤਾ ਹਿੱਸਾ ਹੈ । ਪੈਨਲ ਸਾਹਿਤ ਨਾਲ ਕੰਮ ਕਰਦਾ ਹੈ — arXiv, OpenAlex, Crossref — ਇਸ ਲਈ ਇੱਕ ਜਾਣਿਆ ਨਤੀਜਾ ਹਵਾਲਾ ਦਿੱਤਾ ਜਾਂਦਾ ਹੈ ਨਾ ਕਿ ਬੁਰੀ ਤਰ੍ਹਾਂ ਮੁੜ- ਪ੍ਰਾਪਤ ਕੀਤਾ ਜਾਂਦਾ ਹੈ । ਇਸ ਵਿੱਚ SageMath ਅਤੇ PARI/GP ਗਣਨਾ ਲਈ, Z3 ਅਤੇ CVC5 SMT ਹੱਲ ਕਰਨ ਲਈ, OEIS ਲੂਕਅਪ ਇੱਕ ਕ੍ਰਮ ਦੀ ਪਛਾਣ ਕਰਨ ਲਈ, ਅਤੇ ਇੱਕ sandboxed Python ਵਾਤਾਵਰਣ ਨੈੱਟਵਰਕ ਪਹੁੰਚ ਦੇ ਬਿਨਾਂ ਹੈ । ਇੱਕ ਅਨੁਮਾਨ ਨੂੰ ਦਸ ਹਜ਼ਾਰ ਕੇਸਾਂ ਨਾਲ ਟੈਸਟ ਕੀਤਾ ਜਾ ਸਕਦਾ ਹੈ, ਜਦੋਂ ਤੱਕ ਕੋਈ ਵੀ ਇਸ ਨੂੰ ਸਾਬਤ ਕਰਨ ਦੀ ਕੋਸ਼ਿਸ਼ ਕਰਨ ਲਈ ਇੱਕ ਗੇੜ ਖਰਚ ਨਹੀਂ ਕਰਦਾ ਹੈ, ਅਤੇ ਇੱਕ ਕਨਟਰ ਉਦਾਹਰਨ ਨਾਲ ਤੁਰੰਤ ਚਰਚਾ ਖਤਮ ਹੋ ਜਾਂਦੀ ਹੈ ।
ਸਬੂਤ, ਨਾ ਕਿ ਬੋਲਚਾਲ
ਇੱਕ ਮੇਲ ਨੂੰ ਆਰਗੂਮੈਂਟ ਕੁਆਲਟੀ ਉੱਤੇ ਸਕੋਰ ਨਹੀਂ ਦਿੱਤਾ ਜਾਂਦਾ ਹੈ । ਦਾਅਵਾ ਸਵੀਕਾਰ ਕਰ ਲੈਣ ਦੇ ਮਾਪਦੰਡਾਂ ਵਿੱਚ ਵੰਡਿਆ ਜਾਂਦਾ ਹੈ, ਅਤੇ ਇੱਕ ਮਾਪਦੰਡ ਸਿਰਫ ਤਾਂ ਹੀ ਹੱਲ ਕੀਤਾ ਜਾਂਦਾ ਹੈ, ਜਦੋਂ ਇਸ ਪਿੱਛੇ ਕੁਝ ਤੀਜੀ ਧਿਰ ਦੁਆਰਾ ਮੁੜ- ਚੈੱਕ ਕੀਤਾ ਜਾ ਸਕਦਾ ਹੈ: ਇੱਕ ਸਰੋਤ, ਜਿਸ ਵਿੱਚ ਸਬੰਧਤ ਪਾਠ ਹਵਾਲਾ ਦਿੱਤਾ ਗਿਆ ਹੈ, ਜਾਂ ਕੋਡ, ਜੋ ਕਿ ਅਸਲ ਵਿੱਚ ਅਸਲੀ ਆਉਟਪੁੱਟ ਨਾਲ ਚਲਾਇਆ ਗਿਆ ਹੈ । ਰਿਫਰੈਸ਼ਰ ਆਪਣੇ ਆਪ ਨੂੰ ਫੈਸਲਾ ਲੈਣ ਤੋਂ ਪਹਿਲਾਂ ਸਬੂਤ ਮੁੜ- ਚੈੱਕ ਕਰਦਾ ਹੈ, ਅਤੇ ਜਦੋਂ ਤੱਕ ਮਾਪਦੰਡ ਖੁੱਲ੍ਹਾ ਹੈ, ਤਾਂ ਇਹ ਮੈਚ ਨੂੰ ਖਤਮ ਨਹੀਂ ਕਰ ਸਕਦਾ ਹੈ ।
ਤੁਸੀਂ ਪੱਟੀ ਸੈੱਟ ਕੀਤੀ
ਸਟੈਂਡਰਡ ਤੁਹਾਡੀ ਚੋਣ ਹੈ, ਅਤੇ ਰਿਫਰੇਸਰ ਇਸ ਨੂੰ ਅੱਖਰ-ਬ-ਅੱਖਰ ਰੱਖਦਾ ਹੈ । ਇੱਕ ਧਿਆਨ ਨਾਲ ਮਾਹਰ ਜੋ ਵੀ ਮੰਨਦਾ ਹੈ ਉਸ ਲਈ ਪੁੱਛੋ ਅਤੇ ਤੁਸੀਂ ਉਹ ਪ੍ਰਾਪਤ ਕਰੋ । ਹਰ ਇੱਕ ਅਨੁਮਾਨ ਦੇ ਨਾਲ ਇੱਕ ਪੂਰਾ ਦਲੀਲ ਪੁੱਛੋ ਅਤੇ ਤੁਸੀਂ ਇਸ ਦੇ ਵਿਰੁੱਧ ਜੱਜ ਹੋ । ਇੱਕ ਪੁਰਸਕਾਰ ਸੌਂਪਣ ਦਾ ਸਾਹਮਣਾ ਕਰਨ ਲਈ ਇੱਕ ਬਾਰ ਲਈ ਪੁੱਛੋ, ਅਤੇ ਈਮਾਨਦਾਰ ਨਤੀਜਾ ਆਮ ਤੌਰ ਉੱਤੇ ਇੱਕ ਸਪੱਸ਼ਟ ਖਾਤਾ ਹੈ ਕਿ ਪੈਨਲ ਕਿੱਥੇ ਘੱਟ ਗਿਆ ਹੈ - ਜੋ ਕਿ ਇੱਕ ਭਰੋਸੇਯੋਗ ਦਾਅਵੇ ਤੋਂ ਵੱਧ ਹੈ, ਜੋ ਕਿ ਤੁਹਾਨੂੰ ਆਪਣੇ ਆਪ ਨੂੰ ਜਾਂਚਣਾ ਪਵੇਗਾ ।
ਇਸ ਬਾਰੇ ਸਪੱਸ਼ਟ ਕਰਨ ਲਈ: ਇਹ ਮਸ਼ੀਨ ਨਹੀਂ ਹੈ, ਜੋ ਕਿ ਖੁੱਲ੍ਹੀਆਂ ਸਮੱਸਿਆਵਾਂ ਨੂੰ ਹੱਲ ਕਰਦੀ ਹੈ । ਇਹ ਮਸ਼ੀਨ ਹੈ, ਜੋ ਕਿ ਇੱਕ ਆਰਗੂਮੈਂਟ ਨੂੰ ਹੱਲ ਹੋਣ ਲਈ ਪਾਸ ਕਰਨ ਤੋਂ ਇਨਕਾਰ ਕਰਦੀ ਹੈ, ਜਦੋਂ ਕਿ ਇਹ ਹੱਲ ਨਹੀਂ ਹੈ, ਅਤੇ ਇਹ ਤੁਹਾਨੂੰ ਦੱਸਦੀ ਹੈ ਕਿ ਕਿਹੜਾ ਸਟੈਪ ਫੇਲ੍ਹ ਹੋਇਆ ਹੈ ।
ਇੱਕ ਫੇਲ੍ਹ ਫਾਰਮੈਲਿਜ਼ੇਸ਼ਨ ਹੈ, ਜੋ ਕਿ ਲਾਭਦਾਇਕ ਆਉਟਪੁੱਟ ਹੈ
ਜਦੋਂ Lean ਪ੍ਰਮਾਣ ਬੰਦ ਨਹੀਂ ਕਰੇਗਾ, ਤਾਂ ਤੁਹਾਨੂੰ ਬਾਕੀ ਰਹਿਣ ਵਾਲਾ ਸਹੀ ਟੀਚਾ ਮਿਲੇਗਾ । ਪਰਿਭਾਸ਼ਾ ਵਿੱਚ ਇਹ ਹਮੇਸ਼ਾ ਉਹ ਥਾਂ ਹੈ, ਜਿੱਥੇ ਅਨਪੜ੍ਹ ਦਲੀਲ ਹੱਥ- ਵਗਾਉਣੀ ਹੈ — ਇਹ ਕਦਮ ਹਰੇਕ ਨੇ ਪੜ੍ਹਿਆ ਹੋਵੇਗਾ । ਇਹ ਟੀਚਾ ਉਸ ਸੀਟ ਨੂੰ ਦਿੱਤਾ ਜਾਂਦਾ ਹੈ, ਜੋ ਕਿ ਇਸ ਉੱਤੇ ਹਮਲਾ ਕਰਨ ਲਈ ਸਭ ਤੋਂ ਵਧੀਆ ਹੈ, ਜੋ ਕਿ ਪਹਿਲਾਂ ਹੀ ਕੋਸ਼ਿਸ਼ ਕੀਤੀ ਗਈ ਹੈ, ਅਤੇ ਹੋਰ ਕੁਝ ਨਹੀਂ । ਮਾਡਲ ਜਦੋਂ ਰੁਕ ਜਾਂਦੇ ਹਨ ਤਾਂ ਆਪਣੇ ਆਪ ਨੂੰ ਪੂਰੀ ਕੀਮਤ ਉੱਤੇ ਮੁੜ- ਪੇਸ਼ ਕਰਦੇ ਹਨ; ਇੱਕ ਖਾਸ ਸਵਾਲ ਪਾਸ ਕਰਨ ਨਾਲ ਆਮ ਤੌਰ ਉੱਤੇ ਟੋਕਨਾਂ ਦੇ ਇੱਕ ਹਿੱਸੇ ਲਈ ਬਲਾਕ ਖਤਮ ਹੋ ਜਾਂਦਾ ਹੈ ।
ਲੰਮਾ ਕੰਮ ਬਚਿਆ
ਹਰੇਕ ਲੀਮਾ ਜੋ ਪੈਨਲ ਸਥਾਪਤ ਕਰਦਾ ਹੈ, ਇੱਕ ਸਾਂਝੀ ਲੇਜ਼ਰ ਵਿੱਚ ਆਪਣੇ ਪਰੂਫ ਨਾਲ ਜਾਂਦਾ ਹੈ, ਇਸ ਲਈ ਨਤੀਜੇ ਇੱਕ ਵਾਰ ਲਿਖੇ ਜਾਂਦੇ ਹਨ ਅਤੇ ਕਦੇ ਮੁੜ- ਪ੍ਰਾਪਤ ਨਹੀਂ ਕੀਤੇ ਜਾਂਦੇ, ਅਤੇ ਬੇਅੰਤ ਅੰਤ ਰਿਕਾਰਡ ਕੀਤੇ ਜਾਂਦੇ ਹਨ ਤਾਂ ਕਿ ਕੋਈ ਵੀ ਉਨ੍ਹਾਂ ਵਿੱਚ ਵਾਪਸ ਨਾ ਜਾ ਸਕੇ । ਮੈਚ ਸਰਵਰ- ਪਾਸੇ ਚੱਲਦੇ ਹਨ ਅਤੇ ਸਾਫ਼- ਸਫਾਈ ਨਾਲ ਵਿਰਾਮ ਕਰਦੇ ਹਨ - ਬਜਟ ਉੱਤੇ, ਪਰੋਵਾਈਡਰ ਬੰਦ ਹੋਣ ਤੇ, ਜਾਂ ਕਿਉਂਕਿ ਤੁਸੀਂ ਟੈਬ ਬੰਦ ਕੀਤੀ ਹੈ - ਅਤੇ ਉਹਨਾਂ ਨੂੰ ਉਸੇ ਥਾਂ ਮੁੜ ਸ਼ੁਰੂ ਕਰੋ, ਜਿੱਥੇ ਉਹ ਰੁਕ ਗਏ ਸਨ ।
ਇਹ ਕਿਹੜੇ ਲਈ ਨਹੀਂ ਹੈ
ਪ੍ਰਮਾਣੀਕਰਨ ਇੱਕ ਝਲਕਾਰਾ ਸ਼ਬਦ ਹੈ । ਇਹ ਸਾਇਟ ਗਣਿਤ, ਲੋਜੀਕ, ਸਿਧਾਂਤਕ ਕੰਪਿਊਟਰ ਵਿਗਿਆਨ, ਸਿਧਾਂਤਕ ਭੌਤਿਕ ਵਿਗਿਆਨ ਅਤੇ ਆਰਥਿਕ ਸਿਧਾਂਤ ਲਈ ਬਣਾਈ ਗਈ ਹੈ — ਉਹ ਖੇਤਰ ਜਿੱਥੇ ਇੱਕ ਦਾਅਵੇ ਨੂੰ ਸਬੂਤ ਨਾਲ ਹੱਲ ਕੀਤਾ ਜਾਂਦਾ ਹੈ । ਜੀਵ ਵਿਗਿਆਨ, ਦਵਾਈ, ਰਸਾਇਣ ਜਾਂ ਸਮਾਜਿਕ ਵਿਗਿਆਨ ਵਿੱਚ ਅਨੁਭਵੀ ਸਵਾਲ ਪ੍ਰਮਾਣੀਕਰਨ ਨਹੀਂ ਪੈਦਾ ਕਰਦੇ, ਉਹ ਖੋਜ ਪੈਦਾ ਕਰਦੇ ਹਨ ਅਤੇ ਕੋਈ ਵੀ ਫਾਰਮੈਲਿਜ਼ੇਸ਼ਨ ਉਨ੍ਹਾਂ ਨੂੰ ਹੱਲ ਨਹੀਂ ਕਰੇਗੀ । ਸਾਡੀ ਭੈਣ ਸਾਇਟ referee.chat ਉਹਨਾਂ ਸਵਾਲਾਂ ਲਈ ਇੱਕੋ ਪੈਨਲ- ਐਂਡ- ਰਿਫਰੇਸੀ ਪ੍ਰਕਿਰਿਆ ਨੂੰ ਬਿਨਾਂ ਲੀਨ ਸਟੈਪ ਦੇ ਚਲਾ ਰਹੀ ਹੈ ।